ゲーデルの不完全性定理

対角線補題(カントールの対角線論法の形式版)により、算術の中で $F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ を満たす文 $G_F$——$F$ における自分自身の証明不可能性を主張する文——を構成できる。もし $F \vdash G_F$ なら $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ が成り立つので $F \vdash \neg G_F$ となり、無矛盾性に反する。ゆえに $F \nvdash G_F$ であるが、これはまさに $G_F$ が主張していることそのものなので、$G_F$ は $\mathbb{N}$ において真となる。(後にロッサーが $\omega$-無矛盾性の仮定を取り除いた。)

第1段階(構文の算術化)。$F$ の言語のすべての記号、論理式、および論理式の有限列に一意な自然数(そのゲーデル数)を割り当てる、計算可能な符号化方式を固定する。$F$ が実効的に公理化されているため、関係 $\mathrm{Prf}_F(p, n)$ ——「$p$ はコード $n$ を持つ論理式の証明のコードである」—— は $+$、$\times$、量化子のみを使った算術の論理式で表現できる。証明を1行ずつ検査することは有限の機械的手続きだからである。$\mathrm{Prov}_F(n) := \exists p\, \mathrm{Prf}_F(p, n)$ と定義する。

第2段階(対角線補題)。自由変数を1つ持つ任意の算術の論理式 $\psi(x)$ に対して、対角線補題は $F \vdash D \leftrightarrow \psi(\ulcorner D \urcorner)$ を満たす文 $D$ を生成する——$D$ は自分自身のコードについて $\psi(x)$ が成り立つと主張する。これを $\psi(x) := \neg\mathrm{Prov}_F(x)$ に適用すると、$F \vdash G_F \leftrightarrow \neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$ を満たす文 $G_F$ が得られる。直感的には、$G_F$ は「私は $F$ で証明できない」と述べている。

第3段階($F \nvdash G_F$)。背理法により $F \vdash G_F$ と仮定する。$F$ は実効的に公理化されているため、この証明自体がコード $p_0$ を持ち、$\mathrm{Prf}_F(p_0, \ulcorner G_F \urcorner)$ が真となる。したがって $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ である(具体的な数についての証明可能な算術的事実は、それ自体 $F$ で証明可能である)。しかし対角線の同値関係と $F \vdash G_F$ を組み合わせると $F \vdash \neg \mathrm{Prov}_F(\ulcorner G_F \urcorner)$ が得られる。したがって $F$ はある命題とその否定の両方を証明してしまい、無矛盾性に反する。ゆえに $F \nvdash G_F$ である。

第4段階($G_F$ は真であり、$\omega$-無矛盾性を仮定すれば $F \nvdash \neg G_F$ でもある)。$F \nvdash G_F$ なので、$G_F$ の証明を符号化する数は存在せず、$\neg\mathrm{Prov}_F(\ulcorner G_F \urcorner)$ が $\mathbb{N}$ において成り立つ。対角線の同値関係により、これはまさに $G_F$ が主張していることなので、$G_F$ は真である。もし $F$ が $G_F$ の否定、すなわち $F \vdash \neg G_F$ も証明したなら、これと対角線の同値関係を組み合わせて $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner)$——「ある $p$ が $G_F$ の証明を符号化している」——が得られるが、それを裏付ける実際の証明は一つも存在しないことになり、これはまさに $\omega$-無矛盾性が排除する状況である。したがって $\omega$-無矛盾性のもとでは $F \nvdash \neg G_F$ でもあり、$F$ は不完全である。

第一定理の証明——「$F$ が無矛盾ならば、$F$ は $G_F$ を証明しない」——それ自体を $F$ の内部で形式化することができ、$F \vdash \mathrm{Con}(F) \to G_F$ が得られる。もし $F$ が $\mathrm{Con}(F)$ を証明できたとすると、モーダスポネンスにより $F \vdash G_F$ が導かれ、第一定理に矛盾する。

