数学の作り方 How to make Mathematics

第13章 ゲーデルの不完全性定理

数学は、自分の全てを証明できるか

ヒルベルトは20世紀初頭、壮大な夢を描きました。すべての数学を有限の公理から機械的に導ける完全な体系にまとめ、 その無矛盾性を体系内部で証明する——数学に絶対の基礎を与える計画です。1931年、25歳のゲーデルはこの夢を打ち砕きました。

十分に強く無矛盾などんな(帰納的に公理化された)体系にも、真だが証明できない命題が存在する(第一不完全性定理)。 そしてそのような体系は、自分自身の無矛盾性を証明できない(第二不完全性定理)。前章の停止性問題と同じ 「自己言及+否定」を、算術の内部で実行するのが証明の核心です。証明を数に符号化し(算術化)、「この文は証明できない」 という自己言及文を算術の中で組み立てる——この章はその全行程を、対角線補題を軸に丁寧に追います。

十分強い無矛盾な体系には決定不能命題があり(第一)、自分の無矛盾性を証明できない(第二)。核は算術内部での自己言及。

舞台設定

定義 対象となる理論

言語 {0,S,+,,<}\{0,S,+,\cdot,<\} 上の算術の理論 TT を考える。TT は次を満たすとする: (i)帰納的公理化:公理の集合が決定可能(機械的に「公理かどうか」判定できる)。 (ii)無矛盾。(iii)ロビンソン算術 QQ(あるいはペアノ算術 PA\mathrm{PA})を含む——基本的な算術ができるだけの強さ。

条件(i)が効きます。「証明かどうかを機械的にチェックできる」——これが次の「証明を数として扱える」を可能にします。 なお、TT が算術の全真理を含む必要はありません。QQ 程度の弱い算術で十分——弱い体系でも不完全性を免れないのがミソです。

算術化(ゲーデル数)

証明論の対象(記号・論理式・証明)は、しょせん有限の記号列です。ならば数で名前をつけられる

定義 ゲーデル数

各記号に番号を割り当て、記号列 s0s1sks_0s_1\cdots s_k を例えば 2s0+13s1+1pksk+12^{s_0+1}\cdot 3^{s_1+1}\cdots p_k^{s_k+1}pip_i は素数)で符号化する。 論理式 φ\varphi の符号をゲーデル数 φ\ulcorner\varphi\urcorner と書く。証明(論理式の列)も同様に数に符号化できる。

素因数分解の一意性のおかげで、数から元の記号列が復元できます。決定的なのは次です。

補題 証明関係は決定可能

関係 ProofT(p,n)\mathrm{Proof}_T(p,n):「pp は、ゲーデル数 nn の論理式の TT における証明のゲーデル数である」は決定可能(原始帰納的)。

なぜなら、pp を復元して「各行が公理か・TT の公理か((i) で判定可能)・前の行からの推論か」を機械的にチェックできるから。 「証明を検算する」のは(見つけるのと違い)機械的にできる——この非対称が不完全性を生みます。

表現可能性

決定可能な関係が、TT内部の論理式で語れることを保証するのが表現可能性定理です。これが算術化を「体系の中」へ持ち込みます。

定理 表現可能性定理

決定可能な(帰納的な)関係 RNkR\subseteq\mathbb N^k に対し、TT の論理式 ρ(x1,,xk)\rho(x_1,\dots,x_k) が存在して、任意の aˉ\bar a について R(aˉ) が真  Tρ(a1,,ak),R(aˉ) が偽  T¬ρ(aˉ).R(\bar a)\ \text{が真}\ \Rightarrow\ T\vdash\rho(\underline{a_1},\dots,\underline{a_k}),\qquad R(\bar a)\ \text{が偽}\ \Rightarrow\ T\vdash\lnot\rho(\underline{\bar a}).a\underline a は数 aa を表す項 SSS0SS\cdots S0QQ でも成り立つ。)

つまり「本当に成り立つ算術的事実は、体系が証明できる」(Σ1\Sigma_1-完全性の一種)。とくに ProofT\mathrm{Proof}_T は決定可能なので、 それを表現する論理式 ProofT(x,y)\mathrm{Proof}_T(x,y)TT の中にあります。これを使って証明可能性述語を作ります。

定義 証明可能性述語

