コラム　代入の定義

Last-modified: Sun, 16 Apr 2017 21:46:35 JST (2559d)
Top > コラム　代入の定義
述語論理へ戻る。

ここでは論理式への「代入」という操作を厳密に定義します。与えられた論理式\( \Phi \)に対して、「変項\( x \)に項\( t \)を代入する」という操作は以下のように再帰的に定義することが出来ます。

定義1（代入の再帰的定義）
(1) \( \Phi \)が原子式である場合、文字列として\( \Phi \)に現れる\( x \)を全て\( t \)に置換して得られる原子式を\( (\Phi)[t/x] \)と置く。
(2) \( \Phi \)が論理式\( \Phi_1 \)と\( \Phi_2 \)を用いて\( (\Phi_1) \vee (\Phi_2) \)と表される場合、論理式\( ( (\Phi_1)[t/x]) \vee ( (\Phi_2)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(3) \( \Phi \)が論理式\( \Phi_1 \)と\( \Phi_2 \)を用いて\( (\Phi_1) \wedge (\Phi_2) \)と表される場合、論理式\( ( (\Phi_1)[t/x]) \wedge ( (\Phi_2)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(4) \( \Phi \)が論理式\( \Psi \)を用いて\( \neg (\Psi) \)と表される場合、論理式\( \neg ( (\Psi)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(5) \( \Phi \)が論理式\( \Phi_1 \)と\( \Phi_2 \)を用いて\( (\Phi_1) \to (\Phi_2) \)と表される場合、論理式\( ( (\Phi_1)[t/x]) \to ( (\Phi_2)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(6) \( \Phi \)が\( x \)や\( t \)と文字として異なる変項\( y \)*1と論理式\( \Psi \)を用いて\( \forall y (\Psi) \)と表される場合、論理式\( \forall y ( (\Psi)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(7) \( \Phi \)が\( x \)や\( t \)と文字として異なる変項\( y \)と論理式\( \Psi \)を用いて\( \exists y (\Psi) \)と表される場合、論理式\( \exists y ( (\Psi)[t/x]) \)を\( (\Phi)[t/x] \)と置く。
(8) \( \Phi \)が\( x \)か\( t \)と文字として等しい変項\( y \)と論理式\( \Psi \)を用いて\( \forall y (\Psi) \)と表される場合、論理式\( \Phi \)を\( (\Phi)[t/x] \)と置く。
(9) \( \Phi \)が\( x \)か\( t \)と文字として等しい変項\( y \)と論理式\( \Psi \)を用いて\( \exists y (\Psi) \)と表される場合、論理式\( \Phi \)を\( (\Phi)[t/x] \)と置く。

この再帰的定義における(8)と(9)は全ての状況で代入操作を定義するための便宜的なもので、実際はこれらの状況を考えないようにすることが多く、また文献によってはこれらの状況では代入が定義されないとすることもあります*2。少々煩雑な再帰的定義になっているので、代入操作の計算例を見てみましょう。

例2（代入操作の計算例）
\( x \)と\( y \)を相異なる変項とし、\( t \)を\( x \)や\( y \)と異なる項とする。この時、論理式\( (\forall x ( (t \in x) \vee \neg (y \in t) ) ) \to (\exists y (y \in y) ) \)を\( \Phi \)と置くと、論理式\( \Phi[t/x] \)は以下のように計算される。
　\( ( (\forall x ( (t \in x) \vee \neg (y \in t) ) ) \to (\exists y ( (y \in x) \wedge (x \in t) ) ) )[t/x] \)
＝\( ( (\forall x ( (t \in x) \vee \neg (y \in t) ) )[t/x]) \to ( (\exists y ( (y \in x) \wedge (x \in t) ) )[t/x]) \)（再帰的定義(5)を適用）
＝\( (\forall x ( (t \in x) \vee \neg (y \in t) ) ) \to (\exists y ( ( ( (y \in x) \wedge (x \in t) ) )[t/x]) ) \)（再帰的定義(8)と(7)を適用）
＝\( (\forall x ( (t \in x) \vee \neg (y \in t) ) ) \to (\exists y ( ( ( (y \in x)[t/x]) \wedge ( (x \in t)[t/x] ) ) ) ) \)（再帰的定義(3)を適用）
＝\( (\forall x ( (t \in x) \vee \neg (y \in t) ) ) \to (\exists y ( (y \in t) \wedge (t \in t) ) ) \)（再帰的定義(1)を適用）

こうして定義された代入という概念を用いると、閉論理式というものは論理式\( \Phi \)であっていかなる変項\( x \)と項\( t \)に対しても\( (\Phi)[t/x] \)が\( \Phi \)と文字列として一致するものと言い表せます。



*1 「&mathjax{y};は最初から&mathjax{x};や&mathjax{t};とは違う文字じゃないか」と思うかもしれませんが、この&mathjax{y};は変項記号を表すメタな変数で、変項の文字そのものを表しているわけではありません。公理的集合論に現れる項全体の集まり&mathjax{T};に&mathjax{x};や&mathjax{t};という文字が属しているわけですが、ここでの&mathjax{y};は&mathjax{T};の要素を動く変数であって、&mathjax{T};に属する&mathjax{y};という文字そのものではありません。
*2 [[Encyclopedia of &mathjax{P};-adic Numbers>FrontPage]]では公理的集合論しか考えていないため項&mathjax{t};は変項しかありませんでしたが、一般の論理においては関数記号を用いて表される項も存在し、その場合は(8)と(9)をもう少し複雑に場合分けする必要があります。