第1段階(証明可能性述語は定義可能なだけでなく形式化可能である)。$\mathrm{Prov}_F$ は機械的に検査可能な関係 $\mathrm{Prf}_F(p,n)$ から構成されているため、次の3つの「導出可能性条件」自体が $F$ の内部で証明可能である(この議論で $F$ が単に無矛盾であるだけでなくペアノ算術を拡張している必要がある理由はここにある):($P_1$) $F$ が $\varphi$ を証明するならば $F$ は $\mathrm{Prov}_F(\ulcorner\varphi\urcorner)$ を証明する;($P_2$) $F$ は $\mathrm{Prov}_F(\ulcorner\varphi\to\psi\urcorner) \to (\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_F(\ulcorner\psi\urcorner))$ を証明する;($P_3$) $F$ は $\mathrm{Prov}_F(\ulcorner\varphi\urcorner) \to \mathrm{Prov}_F(\ulcorner\mathrm{Prov}_F(\ulcorner\varphi\urcorner)\urcorner)$ を証明する。

第2段階(定理1自身の議論を形式化する)。対角線の同値関係により $F \vdash \neg G_F \to \mathrm{Prov}_F(\ulcorner G_F \urcorner)$。定理1の非形式的な議論——「もし $G_F$ が証明可能ならば、その証明自体が $\mathrm{Prov}_F(\ulcorner G_F\urcorner)$ を裏付け、対角線の同値関係によって $\neg G_F$ の証明も手に入ってしまう」——は($P_1$)–($P_3$)でカバーされる記号操作以外は何も使っていないため、$F$ の内部での形式的推論として一歩一歩そのまま再現でき、$F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \mathrm{Prov}_F(\ulcorner \neg G_F \urcorner)$ が得られる。$G_F$ とその否定の両方が証明可能であることから、爆発律(ex falso quodlibet)により $F$ は $0 = 1$ を導けるので、これは $F \vdash \mathrm{Prov}_F(\ulcorner G_F \urcorner) \to \neg\mathrm{Con}(F)$、すなわち $F \vdash \mathrm{Con}(F) \to G_F$ を与える。

第3段階(結論)。背理法により $F \vdash \mathrm{Con}(F)$ と仮定する。$F \vdash \mathrm{Con}(F) \to G_F$ とモーダスポネンスを組み合わせると、$F$ は $G_F$ を証明することになる。しかし定理1により、無矛盾な $F$ について $F \nvdash G_F$ であることがすでに示されている——矛盾である。したがって $F$ は $\mathrm{Con}(F)$ を証明できない。これがまさに主張の内容である。

1929年にゲーデル(博士論文)が証明したこの定理は、一階述語論理の推論規則が完全であり、論理的帰結を一つも取り逃さないことを述べている。不完全性定理(1931年)はこれと矛盾しない:$G_F$ が証明できないのは、意図されたモデル $\mathbb{N}$ では $G_F$ が真であっても、$G_F$ が偽となる超準モデルを $F$ が持つからである。

第1段階(健全性——易しい方向、$T \vdash \varphi$ ならば $T \models \varphi$)。$T$ から $\varphi$ への形式的証明の長さについての帰納法で議論する。$T$ のすべての公理は、定義により $T$ の任意のモデル $M$ で真である;純粋に論理的な公理(例えば $\varphi \to (\psi \to \varphi)$)はすべて妥当であり、いかなる解釈のもとでも真である。そして各推論規則は $M$ における真理を保存する:モーダスポネンスの場合、$M \models \theta$ かつ $M \models \theta \to \varphi$ ならば自動的に $M \models \varphi$ となる。したがって証明のすべての行が $M$ で真であり、特に最後の行である $\varphi$ も真である;$M$ は $T$ の任意のモデルであったから、$T \models \varphi$ が成り立つ。

