|| 代わりに入れる時の規則
そのまま「代入」についての「規則」ですね。
じゃあ代入ってなに？ってなると思うんで、それやりましょう。
スポンサーリンク
代入 Substitution
|| 代わりに入れる
簡単に言えば、「変数」を『項』と入れ替えることです。
（『項』は基本的には「定数」か「変数」か「それらの関数」）
「変数」と「項」について知ってれば、
そりゃそうだって感じですね。
具体例
なんらかの式、例えば「 x^2 」がありまして、
「 x 」に「 f(y) 」を代入するっていったら、
「 \{f(y)\}^2 」になる感じ。
これを一般化（いくつでもOK）したものが、規則になります。
代入の厳密な定義
「変数」をいつものように「 x 」と。
「項 Term」をいつものように「 t 」としましょう。
「論理式」も、とりあえず「 φ 」としておきます。
ここで「 x と t を入れ替えた論理式」を、
『 φ_x[t] 』と「定義」します。（ただの決まり）
（ただし入れ替えるのは自由変数だけ）
別の書き方だと↓みたいな感じ。
形式っぽいですけど形式的じゃないです。
↑で言ってることを、なんかそれっぽく書いただけ。
φ[x,y,...]\,\,\,→subst(φ,x,t)→\,\,\,φ_x[t]
この一連の「手順」を『代入 Substitution』と定義してます。
そしてこの手順の結果「 φ_x[t] 」は、
↓みたいに「再帰的定義」されます。
まず「項」について（ u とします）
とゆーわけで「変数」と「定数」と「関数」についてです。
項の定義のやり方を思い出していただければ、だいたいあんな感じ。
・定数についての規則
c_x[t]=c
「 x に t を代入したら、定数はそのまま」ってこと
・変数について
次に「知ってる変数」と「知らない変数」について。
『 x_x[t]=t 』（ x を t に置き換え）
『 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 に「代入」できる
命題記号についての規則
これも似たようなものなんで、省略したいです。
重要なのは『 t を x に代入できる』って部分だけ。
ここでは「 ￢φ,φ∧ψ,φ∨ψ,φ→ψ 」でもいけるぞ、
と宣言されます。
量化記号についての規則
「量化記号」では（ y は束縛されてるから、 y に代入は無理）
ここはちょっと複雑です。複数の条件が存在します。
『 ∀y\,φ と ∃y\,φ 』に、
『 t を x に代入できる』とは、
次の条件を、どれか一個満たしてるとき（代入の定義から）
『 x≠y 』（関係ないからいける）
『 x∉fr(φ) 』（自由変数じゃなけりゃOK）
『「代入できて」かつ「 y が t の中に現れない」』
（要は x=y を避けてるってこと）
と、これでようやく終わりです。
要約すればほんとに単純で、ただ「入れ替え」できるよって話。
細かな条件が必要になったら、ここで確認すればいいわけですね。
無理な時だけ押さえてれば、まあ大丈夫じゃないでしょうか。
主に「量化記号」の取り扱いとか。
他は直観的にできることを許可してるだけなので。