ブーロス流・第二不完全性定理の証明 [趣味のゲーデル]

ブーロスの『無矛盾性の証明不可能性』を読んでいたら、「『論理、論理、また論理』に第二不完全定理のすっきりした証明（のようなもの）が載ってたよなあ」とふと思い出したので、それを参考にしつつ、逃避がてら「ある形式系が無矛盾であれば、その形式系は自らが無矛盾であることを証明できない」ということを主張するゲーデルの第二不完全性定理の（不完全な）証明（のようなもの）を書き下ろす。ろくすっぽ文献に当たらず、ほんとのほんとに「書き下ろし」であるので、そういうものとして読んでほしい。

まず記法の定義からはじめる。いま、ある形式系を考える。この形式系は、一群の（「正しい」と措定しうる）命題と一群の推論規則を備えているとする。そうした「正しいと措定しうる」一群の命題を「公理 axiom」と呼び、それら公理群をここでは \(\Gamma\) で表す。また推論規則としてはモードゥス・ポネンス、つまり「 \(p\) であり、 \(p \rightarrow q\) であれば、 \(q\) である」を備えているとする（ここで \(\rightarrow\) は、あらっぽく「 \(p\) が成立てば \(q\) も成立つ」とでも解釈しておく）。こうした形式系のことを、ここではとりあえず「理論 theory」と呼ぶ。

さて、上述のような理論において、命題 \(p_1 \ldots p_n\) を、 \(\Gamma\) に属するか、あるいは \(\Gamma\) に属する命題にモードゥス・ポネンスを何回か適用して得られる命題としたとき、 \(p_1 \rightarrow \cdots \rightarrow p_n \rightarrow p\) という列が存在する場合、「 \(p\) は（ある命題群 \(\Gamma\) を前提として）証明できる」と言い、記号 \(\Gamma \vdash p\) で表す。誤解の懼れがないか、あるいはその必要がない場合、 \(\vdash\) 左辺の \(\Gamma\) を省略してたんに \(\vdash p\) などとも書く。また、ある命題 \(p\) が証明可能であることを \(\Box p\) とも表す。

以下をある種の「公理」のようなものとして前提する。

(i) もし \(\vdash p\) であれば、 \(\vdash \Box p\)
(ii) \(\vdash (\Box(p \rightarrow q) \rightarrow (\Box p \rightarrow \Box q))\)
(iii) \((\Box p \rightarrow \Box\Box p)\)

これらを「自然言語」で言いかえるとそれぞれ、

(i) ある命題が証明できるのであれば、「ある命題が証明できる」ということが証明できる
(ii) 「 \(p\) であれば \(q\) 、ということが証明できれば、 \(p\) が証明できれば \(q\) も証明できる、ということが成立つ」ということが証明できる
(iii) 「ある命題が証明できるのであれば、その命題が証明できるということが証明できる」ということが証明できる

となる。また上記の「公理」から、以下が導ける。

(iv) もし \(\vdash (p \rightarrow q)\) であれば、 \(\vdash (\Box p \rightarrow \Box q)\)

ここで、何であれ「正しくない＝偽である」命題を \(\perp\) と表し、これを「矛盾 contradiction」と呼ぶ。ある理論が「無矛盾 consistent」であるとは、その理論では矛盾が証明できないことであり、 \(\not\vdash \perp\) と表せる。これは、証明可能オペレータ \(\Box\) を用いて、 \(\neg \Box \perp\) と書くこともできる。また、任意の命題 \(p\) に関して \((\neg p \rightarrow (p \rightarrow \perp))\) がつねに成立つ（直感的に言えばこれは、「ある命題と、その命題の否定が同時に成立つことはない」ということである）。

さて、[Gödel 1931]によれば、ある理論内において、自身の証明不可能性を主張する命題が存在することが示せる。つまり、

(1) \(\vdash p \leftrightarrow \neg \Box p\)

である（ここで \(p \leftrightarrow q\) は「 \(p \rightarrow q\) かつ \(q \rightarrow p\) 」の略記とし、「 \(p\) と \(q\) は同一視できる」とあらっぽく解釈しておく）。また、 \(p \leftrightarrow q\) は「 \(p \rightarrow q\) かつ \(q \rightarrow p\) 」の略記なのだから、 \(p \leftrightarrow \neg \Box p\) が証明できるのであればとうぜん \(p \rightarrow \neg \Box p\) も証明できる。つまり、

(2) \(\vdash p \rightarrow \neg \Box p\)

ここで、上の(2)に(iv)を適用すると

(3) \(\vdash \Box p \rightarrow \Box \neg \Box p\)

を得る。また、上の \(\perp\) のところで言及した \((\neg p \rightarrow (p \rightarrow \perp))\) の \(p\) を \(\Box p\) と読み替え、それに(iv)を適用すると以下が得られる。

(4) \(\vdash \Box \neg p \rightarrow \Box (\Box p \rightarrow \perp)\)

さらに、(ii)の \(p\) を \(\Box p\) 、 \(q\) を \(\perp\) と読み替え

(5) \(\vdash \Box(\Box p \rightarrow \perp) \rightarrow (\Box\Box p \rightarrow \Box \perp)\)

を得る。(iii)および(3)-(5)により、

(6) \(\vdash \Box p \rightarrow \Box \perp\) 。

これの対偶をとって、

(7) \(\vdash \neg \Box \perp \rightarrow \neg \Box p\) 。

(1)より \(\neg \Box p \rightarrow p\) なのだから、(7)と合わせて

(8) \(\vdash \neg \Box \perp \rightarrow p\) 。

これに(iv)を適用して、

(9) \(\vdash \Box \neg \Box \perp \rightarrow \Box p\) 。

ゆえに、(6)と(9)（の対偶）より以下を得る。

(10) \(\vdash \neg \Box \perp \rightarrow \neg \Box \neg \Box \perp\) 。

これはつまり、ある理論において、「もし \(\neg \Box \perp\) ならば \(\neg \Box \neg \Box \perp\) 」ということである。また、(i)により、「もし \(\neg \Box \perp\) ならば \(\Box \neg \Box \perp\) 」ということも成立たなければならない。しかしながら、上で述べたように、ある命題とその否定が同時に成立つことは矛盾である（＝それら命題とその否定が同時に成立つ理論は矛盾している）。つまり、「ある理論内で、矛盾が証明できない、ということが証明できるなら、矛盾が証明できる（＝その理論は矛盾している）」が成立つ。しかるに、この対偶をとって、「ある理論内で矛盾が証明できない（＝その理論は無矛盾である）のなら、その理論内で矛盾が証明できない、ということは証明できない」ということである。そしてこれが、ゲーデルの第二不完全定理の言うところであった。