第2段階(完全性——難しい方向、対偶による:$T \nvdash \varphi$ ならば $T \not\models \varphi$)。$T \nvdash \varphi$ と仮定する。このとき集合 $T \cup \{\neg\varphi\}$ は無矛盾である(もし矛盾を証明してしまうなら、背理法により $T$ が $\varphi$ を証明することになる)。ヘンキンの方法を用いて、これを証人を持つ極大無矛盾集合 $\Sigma$ へと拡張する:$\exists x\, \psi(x)$ が $\Sigma$ に属するときはいつでも、新しい定数 $c$ を追加して $\psi(c)$ も $\Sigma$ に属するようにする。拡張された言語の閉じた項を $\Sigma$ における証明可能な等号で同一視したものを要素とし、関係と関数を $\Sigma$ から直接解釈する項モデル $M_\Sigma$ を構成する。項の長さについての帰納法(「真理の補題」)により、任意の文 $\theta$ について $M_\Sigma \models \theta \iff \theta \in \Sigma$ が成り立つ。

第3段階(モデルの組み立てと結論)。$\neg\varphi \in \Sigma$ なので、真理の補題により $M_\Sigma \models \neg\varphi$ が成り立ち、$T$ のすべての公理が $\Sigma$ に属することから $M_\Sigma \models T$ も成り立つ。したがって $M_\Sigma$ は $\varphi$ が成り立たない $T$ の実際のモデルであり、すなわち $T \not\models \varphi$ である。これにより第2段階の対偶が証明され、第1段階と合わせて、$T \vdash \varphi$ であることと $T \models \varphi$ であることは同値となる——これはゲーデルの1929年の博士論文の結果であり、後にレオン・ヘンキン(1949年)によって、ここで用いた項モデルの構成へと整理された。

仮に $H(P, x)$ が停止性を判定できたとしよう。$H(P, P)$ を実行し、$H$ が「停止する」と答えたら無限ループに入り、$H$ が「ループする」と答えたら停止する機械 $D(P)$ を作る。$D$ に自分自身のコードを与えると、$D(D)$ が停止することと $H(D, D)$ が「ループする」と答えることが同値になり矛盾する。これはゲーデルの対角線文の、計算の側における双子そのものである。

第1段階(停止判定器が存在すると仮定する)。背理法により、コード $P$ を持つプログラムが入力 $x$ で停止するなら「停止する」、そうでなければ「ループする」と、常に停止して正しく答えるアルゴリズム $H$ が存在すると仮定する($H(P, x)$ は常に停止する)。

第2段階($H$ から対角線機械を構成する)。プログラムのコード $P$ を入力とし、まず $H(P, P)$ を計算する新しいアルゴリズム $D(P)$ を定義する——$H$ に $P$ をプログラムと入力の両方として与えて実行する。もし $H(P, P)$ が「停止する」と答えたら、$D$ はわざと無限ループに入る;もし $H(P, P)$ が「ループする」と答えたら、$D$ は(例えば $0$ を返して)直ちに停止する。

第3段階($D$ に自分自身のコードを与える)。$D$ 自体がアルゴリズムなのでコードを持ち、そのコードの上で $D$ を実行することを妨げるものは何もない:$D(D)$ を考える。二つの場合があり、どちらも不可能である:もし $D(D)$ が停止するなら、構成によりこれはちょうど $H(D, D)$ が「ループする」と答えた場合に起こる——つまり $H$ は、$D$ が $D$ 上で停止しないと誤って報告したことになるが、実際にはたった今停止したのである。逆に $D(D)$ が永遠に走り続けるなら、これはちょうど $H(D, D)$ が「停止する」と答えた場合に起こる——つまり $H$ は停止すると誤って報告したことになるが、実際には永遠にループするのである。

第4段階(結論)。いずれの場合も $H$ は入力 $(D, D)$ に対して誤った答えを出してしまい、$H$ が常に正しいという仮定に矛盾する。したがって、そのようなアルゴリズム $H$ は存在しえない:停止問題は決定不能である。