ProvT(y):xProofT(x,y)(「ゲーデル数 y の文は T で証明可能」を表す論理式).\mathrm{Prov}_T(y):\equiv \exists x\,\mathrm{Proof}_T(x,y)\qquad(\text{「ゲーデル数 } y \text{ の文は } T \text{ で証明可能」を表す論理式}).

これで「φ\varphi は証明可能」というメタな主張が、TT の中の文 ProvT(φ)\mathrm{Prov}_T(\ulcorner\varphi\urcorner) として表せます。 体系が自分の証明可能性を語れるようになった——自己言及の準備が整いました。

対角線補題(不動点補題)

不完全性の心臓部。任意の性質について、「自分がその性質をもつ」と主張する文を作れるという驚くべき補題です。

定理 対角線補題(不動点補題)

1変数の任意の論理式 ψ(x)\psi(x) に対し、ある文 GG が存在して TGψ(G).T\vdash G\leftrightarrow \psi(\ulcorner G\urcorner).GG は「私は性質 ψ\psi をもつ」と言う自己言及文。)

証明

論理式の対角化を考える。1変数論理式 θ(x)\theta(x) に対し、その xx に自分自身のゲーデル数を代入した文の ゲーデル数を返す操作 diag(θ)=θ(θ)\mathrm{diag}(\ulcorner\theta\urcorner)=\ulcorner\theta(\ulcorner\theta\urcorner)\urcorner は、記号列の機械的な操作なので計算可能。 表現可能性定理より、diag\mathrm{diag} を表現する論理式 Diag(x,y)\mathrm{Diag}(x,y)(「y=diag(x)y=\mathrm{diag}(x)」を表す)がある。

いま論理式 θ(x):y(Diag(x,y)ψ(y))\theta(x):\equiv \exists y\,\big(\mathrm{Diag}(x,y)\land\psi(y)\big) を作り、その自分自身への対角化 G:θ(θ)G:\equiv \theta(\ulcorner\theta\urcorner) とおく。定義より G=diag(θ)\ulcorner G\urcorner=\mathrm{diag}(\ulcorner\theta\urcorner)TT の中で計算すると、Diag(θ,y)\mathrm{Diag}(\ulcorner\theta\urcorner,y) は 「y=Gy=\ulcorner G\urcorner」と同値に導けるので、 TGy(Diag(θ,y)ψ(y))ψ(G).T\vdash G\leftrightarrow \exists y(\mathrm{Diag}(\ulcorner\theta\urcorner,y)\land\psi(y))\leftrightarrow \psi(\ulcorner G\urcorner).

θ\theta を自分自身に適用する」——前章の D(D)D(\langle D\rangle)、第1章のカントール対角線と、まったく同じ自己適用です。 これで任意の ψ\psi について自己言及文が作れる。とりわけ ψ\psi に「証明できない」を入れると、決定的な文が生まれます。

第一不完全性定理

定義 ゲーデル文

対角線補題を ψ(x):¬ProvT(x)\psi(x):\equiv\lnot\mathrm{Prov}_T(x) に適用して得た文 GG。すなわち TG¬ProvT(G).T\vdash G\leftrightarrow \lnot\mathrm{Prov}_T(\ulcorner G\urcorner). GG は「私は TT で証明できない」と主張する。

定理 第一不完全性定理

TT が(i)(ii)(iii) を満たすとする。(a)TT が無矛盾なら T⊬GT\not\vdash G。(b)TTω\omega-無矛盾なら T⊬¬GT\not\vdash\lnot G。 よって GGTT決定不能(独立)。しかも GG は標準モデル N\mathbb N

証明

(a) TGT\vdash G と仮定する。すると実際に GG の証明 pp が存在し、ProofT(p,G)\mathrm{Proof}_T(p,\ulcorner G\urcorner) が真。表現可能性より TProofT(p,G)T\vdash\mathrm{Proof}_T(\underline p,\ulcorner G\urcorner)、ゆえに TProvT(G)T\vdash\mathrm{Prov}_T(\ulcorner G\urcorner)。一方、GG の定義から TG¬ProvT(G)T\vdash G\to\lnot\mathrm{Prov}_T(\ulcorner G\urcorner)TGT\vdash G と MP で T¬ProvT(G)T\vdash\lnot\mathrm{Prov}_T(\ulcorner G\urcorner)。 これで TTProvT(G)\mathrm{Prov}_T(\ulcorner G\urcorner) とその否定を証明し、矛盾。無矛盾性に反するので T⊬GT\not\vdash G

