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

　さて、これまでにε量化記号を導入することで、直観主義論理を逸脱してしまうことを示す２つの事例を紹介しました。これらの事実が発見されたのは意外に歴史が浅く、２番目のものは1975年のDiaconescuの発見によるもので、最初のものについては実に1993年のBellの発見によるもののようです。
　さて、これだけの証拠を突きつけられると、排中律は選択公理から一種導出されるもの、と認識されるのも当然のように思えます。

　しかし、もう少し立ち入って考察すると、違った側面が出てきます。今回は、まず２番目のものについて先に分析してみることにします。

　まず、２番目のものというのは、

(1) R(P) と P ⇔ Q から R(Q) が導ける。

という“推論規則”を使って

(2) ∀x(P(x) ⇔ Q(x)) ⇒ εxP(x) = εxQ(x)

という“ε公理”を導いたのでした。
　しかし、今までの、一貫して「形式化の原理」のみによって新しい記号や推論規則を導出してきた方針のもとでは、(1) 自体が実は正当化されないのです。

　(1) は、確かに R が論理記号 ∧ ∨ ⇒ ∀ ∃ や派生的に定義された ¬ ⇔ や等号 = や一般の関数記号（定項を含む）、述語記号、変数のみを使って構成された論理式については成立します。
　実際、直観主義論理においても、論理記号について、

(3a) P を構成要素に持つ命題 A(P) と B(P) が性質 (1) を満たせば、命題 A(P)∧B(P) , A(P)∨B(P) , A(P)⇒B(P) も性質 (1) を満たす。

(3b) P を構成要素に持つ命題 A(P) が性質 (1) を満たせば、命題 ∀xA(P) , ∃xA(P) も性質 (1) を満たす。

という性質が成り立つことがわかります。
　一例として A(P)⇒B(P) の場合を確かめてみます。
　この命題が成り立つとき、P⇔Q を用いて A(Q)⇒B(Q) を導くのですが、そのために A(Q) を仮定すると、A について (1) が成り立つことから A(P) が成り立ち、これと A(P)⇒B(P) に対して (⇒消去) を用いれば B(P) が得られ、今度は B に対して (1) が成り立つことを用いれば B(Q) が成り立つことがわかるので、(⇒導入) によって、確かに A(Q)⇒B(Q) が得られます。
　上記の証明において、論理記号 ⇒ の推論規則が局所完全性を満たすことの証明と本質的に同様な論法が用いられていることに注意してください。以上の結果は、他の論理記号でも同様にして確かめられます。

　従って、(3) を繰り返し用いることにより、論理記号 ∧ ∨ ⇒ ∀ ∃ や派生的に定義された ¬ ⇔ や等号 = や一般の関数記号（定項を含む）、述語記号、変数のみを使って構成された論理式について (1) が成立することがわかります。

　ところが、上記のような論法は、εのような、命題から項を作るような論理記号を含む場合には成立しません。
　つまり、εを含むような論理式については、(1) は一般的に成立しない性質だったのですから、そんなものを形式化して一般的な推論規則などにしてはいけなかったのです。この (1) から (2) を導いたとき、まさに (1) の成立を確かめていない「命題から項を作るような論理記号」εを含む命題に適用してしまったのですから、これは明確な“ルール違反”です。

　それに加えて、今まで「形式化の原理」を発動する際は、必ず新たな記号を追加する際に用いてきたのに、(1) には新たな記号は登場していません。
　つまり、(1) を推論規則として新規に導入しようというのなら、⇔ を

(4) P⇔Q ≡ (P⇒Q)∧(Q⇒P)

によって定義するのではなく、推論規則 (1) によって定義しなければなりません。しかし、そうすると、今度は ⇔ の持つ意味が強くなりすぎて、逆に今度は (4) が成り立たなくなります。

　実際、(1) は、「P⇔P が成り立つ」という推論規則を導入規則に持つような論理記号 ⇔ との間に局所整合性と局所完全性が成り立つような消去規則に他なりません。
　言い換えると、等号のときと同じことで、(1) は「P と Q は記号列として同じものである」場合にしか一般には成り立たないということになり、P と Q が単に同値だというだけでは P⇔Q は成り立たなくなってしまうからです。

　さて、(2) を導いた根拠である (1) 自体の根拠が無かったのですから、当然 (2) も根拠を持たない、ということになり、従ってその (2) を用いた排中律の導出にも根拠がない、ということになり、これで２番目の例に関する問題点は解決しました（なお、ここで“根拠”と呼んだのは、あくまで“「形式化の原理」のみによって新たな概念を追加する”という立場のもとでの“根拠”の意味であり、絶対的な意味で“根拠が無い”と主張したり、ましてや“だからこの (2) を前提にしているBourbakiは根拠が無いのである”などと主張しているわけでは毛頭ありませんので、念のため）。

　ちなみに、(1) を離れて (2) それ自体の正当性を考えた場合でも、(1) と同様な意味で“形式化の原理”を逸脱しています。なぜなら、この推論規則には、新たに追加される記号は含まれておらず、= も ε も、既に別の推論規則によって導入されたものだからです。
　もしも (2) を新規に推論規則に追加したいのであれば、これは等号 = の定義ともみなすべき推論規則ですから、当然 T = T という推論規則に加えて (2) も等号 = の導入規則に追加しなければなりません。
　ところが、このようにして等号の導入規則を増やしてしまうと、今まで等号の消去規則だった

(5) R(S) と S=T から R(T) が導ける。

をそのままにしておくと、局所整合性がもはや成立しなくなってしまいます。

　すなわち、(5) の S に εxP(x) を、T に εxQ(x) を代入し、S=T を ∀x(P(x)⇔Q(x)) に置き換えると、(5) は

(6) R(εxP(x)) と ∀x(P(x)⇔Q(x)) から R(εxQ(x)) が導ける。

に変形されますが、「P(x) を満たす x がただ一つ存在する」というような特別な場合でもない限り、(ε導入) だけを用いて (6) を導くことは一般には不可能です。

　要するに、もしも (2) をどうしても推論規則にしたいのであれば、等号に関する消去規則 (5) もそれ相応に、局所整合性が成立するように弱める必要があるのです。

　以上に見られるように、“形式化の原理”という観点で２番目の問題を考察すると、これは

(7) εを導入して（非構成的な）選択公理が成り立ったから排中律が成立するようになった。

のではなく、

(8) εを導入しただけでなく、形式化の原理を逸脱するような推論規則を導入して等号の推論規則の間に局所整合性が成り立たなくなったから排中律などという余計なモノが証明されてしまった。

ということになります。

　以上のように、２番目の問題は比較的そのポイントが明確に指摘できましたが、最初にあげた問題の方は、少し複雑です。これについては次回に解説したいと思います。