代入規則 Substitution Rules


|| 代わりに入れる時の規則

そのまま「代入」についての「規則」ですね。

じゃあ代入ってなに?ってなると思うんで、それやりましょう。

スポンサーリンク






代入 Substitution


|| 代わりに入れる

簡単に言えば、「変数」を『項』と入れ替えることです。

(『項』は基本的には「定数」か「変数」か「それらの関数」)




「変数」と「項」について知ってれば、

そりゃそうだって感じですね。






具体例


なんらかの式、例えば「 x^2 」がありまして、

x 」に「 f(y) 」を代入するっていったら、

\{f(y)\}^2 」になる感じ。




これを一般化(いくつでもOK)したものが、規則になります。






代入の厳密な定義


「変数」をいつものように「 x 」と。

「項 Term」をいつものように「 t 」としましょう。

「論理式」も、とりあえず「 φ 」としておきます。




ここで「 xt を入れ替えた論理式」を、

φ_x[t] 』と「定義」します。(ただの決まり)

(ただし入れ替えるのは自由変数だけ)



別の書き方だと↓みたいな感じ。

形式っぽいですけど形式的じゃないです。

↑で言ってることを、なんかそれっぽく書いただけ。


φ[x,y,...]\,\,\,→subst(φ,x,t)→\,\,\,φ_x[t]



この一連の「手順」を『代入 Substitution』と定義してます。




そしてこの手順の結果「 φ_x[t] 」は、

↓みたいに「再帰的定義」されます。






まず「」について( u とします)


とゆーわけで「変数」と「定数」と「関数」についてです。

項の定義のやり方を思い出していただければ、だいたいあんな感じ。






・定数についての規則


c_x[t]=c



xt を代入したら、定数はそのまま」ってこと






・変数について


次に「知ってる変数」と「知らない変数」について。



x_x[t]=t 』( xt に置き換え)

y_x[t]=y 』( y は関係なし)






・関数について


2つくらいに減らしてみると直観的です。



(\,f(t_1,t_2,...,t_n)\,)_x[t]=f(t_1)_x[t],...f(t_n)_x[t]



要は「 分解できるよ 」ってこと

+ とかで見ると分かり易いかも)




ここまではっきりしたんで、

次はこの「項」を使った「論理式」について。






論理式について( φ で)


「論理式」は「項」を「述語記号」で繋げたやつのことです。




・原子論理式について


「原子論理式」を「 P(t_1,t_2,...,t_n) 」ってすると、



(P(t_1,t_2,...,t_n))_x[t]=P(t_1)_x[t],...,P(t_n)_x[t] (分解)



P= とかで置き換えると分かり易いかも)






・結合記号に関して


これも分解できるよって言ってる感じ。

難しく考える必要はありません。




否定『 (¬φ)_x[t]=(¬φ_x[t]) 』(文否定したら全部否定)

論理積『 (φ∧ψ)_x[t]=(φ_x[t]∧ψ_x[t]) 』(置換しても関係は同じ)

論理和『 (φ∨ψ)_x[t]=(φ_x[t]∨ψ_x[t])

論理包含『 (φ→ψ)_x[t]=(φ_x[t]→ψ_x[t])

同値『 (φ↔ψ)_x[t]=(φ_x[t]↔ψ_x[t])



具体的に、なんか文章書いてみたら分かります。

基本は『文字が変わる』だけです。






・量化記号だとどうなるか


当然のように「知ってる変数」と「知らない変数」で分けられます。



「知ってる変数」のとき( x

全称量化『 (∀x\,φ)_x[t]=∀x\,φ 』( x は束縛されてるんで)

存在量化『 (∃x\,φ)_x[t]=∃x\,φ




「知らない変数」のとき( y

(∀y\,φ)_x[t]=∀y\,φ_x[t] 』(知らん奴には影響なし)

(∃y\,φ)_y[t]=∃x\,φ_x[t] 』(後は項で場合分け)




長かったですが、これで「代入した結果」の定義は終わりです。

次は「代入できるかどうか」の話に移ります。







代入可能性 Substitutable


要は、ぶち込めるよ!ってこと。

これを定義して、こういう時は「代入していいよ」って感じです。




というわけで「代入可能性」の厳密な定義について。



まず恒例「論理式」と「変数」と「項」を用意。

それぞれ「 φ,ψ 」「 x,y 」「 t 」で。




というわけで、↓を満たすとき「代入可能」って言えますよと。

要約すると「代入」は定義できてるんで、

それが「できる」って宣言してるだけですね。






原子論理式についての規則


規則っちゃ規則ですけど、感覚的には許可っぽい感じ?

要約すると「代入して良いですよ」の宣言です。



原子論理式 φ では、

t は、常に x に「代入」できる






命題記号についての規則


これも似たようなものなんで、省略したいです。



重要なのは『 tx に代入できる』って部分だけ。

ここでは「 ¬φ,φ∧ψ,φ∨ψ,φ→ψ 」でもいけるぞ、

と宣言されます。






量化記号についての規則


「量化記号」では( y は束縛されてるから、 y に代入は無理)

ここはちょっと複雑です。複数の条件が存在します。




∀y\,φ∃y\,φ 』に、

tx に代入できる』とは、



次の条件を、どれか一個満たしてるとき(代入の定義から)



x≠y 』(関係ないからいける)

x∉fr(φ) 』(自由変数じゃなけりゃOK)

『「代入できて」かつ「 yt の中に現れない」』



(要は x=y を避けてるってこと)






と、これでようやく終わりです。



要約すればほんとに単純で、ただ「入れ替え」できるよって話。

細かな条件が必要になったら、ここで確認すればいいわけですね。




無理な時だけ押さえてれば、まあ大丈夫じゃないでしょうか。

主に「量化記号」の取り扱いとか。

他は直観的にできることを許可してるだけなので。