(b) T¬GT\vdash\lnot G と仮定する。GG の定義より TProvT(G)T\vdash\mathrm{Prov}_T(\ulcorner G\urcorner)、すなわち TxProofT(x,G)T\vdash\exists x\,\mathrm{Proof}_T(x,\ulcorner G\urcorner)。ところが (a) より T⊬GT\not\vdash G、つまり GG の証明は実際には存在しないので、 各具体的な nn について ProofT(n,G)\mathrm{Proof}_T(n,\ulcorner G\urcorner) は偽、表現可能性より T¬ProofT(n,G)T\vdash\lnot\mathrm{Proof}_T(\underline n,\ulcorner G\urcorner)すべての nn で成り立つ。TxProofT(x,G)T\vdash\exists x\,\mathrm{Proof}_T(x,\ulcorner G\urcorner) かつ全ての n\underline nT¬ProofT(n,)T\vdash\lnot\mathrm{Proof}_T(\underline n,\dots)——これは ω\omega-無矛盾性の否定にほかならない。ω\omega-無矛盾ゆえ T⊬¬GT\not\vdash\lnot G

真理:(a) より GG は証明不能。GG は「GG は証明不能」と言っているので、GG の主張は事実として正しい。 すなわち NG\mathbb N\models GGG は真だが TT で証明できない。∎

注意 ロスサーの改良と ω-無矛盾性

(b) だけ ω\omega-無矛盾性(「xϕ(x)\exists x\,\phi(x) を証明するなら、ある n\underline nϕ(n)\phi(\underline n) が偽とはならない」)という 無矛盾性より強い仮定を使った。ロスサーの改良:証明可能性述語を工夫した文(「私の証明より短い反証がある」型)を使うと、 単なる無矛盾性だけで (a)(b) 両方が言え、ω\omega-無矛盾性は不要になる。以後は「無矛盾なら不完全」と述べてよい。

不完全性の一般形

QQ を含む帰納的公理化された無矛盾な理論 TT不完全(決定できない文がある)。TTGG を公理として足しても、 新しい理論に対する別のゲーデル文が現れ、完全にはできない。真な算術命題全体 Th(N)\mathrm{Th}(\mathbb N) は帰納的に公理化できない。

第二不完全性定理

TT は自分の無矛盾性を証明できない」。第一定理の証明を、TT内部で形式化するのが鍵です。

定義 無矛盾性言明と導出可能性条件

Con(T):¬ProvT(0=1)\mathrm{Con}(T):\equiv\lnot\mathrm{Prov}_T(\ulcorner 0=1\urcorner)(「矛盾は証明できない」)。証明可能性述語は次の 導出可能性条件(ヒルベルト–ベルナイス–レープ)を満たす: (D1)TφTProvT(φ)T\vdash\varphi\Rightarrow T\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)、 (D2)TProvT(φψ)(ProvT(φ)ProvT(ψ))T\vdash\mathrm{Prov}_T(\ulcorner\varphi\to\psi\urcorner)\to(\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_T(\ulcorner\psi\urcorner))、 (D3)TProvT(φ)ProvT(ProvT(φ))T\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_T(\ulcorner\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\urcorner)

定理 第二不完全性定理

TTPA\mathrm{PA} 以上の強さ、帰納的公理化、無矛盾)は自身の無矛盾性を証明できない:T⊬Con(T)T\not\vdash\mathrm{Con}(T)

証明

第一定理 (a) の証明「TT が無矛盾なら GG は証明不能」は、G¬ProvT(G)G\leftrightarrow\lnot\mathrm{Prov}_T(\ulcorner G\urcorner) と 導出可能性条件だけを使う議論なので、そっくり TT の内部で再現できる。その形式化が TCon(T)¬ProvT(G),T\vdash \mathrm{Con}(T)\to\lnot\mathrm{Prov}_T(\ulcorner G\urcorner), そして ¬ProvT(G)\lnot\mathrm{Prov}_T(\ulcorner G\urcorner)GG と同値だったから TCon(T)G.T\vdash\mathrm{Con}(T)\to G. ここで仮に TCon(T)T\vdash\mathrm{Con}(T) なら、MP で TGT\vdash G。だが第一定理 (a) より(TT 無矛盾)T⊬GT\not\vdash G。矛盾。 ゆえに T⊬Con(T)T\not\vdash\mathrm{Con}(T)。∎

