|| 代わりに入れる時の規則
「代入」についての「規則」について。
スポンサーリンク
代入 Substitution
|| 代わりに入れる
「変数」に『項』を入れること。
（『項』は「定数」「変数」「それらの関数」のどれか）
特に疑問らしい疑問は無いと思います。
具体例
なんらかの式、例えば「 x^2 」があったとして
「 x 」に「 f(y) 」を代入するっていったら、
「 x^2 」が「 \{f(y)\}^2 」になる、この感じ。
代入の厳密な定義
「変数」を「 x 」として
「項 Term」を「 t 」とし
「論理式」を「 φ 」としておきます。
この上で、
「 x と t を入れ替えた論理式」なんかを
『 φ_x[t] 』みたいに書く、ということにしておきます。
まあつまり↓みたいに表現する感じで、
\begin{array}{lllll} \displaystyle φ[x,y,...]&→&\mathrm{subst}(φ,x,t) \\ \\ &→&φ_x[t] \end{array}
この一連の「手順」を指して
『代入 Substitution』と呼ぶことに。
項 Term について
「変数」と「定数」と「関数」について
『代入』での振る舞いを定義していきます。
・定数についての規則
x に t を代入しても定数はそのまま
\begin{array}{rlc} \displaystyle c_x[t]&=&c \end{array}
当たり前ですね。
・変数について
「変数 → 別の項」「別の変数 → 変えない」
この２つのパターンで分けられる。
\begin{array}{rlc} \displaystyle x_x[t]&=&t \end{array}
x を t に置き換え
これは普通の操作ですね。
\begin{array}{rlc} \displaystyle y_x[t]&=&y \end{array}
y は関係なし
これは「複数の変数を区別するため」の決まりです。
これも当たり前ですね。
・関数について
それぞれ見るよ、って感じのやつ。
\begin{array}{llllllll} f(t_1)_x[t]&=&f\Bigl( (t_1)_x[t] \Bigr) \\ \\ \displaystyle \Bigl(f(t_1,t_2)\Bigr)_x[t]&=&f\Bigl( (t_1)_x[t],(t_2)_x[t] \Bigr) \\ \\ \Bigl(f(t_1,t_2,...,t_n)\Bigr)_x[t]&=&f\Bigl( (t_1)_x[t],...(t_n)_x[t] \Bigr) \end{array}
これも当たり前ですね。
\begin{array}{llllllll} \displaystyle f(x)_x[a]&=&f(x_x[a]) \\ \\ &=&f(a) \\ \\ \\ f(x,y)_x[a]&=&f(x_x[a],y_x[a]) \\ \\ &=&f(a,y) \end{array}
具体的にはこれのことですし。
論理式について
「論理式」っていうのは
「項」を「述語記号」で繋げたやつのこと。
そのことを念頭にして
「代入」での振る舞いを定義していきます。
・原子論理式について
「原子論理式」を「 P(t_1,t_2,...,t_n) 」とすると、
\begin{array}{llllllll} \displaystyle \Bigl( P(t_1,t_2,...,t_n) \Bigr)_x[t]&=&P \Bigl( (t_1)_x[t],...,(t_n)_x[t] \Bigr) \end{array}
関数のと同様、まあこんな感じ。
・結合記号に関して
これも単なる記号の移動ですね。
「全体に代入」→「一個一個確認」
こんな感じなので難しく考える必要はありません。
\begin{array}{llllll} \displaystyle (￢φ)_x[t]&=&￢φ_x[t] &&\mathrm{not} \\ \\ \\ (φ∧ψ)_x[t]&=&φ_x[t]∧ψ_x[t] &&\mathrm{and} \\ \\ (φ∨ψ)_x[t]&=&φ_x[t]∨ψ_x[t]&&\mathrm{or} \\ \\ \\ (φ→ψ)_x[t]&=&φ_x[t]→ψ_x[t] &&\mathrm{if}\text{-}\mathrm{then} \\ \\ (φ↔ψ)_x[t]&=&φ_x[t]↔ψ_x[t] &&\mathrm{equal} \end{array}
見ての通り、どれも当然のことですし。
\begin{array}{lllll} \displaystyle \Bigl( φ(x,y)→ψ(x,y) \Bigr)_x[t]&=&φ(x,y)_x[t]→ψ(x,y)_x[t] \\ \\ &=&φ(x_x[t],y_x[t])→ψ(x_x[t],y_x[t]) \\ \\ &=&φ(t,y)→ψ(t,y) \\ \\ \\ \Bigl( φ(y)→ψ(y) \Bigr)_x[t]&=&φ(y)_x[t]→ψ(y)_x[t] \\ \\ &=&φ(y_x[t])→ψ(y_x[t]) \\ \\ &=&φ(y)→ψ(y) \end{array}
実際、具体的には関数のとほぼ同様です。
・量化記号だとどうなるか
「知ってる変数（束縛変数）」と
「知らない変数（自由変数）」とで分けられます。
「知ってる変数 x 」の時
\begin{array}{lllllll} \displaystyle (∀x \, φ)_x[t]&=&∀x \, φ \\ \\ (∃x \, φ)_x[t]&=&∃x \, φ \end{array}
この場合の x はほぼ定数なので
自由変数や条件に合わない定数とは入れ替えができません。
だからこう。
これに対して、
「知らない変数 x 」の時
「束縛変数 y(≠x) 」とすると、
\begin{array}{llllll} \displaystyle (∀y \, φ)_x[t]&=&∀y \, φ_x[t] \\ \\ (∃y \, φ)_x[t]&=&∃y \, φ_x[t] \end{array}
論理式 φ に含まれているかもしれない
そんな「自由変数 x 」がある場合には入れ替えが。
無い場合には入れ替えができません。
以上、長かったですが
これで「代入の定義」については終わりです。
代入可能性 Substitutable
|| 代入できるよっていう性質
ぶち込めるよ、っていう性質のこと。
「論理式 φ の変数 x に項 t が代入可能である」
これの厳密な定義について話すために
とりあえず「論理式 φ,ψ 」「変数 x,y 」「項 t 」を用意。
原子論理式についての規則
「代入して良いですよ」の宣言
原子論理式 φ では t は常に x に「代入可能」である
これは当たり前すぎるので解説は不要でしょう。
ただ、この言い回しは↓でも使うので、
「論理式 φ の変数 x に項 t は代入可能である」
「 t\mathrm{ \,\, is \,\, substitutable \,\, for \,\,} x \mathrm{\,\, in \,\,} φ 」
\begin{array}{llllll} \displaystyle \mathrm{Substitutable}(φ,x,t) \end{array}
これを省略するための記号を定義しておきます。
命題記号についての規則
↑で定義した記号を使うと
\begin{array}{llllll} \displaystyle \mathrm{Substitutable}(φ,x,t)&⇔&\mathrm{Substitutable}(￢φ,x,t) \\ \\ \\ \mathrm{Substitutable}\Bigl( (φ,ψ),x,t \Bigr)&⇔&\mathrm{Substitutable}(φ∧ψ,x,t) \\ \\ \mathrm{Substitutable}\Bigl( (φ,ψ),x,t \Bigr)&⇔&\mathrm{Substitutable}(φ∨ψ,x,t) \\ \\ \\ \mathrm{Substitutable}\Bigl( (φ,ψ),x,t \Bigr)&⇔&\mathrm{Substitutable}(φ→ψ,x,t) \\ \\ \mathrm{Substitutable}\Bigl( (φ,ψ),x,t \Bigr)&⇔&\mathrm{Substitutable}(φ⇔ψ,x,t) \end{array}
まあこんな感じ。
これも特に疑問は出ないと思います。
量化記号についての規則
ここはちょっとややこしいです。
自由変数やら束縛変数やらの規則も加わるので。
\begin{array}{llllll} \displaystyle \mathrm{Substitutable}(∀y \, φ,x,t)&⇔&\mathrm{Condition}(φ,(x,y),t) \\ \\ \\ \mathrm{Substitutable}(∃y \, φ,x,t)&⇔&\mathrm{Condition}(φ,(x,y),t) \end{array}
条件 \mathrm{Condition}(φ,(x,y),t) はややこしいので↓に追記
\begin{array}{llllll} \displaystyle &y&≠&x \\ \\ ∨&x&∈&\mathrm{fr}(φ) \\ \\ ∨\Bigl( & y&∉&\mathrm{fr}(t)&∧&\mathrm{Substitutable}(φ,x,t) \Bigr) \end{array}
なんか難しく見えるかもしれませんが、
要は「 y と x は違う」って話で、
y≠x と x∈\mathrm{fr(φ)} はただ同値関係になる命題。
メインは一番下のやつで、
他はおまけだと思ってOKです。
そんなに難しく考えないでください。
ちなみに \mathrm{fr}(φ) の記号は
『論理式 φ の中にある全ての自由変数の集合』を表しています。
以上、代入に関してはこんな感じです。
まあ要はただ「入れ替え」できるよって話で、
そんな難しいこと言ってるわけではありません。
厳密な定義には細かな条件が必要になった。
だからこんな面倒な感じになった。
ただそれだけの話なので、
「代入が不可能」な時（量化あたり）だけ押さえてれば、
まあ他のは特に覚えなくても大丈夫だと思います。
