数理科学と日本古代史のブログ

　さて、量化記号 ∀ と ∃ に関する推論規則を推論図の形にまとめてみましょう。

　（∀導入）　　　　（∀消去）

　　　P(x)　　　　　　∀xP(x)
　 -----------x　　　-----------
　　∀xP(x)　　　　　　P(T)


　（∃導入）　　 （∃消去）

　　　　　　　　　　∃xP(x)
　　 P(T)　　　　　P(x)├ R
　 -----------　　------------x
　　∃xP(x)　　　　　 R


　ただし （∀導入） で横棒の右に x と書いてあるのは、x が自由変数であることを意味し、（∃消去） のそれは、x が 下段の命題 R に含まれない自由変数であることを意味します。

　これらについても、命題論理のところで導入した局所整合性と局所完全性が成り立ちます。

　実際、（∀消去） の上段の ∀xP(x) のところを （∀導入） の上段、すなわち P(x) で置き換え、更に導入規則の制約条件であった「x は自由変数である」という条件を付けると

　　 P(x)
　 --------x
　　 P(T)

となりますが、これは、x が自由変数であることを用いると、論理記号に無関係な推論規則である （代入） を変数 x と項 T に対して適用すれば導出できる推論図です。

　また、（∃消去） の上段の ∃xP(x) のところを （∃導入） の上段、すなわち P(T) で置き換え、制約条件はそのまま残すと

　　　　P(T)
　　 P(x)├ R
　　------------x
　　　　　R

となりますが、上段の２番目の式において、x が R に含まれない自由変数であることを用いて推論規則 （代入） を変数 x と T に適用すると、P(x)├ R から P(T)├ R
が得られるので、今度は上段の最初の式 P(T) とこの P(T)├ R に対してこれまた論理記号に無関係な推論規則 （カット） を用いることにより、上記の推論図の下段である R が得られます。

　以上で、∀ についても ∃ についても局所整合性が成り立っていることがわかりました。

　次に局所完全性ですが、これは、それぞれの導入規則を ∀' と ∃' に対する導入規則に置き換えたもの、すなわち

　（∀'導入）　　　 （∀消去）

　　　P(x)　　　　　　∀xP(x)
　 -----------x　　　-----------
　　∀'xP(x)　　　　　 P(T)


　（∃'導入）　　（∃消去）

　　　　　　　　　　∃xP(x)
　　 P(T)　　　　　P(x)├ R
　 -----------　　------------x
　　∃'xP(x)　　　　　R

を用いて ∀xP(x) から ∀'P(x) が導けることと、∃xP(x) から ∃'P(x) が導けることを示せばよいのですが、これは簡単です。

　実際、∀xP(x) から、（∀消去） を、T として特に任意に選んだ自由変数 x という項の場合について適用すれば P(x) が得られ、x が自由変数であることに注意すれば、（∀'導入） により ∀'xP(x) が得られます。

　また、∃xP(x) が成り立つとき、∃'xP(x) という命題に含まれない自由変数 x に対して P(x) を仮定すると、x も項ですから、（∃'導入） により ∃'xP(x) が得られ、これは x を含みませんから、（∃消去） で R に ∃'xP(x) を代入したものの上段が得られます。よってその下段、すなわち ∃'xP(x) が得られます。

　以上で、量化記号 ∀ と ∃ についても、局所整合性と局所完全性が成り立つことがわかりました。

　さて、この量化記号の推論規則ですが、ちょっと意味論的に考えると奇妙な結果が導かれてしまうことに注意しておきます。

　それは、自由変数 x を任意に選ぶと、x も項には違いありませんから、∀xP(x) を仮定すると、（∀消去） により P(x) が得られます。ところが、今度は （∃導入） を用いると、x も項であることから ∃xP(x) が得られます。
　従って、（⇒導入） により

　∀xP(x) ⇒ ∃xP(x)

が純粋に論理的に導かれてしまいます。
　これは言葉で表現すると、「すべての x について P(x) が成り立てば、P(x) を満たす x が存在する」ということになりますが、これはとても奇妙です。
　なぜなら P(x) を満たす x が存在するかどうかを論じているのに、すべての x について P(x) が成り立つことを証明すればいいって、そりゃないでしょう。もし対象領域そのものが空だったら「すべての x に対して P(x) が成り立つ」は自明に成り立ってしまうにもかかわらず、P(x) を満たす x は存在しないんだから変じゃないか、というわけです。

　我々は、意味論を無視しているので、これは奇妙ではない、ととぼけることはできるかもしれませんが、しかし ∀ や ∃ を形式化の原理で定義したとき、形式化する前は、∀ は「すべての」という趣旨で、∃ は「存在する」という趣旨で定義したのですから、その趣旨に一見反した結果が出てきたのはやはり奇妙に見えます。
　しかし、この乖離は、そもそも変数という概念を導入したときに実は生じていたのです。その詳細は、後で ε量化記号というものを導入する際、同様な問題が発生するので、そのとき解説することにします。

　本日はここまで。