驚くほど短い——第一定理さえ形式化できれば、第二定理は数行です。含意は深刻です。TT が無矛盾なら、TT\lceil自分は無矛盾\rfloorを証明できない」TT が自分の無矛盾性を証明したら、それは TT矛盾している証拠になる。 ヒルベルトの「体系内部で無矛盾性を証明する」夢は、原理的に不可能だったのです。関連してタルシキの真理定義不能性—— 「真である」を表す算術の論理式は存在しない(もしあれば対角線補題で「私は偽」という文が作れ嘘つきのパラドックスになる)——も 同じ対角線補題から出ます。証明可能性(算術化できる)と真理(できない)の差が、不完全性の源泉です。

ゲンツェンの無矛盾性証明

第二定理は「PA\mathrm{PA} 内部では PA\mathrm{PA} の無矛盾性を証明できない」と言うだけで、外から証明する道を閉ざしません。 ゲンツェン(1936)は、PA\mathrm{PA} の外の原理をただ一つ——順序数 ε0\varepsilon_0 までの超限帰納法——借りて、PA\mathrm{PA} の無矛盾性を証明しました。

定理 ゲンツェンの無矛盾性証明

PA\mathrm{PA} の各証明に順序数 <ε0<\varepsilon_0 を割り当て、カット除去的な変形で証明を単純化するたびに その順序数が真に減少するように仕組む。ε0\varepsilon_0 未満に無限降下列は無い(ε0\varepsilon_0 までの超限帰納法)ので、 矛盾の証明(空シークエントの証明)へ至る変形は停止し、0=10=1 の証明は存在しえない。ゆえに PA\mathrm{PA} は無矛盾。

ここで ε0=sup{ω, ωω, ωωω,}\varepsilon_0=\sup\{\omega,\ \omega^\omega,\ \omega^{\omega^\omega},\dots\}ω\omega の“塔”の極限で、ωε0=ε0\omega^{\varepsilon_0}=\varepsilon_0 を満たす最小の順序数。 PA\mathrm{PA}ε0\varepsilon_0 未満の各順序数までの超限帰納法は証明できるが、ε0\varepsilon_0 までのそれは証明できない (できれば第二定理に反する)。この ε0\varepsilon_0PA\mathrm{PA}証明論的順序数——体系の“強さ”を測る目盛りです (第16章の逆数学と響き合う)。第9章のカット除去が、ここで算術の無矛盾性証明の技術的エンジンとして結実しています。

つまずきポイント

注意 よくある誤解

  • 「証明できない=偽」ではない。 ゲーデル文 GGTT で証明できないが(標準モデルで)。証明可能性と真理は別。GG を足しても、また別の決定不能文が現れる。
  • 不完全性は「数学が間違っている」ではない。 「十分強い体系は、真理をすべては枚挙できない」という限界の主張。個々の数学は健在。
  • 第二定理は「無矛盾性を絶対に証明できない」ではない。 TT 内部では不可能というだけ。ゲンツェンのように、より強い(ε0\varepsilon_0 帰納法を持つ)原理を借りれば外から証明できる。
  • 完全性定理(第7章)と矛盾しない。 完全性は「妥当な論理式は導ける」(論理について)、不完全性は「算術には決定できない文がある」(特定の理論について)。対象が違う。

この章のまとめ

  • 算術化(ゲーデル数)で証明・論理式を数に符号化。証明関係は決定可能で、表現可能性定理により TT 内部の論理式 ProvT\mathrm{Prov}_T で語れる。
  • 対角線補題(自己適用の対角線化)が「私は ψ\psi をもつ」という自己言及文を生む。ψ=¬ProvT\psi=\lnot\mathrm{Prov}_T でゲーデル文 GG「私は証明できない」を作る。
  • 第一不完全性定理:無矛盾(ロスサーで十分)な帰納的公理化理論 TQT\supseteq Q には決定不能文があり、GG は真だが証明不能。第二不完全性定理:導出可能性条件から TCon(T)GT\vdash\mathrm{Con}(T)\to G、ゆえに T⊬Con(T)T\not\vdash\mathrm{Con}(T)——自分の無矛盾性を証明できない。
  • ゲンツェンε0\varepsilon_0 までの超限帰納法を借りて PA\mathrm{PA} の無矛盾性を外から証明。ε0\varepsilon_0PA\mathrm{PA} の証明論的順序数で、カット除去が技術的核心。

論理と計算の限界を見ました。次章から公理的集合論——数学全体の土台 ZFC と、順序数・基数へ進みます。