|| 記号を入れ替える時の規則
「問題無く代入ができる」の具体的な中身
スポンサーリンク
代入規則の概要
これは「論理式」の後に定義されるので
\begin{array}{lcl} 言語定義段階 && 意味を持たない記号が存在するだけ \\ \\ 項定義段階 && 定数と変数と関数の出力 \\ \\ 論理式定義段階 && 論理的主張の最低限の形 \\ \\ \\ 変数分類段階 && 自由変数と束縛変数 \\ \\ α変換定義段階 && 束縛変数の同意味での記号入れ替え \\ \\ 代入定義段階 && 問題無く代入できるとは \end{array}
まずは「論理式」についての確認を推奨します。
（確認しなくても感覚的には分かるはず）
\begin{array}{ccc} 代入規則 & \left\{ \begin{array}{l} 変数・項・命題変数の入れ替え \\ \\ 自由変数と束縛変数での注意事項 \end{array} \right. \end{array}
概観としてはシンプルなので
理解のハードルはけっこう低いと思います。
記号変換
これは元を辿っていくと
「記号の入れ替え」についての考察から始まっていて
\begin{array}{ccc} 記号変換 & \left\{ \begin{array}{l} 意味不変記号変換 &\Longleftrightarrow& α変換 \\ \\ 意味可変記号変換 &\Longleftrightarrow& 代入 \end{array} \right. \end{array}
結果、このように分類された形の１つとして
「代入」という操作は定義されています。
意味不変記号変換
「 α 変換」とも呼ばれるこれは
（ λ 計算上の最初の規則であることが由来）
\begin{array}{ccc} \left( \begin{array}{ccc} 束縛変数 && 自由変数 \\ \\ \forall x \,\, P(x)&& Q(x) \end{array} \right) &\Longrightarrow& \forall x \,\, P(x) \to \forall y \,\, P(y) \end{array}
要はこういう「重複を避ける」感じの話で
（意味が異なる同じ記号を別々の記号へ）
\begin{array}{ccc} 別々に書くべき変数 &\to& 記号書き換え \\ \\ 変数の衝突回避 &\to& α変換 \end{array}
主に「変数の衝突を回避する」ための操作になります。
代入 Substitution
|| 代わりに入れるという記号操作
\begin{array}{lcl} φ[x/t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \\ \\ φ_x[t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \\ \\ φ[x:=t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \end{array}
『束縛変数には触らない』という制限が付いています。
（構文規則としての代入規則で触れるのは自由変数だけ）
代入規則 Substitution Rules
確認しておくと
\begin{array}{ccc} f(x) &\overset{xに1を代入する}{\Longrightarrow}& f(1) \\ \\ P(y) &\overset{yに3を代入する}{\Longrightarrow}& P(3) \end{array}
「代入」の具体的な操作はこんな感じです。
（感覚的に分かる通りの操作）
\begin{array}{ccc} φ[x:=t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \end{array}
そしてこの「代入」という操作は
『定数』に対して行う場合
\begin{array}{rlc} c[x:=t]&=&c \end{array}
無意味な操作となり
（代入という操作を適用しても変化無し）
\begin{array}{lcl} x[x:=t]&=&t \\ \\ y[x:=t] &=& y \end{array}
『自由変数』に対してだけ意味を持つ操作になります。
（記号の入れ替え操作なので区別される）
関数での代入
以上の振る舞いから分かる通り
\begin{array}{ccc} φ_x[t] &\Longleftrightarrow& 式φの自由変数xを項tに置き換える \end{array}
「自由変数を持つ関数」における「代入」は
（見た目を短くするためにこの表記を採用）
\begin{array}{lcl} 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}{lclcl} 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}
具体的にはこのような操作を許可します。
（やっていい記号の操作を宣言してるだけ）
論理式での代入
まず「原子論理式」から辿っていくと
\begin{array}{lcl} \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}{lcl} (￢φ)_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}{lcl} \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}
具体的にはこんな感じです。
（何度も言ってるようにこれは単なる記号操作です）
述語論理での代入
問題はこの範囲の話で
\begin{array}{lcl} \Bigl( ∀x \, φ(x,y) \Bigr)[y:= t]&=&∀x \, φ(x,y[y:=t]) && 代入 \\ \\ \Bigl( ∀x \, φ(x) \Bigr)[x:= t]&=&\Bigl( ∀y \, φ(y) \Bigr)[x:= t] && α変換 \end{array}
ここで「代入における注意事項」が出てきます。
（ \forall x \,\, φ(x) の x は束縛変数であるため代入不可）
ここで使われるのが
\begin{array}{ccc} φ[x=y] &\Longleftrightarrow& 束縛変数記号xを記号yに書き換える \end{array}
「意味不変記号変換（α変換）」と
（ ( \forall x \,\, P(x) )[x=y]=\forall y \,\, P(x)[x=y]=\forall y \,\, P(y) とする）
\begin{array}{lcl} \mathrm{Free}(t) &\Longleftrightarrow& 項tの中にある自由変数記号の全て \\ \\ \mathrm{Free}(t) &\Longleftrightarrow& 項tを分解して取り出せる全ての自由変数 \end{array}
「項 t の自由変数集合」という概念で
（ t=f(x,y) なら \mathrm{Free}(t)=\{x,y\} こうなる）
\begin{array}{ccc} (\forall x \,\, φ)[y:=t] & \left\{ \begin{array}{lcl} \forall x \,\, φ && \mathrm{if} \,\, x=y \\ \\ \forall x \,\, φ[y:=t] && \mathrm{if} \,\, x\not\in \mathrm{Free}(t) \\ \\ (\forall x \,\, φ)[x=新記号][y:=t] && \mathrm{if} \,\, x\in \mathrm{Free}(t) \end{array} \right. \end{array}
これで場合分けすることにより
（項 t の中で記号 x が自由変数なら新記号に x をα変換）
\begin{array}{ccc} (\forall x \,\, φ)[y:=t] & \left\{ \begin{array}{lcl} \forall x \,\, φ && \mathrm{if} \,\, x=y \\ \\ \forall x \,\, φ[y:=t] && \mathrm{if} \,\, x\not\in \mathrm{Free}(t) \\ \\ (\forall x \,\, φ)[x=新記号][y:=t] && \mathrm{if} \,\, x\in \mathrm{Free}(t) \end{array} \right. \\ \\ \\ (\exists x \,\, φ)[y:=t] & \left\{ \begin{array}{lcl} \exists x \,\, φ && \mathrm{if} \,\, x=y \\ \\ \exists x \,\, φ[y:=t] && \mathrm{if} \,\, x\not\in \mathrm{Free}(t) \\ \\ (\exists x \,\, φ)[x=新記号][y:=t] && \mathrm{if} \,\, x\in \mathrm{Free}(t) \end{array} \right. \end{array}
「量化」における「代入規則」は
「束縛変数を直接触らない」形でこのように表現されます。
（ややこしいが要は記号をちゃんと整理してるだけ）
代入規則についての整理
整理すると
\begin{array}{lclcl} c[x:=t]&=&c && 定数 \\ \\ \\ x[x:=t]&=&t && 置き換え対象の自由変数 \\ \\ y[x:=t] &=& y &&置き換え対象でない自由変数 \end{array}
「項」については
（項は定数または変数または関数の出力）
\begin{array}{lcl} 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}{lcl} \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}{lcl} (￢φ)_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}{ccc} (\forall x \,\, φ)[y:=t] & \left\{ \begin{array}{lcl} \forall x \,\, φ && \mathrm{if} \,\, x=y \\ \\ \forall x \,\, φ[y:=t] && \mathrm{if} \,\, x\not\in \mathrm{Free}(t) \\ \\ (\forall x \,\, φ)[x=新記号][y:=t] && \mathrm{if} \,\, x\in \mathrm{Free}(t) \end{array} \right. \\ \\ \\ (\exists x \,\, φ)[y:=t] & \left\{ \begin{array}{lcl} \exists x \,\, φ && \mathrm{if} \,\, x=y \\ \\ \exists x \,\, φ[y:=t] && \mathrm{if} \,\, x\not\in \mathrm{Free}(t) \\ \\ (\exists x \,\, φ)[x=新記号][y:=t] && \mathrm{if} \,\, x\in \mathrm{Free}(t) \end{array} \right. \end{array}
「述語論理」のパターンで
それぞれこのように定義されています。
（以上の「代入の振る舞い」が代入規則と呼ばれる）
代入可能性 Substitutable
|| 自由変数が束縛変数にならないように
『代入が問題無くできる』の具体的な中身
\begin{array}{lcl} 代入規則 && 束縛変数が重複したらα変換 \\ \\ 代入可能性 && 自由変数が束縛されるのを回避 \end{array}
「代入」における最後のチェック項目で
（定義段階ではなく代入をする段階での重複を防ぐ）
\begin{array}{lcl} \Bigl( \forall x \,\, φ(x,y) \Bigr) [y=t] &\overset{代入できる？}{\longrightarrow}& t=f(z) && 〇 \\ \\ \Bigl( \forall x \,\, φ(x,y) \Bigr) [y=t] &\overset{代入できる？}{\longrightarrow}& t=f(x) && × \end{array}
こういう操作をこの段階で禁止します。
（自由変数→束縛変数の形を回避する）
束縛変数と代入可能性
これは「自由変数である」と
「束縛変数である」を使うことで
\begin{array}{ccc} \mathrm{Bound}(φ) &\Longleftrightarrow& φの全ての束縛変数 \\ \\ \mathrm{Free}(t) &\Longleftrightarrow& tの全ての自由変数 \end{array}
「変数が被らない」を意味する
\begin{array}{ccc} \mathrm{Bound}(φ)∩\mathrm{Free}(t) &=& ∅ \end{array}
このような形で定義されています。
（この辺りの詳細は変数の記事で扱います）
意味不変記号変換の規則
補足しておくと
「意味不変記号変換（α変換）」の定義は
\begin{array}{lcl} \forall x \,\, φ &\to& xは束縛変数である \\ \\ \exists x \,\, φ &\to& xは束縛変数である \end{array}
まず「束縛変数かどうか」の判定から始まります。
（ φ はこの時点では中身が不明な論理式）
\begin{array}{ccc} xは束縛変数である &\to& (\forall x \,\, φ)[x=y] \end{array}
そこから想定されるこの「最初の形」から
（α変換が必要となる場合にこの形が想定される）
\begin{array}{ccc} (\forall x \,\, φ)[x=y] &\Longleftrightarrow& 束縛変数記号xをyに書き換える \end{array}
「新記号 y に入れ替える」というのが「α変換」であり
\begin{array}{ccc} x[x=y]&=& y \end{array}
その最終着地としてこの操作が置かれ
（最初の形からこの最終着地に至るのがα置換）
「任意の論理式 φ 」から
\begin{array}{lcl} \Bigl(f(t_1,...,t_n)\Bigr)[x=y]&=&f\Bigl( (t_1)[x=y],...(t_n)[x=y] \Bigr) \\ \\ \Bigl( P(t_1,...,t_n) \Bigr)[x=y]&=&P \Bigl( (t_1)[x=y],...,(t_n)[x=y] \Bigr) \end{array}
「最終着地 x[x=y]= y に辿り着く」ために
\begin{array}{lcl} (￢\phi )[x=y]&=&￢\phi [x=y] &&\mathrm{not} \\ \\ \\ (\phi∧ψ)[x=y]&=&\phi[x=y]∧ψ[x=y] &&\mathrm{and} \\ \\ (\phi∨ψ)[x=y]&=&\phi[x=y]∨ψ[x=y]&&\mathrm{or} \\ \\ \\ (\phi→ψ)[x=y]&=&\phi[x=y]→ψ[x=y] &&\mathrm{if}\text{-}\mathrm{then} \\ \\ (\phi↔ψ)[x=y]&=&\phi[x=y]↔ψ[x=y] &&\mathrm{equal} \\ \\ \\ (\forall x \,\, \phi )[x=y] &=& \forall x \,\, (\phi [x=y] ) && \mathrm{All} \\ \\ (\exists x \,\, \phi )[x=y] &=& \exists x \,\, (\phi [x=y] ) && \mathrm{Exist} \end{array}
（束縛子と最終着地が前提にあって他はその補助）
新記号 New Symbol
↑ でこれの詳細について省略したのは
\begin{array}{ccc} f\Bigl( x,y,g(z) \Bigr) &\to& aが無い \\ \\ f\Bigl( x,y,g(z) \Bigr) &\to& x_1が無い \\ \\ f\Bigl( x,y,g(z) \Bigr) &\to& x_nが無い \\ \\ & \vdots \end{array}
人間視点ではパっと見で分かる上に
（あえて定義しなくても人間にとって明らか）
\begin{array}{lcl} 新記号 &\to& 論理式の定数記号と変数記号以外の記号 \\ \\ 論理式 &\to& 全ての定数記号と変数記号 \end{array}
形式的に求めるのが意外と面倒だからで
（論理式を分解して定数と変数の記号を取り出すのが大変）
\begin{array}{ccc} *はφの新記号である &\Longleftrightarrow& *はφの記号ではない \\ \\ \mathrm{NewVar}(φ,*) &\Longleftrightarrow& * \not\in \mathrm{Symbols}(φ) \end{array}
実際、これを定義しようとすると
「自由変数の集合」のようなものを作る必要があります。
記号抽出写像 Symbol Extraction Map
↑ を厳密に定義するためには
\begin{array}{ccc} 論理式表現記号 & \left\{ \begin{array}{ll} 項表現記号 & \left\{ \begin{array}{ll} 定数記号 \\ \\ 変数記号 \\ \\ 関数記号 \end{array} \right. \\ \\ \\ 論理記号 & \left\{ \begin{array}{l} 述語記号 \\ \\ 論理演算記号 \\ \\ 量化記号 \end{array} \right. \end{array} \right. \end{array}
「論理式で使われている記号」を考えて
（より厳密には「括弧やカンマなど」の「基礎記号」も）
\begin{array}{ccc} \mathrm{Symbols}(φ) &=& φの中にある全ての記号 \end{array}
まず「記号の集合」を得る関数を想定する必要があります。
（この具体的な中身を詰め込む形で定義する）
記号抽出写像の振る舞い
まず簡単な具体例を考えて
\begin{array}{lcl} \mathrm{Symbols}(c) &=& \{c\} \\ \\ \mathrm{Symbols}(x) &=& \{x\} \\ \\ \mathrm{Symbols}\Bigl( f(x,y) \Bigr) &=& \{f,x,y\} \end{array}
この「記号抽出写像」の振る舞いを考えると
\begin{array}{ccc} \mathrm{Symbols}\Bigl( f(x,y) \Bigr) &=& \{f\}∪\mathrm{Symbols}(x) ∪ \mathrm{Symbols}(y) \end{array}
最終着地については
\begin{array}{ccc} \mathrm{Symbols}(項) &=& \{ 関数記号,定数記号,変数記号 \} \end{array}
こんな感じになりそうだということが分かります。
（項にまで辿り着ければ全部の記号が得られる）
論理式からの逆算
以上を踏まえて
\begin{array}{lcl} \mathrm{Symbols}\Bigl( f(t_1,...,t_n) \Bigr) &=& \{f\}∪\mathrm{Symbols}(t_1)∪\cdots ∪ \mathrm{Symbols}(t_n) \\ \\ \mathrm{Symbols}\Bigl( P(t_1,...,t_n) \Bigr) &=& \{P\}∪\mathrm{Symbols}(t_1)∪\cdots ∪ \mathrm{Symbols}(t_n) \end{array}
「関数」と「原子論理式」がこうなるとすると
\begin{array}{lcl} \mathrm{Symbols}(￢\phi )&=&\{￢\}∪\mathrm{Symbols}(\phi ) \\ \\ \\ \mathrm{Symbols}(\phi∧ψ)&=&\{∧\} ∪\mathrm{Symbols}(\phi) ∪ \mathrm{Symbols}(ψ) \\ \\ \mathrm{Symbols}(\phi∨ψ)&=&\{∨\} ∪\mathrm{Symbols}(\phi) ∪ \mathrm{Symbols}(ψ) \\ \\ \\ \mathrm{Symbols}(\phi→ψ)&=&\{→\} ∪\mathrm{Symbols}(\phi) ∪ \mathrm{Symbols}(ψ) \\ \\ \mathrm{Symbols}(\phi↔ψ)&=&\{↔\} ∪\mathrm{Symbols}(\phi) ∪ \mathrm{Symbols}(ψ) \\ \\ \\ \mathrm{Symbols}( \forall x \,\, \phi )&=&\{\forall , x \} ∪\mathrm{Symbols}(\phi) \\ \\ \mathrm{Symbols}( \exists x \,\, \phi )&=&\{\exists , x \} ∪\mathrm{Symbols}(\phi) \end{array}
「論理式から」の逆算のためには
こういった手順が必要であることが分かります。
（これにより記号抽出写像は再帰的に定義されたと言える）