Gödelの不完全性定理

同義語：ゲーデルの不完全性定理不完全性定理Gödel's incompleteness theoremsGödel's incompleteness theoremincompleteness theorems

概要

前提知識: 一階述語論理, 計算可能関数, 決定可能な理論, 無矛盾性

自然数の正しい命題をすべて証明できる公理系を、機械的に確かめられる形で書き下せるか。Gödel の不完全性定理はこれに否定的に答える。第1不完全性定理は、足し算と掛け算についてのごく弱い公理系 $\mathsf Q$ を含み、公理の集合が決定可能で、無矛盾な理論には、その文も否定も証明できない文があることを主張する。第2不完全性定理は、そのような理論が適当な条件のもとで自分の無矛盾性を表す文を証明できないことを主張する。
鍵になるのは、論理式や証明に自然数の番号（Gödel 数）を付けると「$x$ は $y$ の証明の番号である」という関係が計算可能になり、計算可能な関係は算術の論理式で表現できる、という観察である。こうして「この文は証明できない」と語る文が作れる。

設定

算術の言語を $L_A=\{0,S,+,\cdot,<\}$ とし、その標準的な構造を $\mathfrak N=(\mathbb N,0,S,+,\cdot,<)$（$S$ は $n\mapsto n+1$）とする。$n\in\mathbb N$ の数項 $\underline n$ は $S$ を $n$ 個並べた項 $S\cdots S0$ であり、その値はどの割り当てでも $n$ である（Tarskiの真理定義の記事の節「真理の定義不可能性」と同じ約束）。
$L_A$ の文の集合を理論とよび、$T\vdash\sigma$ は $T$ から $\sigma$ が一階述語論理で導出できることを表す。Gödelの完全性定理により、$T\vdash\sigma$ で $\mathcal M$ が $T$ のモデルなら $\mathcal M\models\sigma$ である（健全性）。無矛盾 は無矛盾性の記事の定義「無矛盾性」による。$T\vdash\sigma$ と $T\vdash\lnot\sigma$ のどちらも成り立たない文 $\sigma$ を、$T$ から独立な文という。
Gödel 数 を 1 つ固定し、論理式 $\varphi$ の Gödel 数を $\#\varphi$、その数項を $\ulcorner\varphi\urcorner:=\underline{\#\varphi}$ と書く。文の集合が 決定可能 であるとは、Gödel 数の集合が計算可能（計算可能関数の記事の定義「計算可能関数」の 3）であることをいう。$\operatorname{Cn}(T):=\{\sigma\mid T\vdash\sigma\}$ が決定可能なとき $T$ は決定可能であるといい（決定可能な理論の記事の定義「決定可能な理論」）、$T$ 自身が決定可能な文の集合であるとき、$T$ は 決定可能な公理系 であるという。「アルゴリズムで判定できる」を「計算可能」と読み替えてよいことは Church–Turingのテーゼの記事の節「テーゼの主張」による。

Robinson の算術と Peano 算術

次の 8 個の文からなる理論を Robinson の算術 $\mathsf Q$ という。

$\forall x\forall y\,(Sx=Sy\to x=y)$
$\forall x\,\lnot(0=Sx)$
$\forall x\,(\lnot x=0\to\exists y\,x=Sy)$
$\forall x\,(x+0=x)$
$\forall x\forall y\,(x+Sy=S(x+y))$
$\forall x\,(x\cdot0=0)$
$\forall x\forall y\,(x\cdot Sy=x\cdot y+x)$
$\forall x\forall y\,\bigl(x< y\leftrightarrow\exists z\,(Sz+x=y)\bigr)$
$\mathsf Q$ に、すべての論理式 $\varphi(x,\vec u)$ についての帰納法の公理 $\forall\vec u\,\bigl(\bigl(\varphi(0,\vec u)\land\forall x\,(\varphi(x,\vec u)\to\varphi(Sx,\vec u))\bigr)\to\forall x\,\varphi(x,\vec u)\bigr)$ を加えた理論を Peano 算術 $\mathsf{PA}$ という。理論 $T$ が $\mathsf Q$ の 8 個の公理をすべて導出するとき、$T$ は $\mathsf Q$ を含む という。

$\mathsf Q$ と $\mathsf{PA}$ の公理はどちらも $\mathfrak N$ で真なので（8 は「$x < y$ と、ある $z$ で $(z+1)+x=y$ となることは同値」という主張）、$\mathfrak N$ は両者のモデルである。帰納法の公理の形かどうかは記号列を調べれば判定できるので、$\mathsf{PA}$ の公理の集合は決定可能である。

表現可能性

関係 $R\subset\mathbb N^k$ が $\mathsf Q$ で 表現可能 であるとは、自由変数が $x_1,\dots,x_k$ の中にある論理式 $\varphi(x_1,\dots,x_k)$ があって、すべての $\vec n=(n_1,\dots,n_k)$ について、$R(\vec n)$ なら $\mathsf Q\vdash\varphi(\underline{n_1},\dots,\underline{n_k})$、$R(\vec n)$ でないなら $\mathsf Q\vdash\lnot\varphi(\underline{n_1},\dots,\underline{n_k})$ となることをいう。
関数 $f\colon\mathbb N^k\to\mathbb N$ が $\mathsf Q$ で表現可能であるとは、論理式 $\varphi(x_1,\dots,x_k,y)$ があって、すべての $\vec n$ について $\mathsf Q\vdash\varphi(\underline{\vec n},\underline{f(\vec n)})$ かつ $\mathsf Q\vdash\forall y\,\bigl(\varphi(\underline{\vec n},y)\to y=\underline{f(\vec n)}\bigr)$ となることをいう。

対角化関数 $d\colon\mathbb N\to\mathbb N$ を、$n=\#\theta$ で $\theta$ の自由変数が $x$ だけ（またはない）のとき $d(n):=\#\theta(\underline n)$、それ以外のとき $d(n):=0$ と定める。$\theta(\underline n)$ は $\theta$ の $x$ に数項 $\underline n$ を代入した文で、$d(\#\theta)$ は $\theta$ に自分自身の Gödel 数を入れた文の Gödel 数である。決定可能な公理系 $T$ について、関係 $\mathrm{Prf}_T\subset\mathbb N^2$ を「$m$ は $T$ からの導出の Gödel 数で、その最後の論理式の Gödel 数が $n$」で定める。

この記事では証明しない事実

次の 3 つを使う。

計算可能な関数・関係はすべて $\mathsf Q$ で表現可能である（OLT26 Theorem 35.2（p. 553）、Theorem 35.29（p. 567）。逆も成り立つ）。
対角化関数 $d$ は計算可能である（OLT26 §37.2、p. 582）。
$T$ が決定可能な公理系なら $\mathrm{Prf}_T$ は計算可能である（公理の集合が原始再帰的な場合が OLT26 Proposition 34.28（p. 549）、決定可能な場合の言明は同書 §37.3（pp. 583–584））。
1 の要点は有限列を符号化する Gödel の $\beta$ 関数にある（OLT26 §35.3、p. 555）。

対角化補題

自由変数が $y$ だけの任意の論理式 $\psi(y)$ に対して、文 $\sigma$ で
$$ \mathsf Q\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner) $$
を満たすものがある。

自分の Gödel 数を入れた文を作る

rem-git-facts の 1・2 により、$d$ は論理式 $D(x,y)$ で $\mathsf Q$ で表現される。すなわち、すべての $n$ について
$$ \mathsf Q\vdash D(\underline n,\underline{d(n)}),\qquad \mathsf Q\vdash\forall y\,\bigl(D(\underline n,y)\to y=\underline{d(n)}\bigr) $$
である。$\theta(x):=\exists y\,\bigl(D(x,y)\land\psi(y)\bigr)$ とおくと、$\theta$ の自由変数は $x$ だけである。$n:=\#\theta$、$\sigma:=\theta(\underline n)=\exists y\,\bigl(D(\underline n,y)\land\psi(y)\bigr)$ とおくと、$d$ の定義により $d(n)=\#\sigma$、すなわち $\underline{d(n)}=\ulcorner\sigma\urcorner$ である。
あとは $\mathsf Q$ の中で $\sigma$ と $\psi(\ulcorner\sigma\urcorner)$ が同値であることを、表現の 2 式で $y$ を $\ulcorner\sigma\urcorner$ に取り替えて確かめればよい。

詳しい推論を開く

$\sigma$ を仮定すると、ある $y$ で $D(\underline n,y)$ と $\psi(y)$ が成り立つ。表現の第 2 式から $y=\ulcorner\sigma\urcorner$ なので、等号の性質により $\psi(\ulcorner\sigma\urcorner)$ が成り立つ。逆に $\psi(\ulcorner\sigma\urcorner)$ を仮定すると、表現の第 1 式 $D(\underline n,\ulcorner\sigma\urcorner)$ と合わせて、$y:=\ulcorner\sigma\urcorner$ が $D(\underline n,y)\land\psi(y)$ を満たすので $\sigma$ が成り立つ。以上は一階述語論理の推論と $\mathsf Q$ で導出できる 2 式だけを使っているので、$\mathsf Q\vdash\sigma\leftrightarrow\psi(\ulcorner\sigma\urcorner)$ である。 $\square$

$\sigma$ は「私は性質 $\psi$ をもつ」と自分について語る文である。$\mathfrak N$ での充足に置き換えた同じ構成が Tarskiの真理定義の記事の補題「対角化補題（意味論の形）」であり、$\psi$ を「真でない」にとると Tarski の定理、「証明できない」にとると以下の定理になる。同じ補題は OLT26 Lemma 37.2（p. 583）、集合論 ZF の中での形は Kun80 Chapter I, Theorem 14.2（p. 40）にある。

証明できることを算術の文で表す

以下、$T$ を決定可能な公理系とする。rem-git-facts の 1・3 により、$\mathrm{Prf}_T$ を $\mathsf Q$ で表現する論理式 $\mathrm{Pr}_T(x,y)$ がある。これを 1 つ選んで
$$ \mathrm{Prov}_T(y):=\exists x\,\mathrm{Pr}_T(x,y) $$
とおく。$\mathrm{Prov}_T(\ulcorner\varphi\urcorner)$ は「$\varphi$ は $T$ から導出できる」と読める文で、この読みが正しいことが次の補題の 2 である。

証明可能性の表現

$T$ を決定可能な公理系、$\varphi$ を論理式とする。

$T\vdash\varphi$ なら $\mathsf Q\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)$ である。
すべての $m,n$ について、$\mathfrak N\models\mathrm{Pr}_T[m,n]\iff\mathrm{Prf}_T(m,n)$ である。とくに $\mathfrak N\models\mathrm{Prov}_T[\#\varphi]\iff T\vdash\varphi$ である。

1：導出の番号 $m$ について $\mathsf Q\vdash\mathrm{Pr}_T(\underline m,\ulcorner\varphi\urcorner)$ となることから従う。

詳しい証明を開く

$T\vdash\varphi$ なら $\varphi$ の導出があり、その Gödel 数を $m$ とすると $\mathrm{Prf}_T(m,\#\varphi)$ が成り立つ。表現の定義により $\mathsf Q\vdash\mathrm{Pr}_T(\underline m,\ulcorner\varphi\urcorner)$ であり、存在記号の導入により $\mathsf Q\vdash\exists x\,\mathrm{Pr}_T(x,\ulcorner\varphi\urcorner)$ である。

2：要点は、$\mathsf Q$ で導出できることは健全性により $\mathfrak N$ で真なので、表現の定義の 2 つの場合がそのまま $\mathfrak N$ での真偽になることである。

詳しい証明を開く

$\mathrm{Prf}_T(m,n)$ なら $\mathsf Q\vdash\mathrm{Pr}_T(\underline m,\underline n)$ であり、$\mathfrak N$ は $\mathsf Q$ のモデルなので健全性により $\mathfrak N\models\mathrm{Pr}_T(\underline m,\underline n)$ である。数項の値は $m,n$ なので、一階述語論理の記事の補題「代入補題」により $\mathfrak N\models\mathrm{Pr}_T[m,n]$ である。$\mathrm{Prf}_T(m,n)$ でないなら、同じ議論を $\mathsf Q\vdash\lnot\mathrm{Pr}_T(\underline m,\underline n)$ に使って $\mathfrak N\not\models\mathrm{Pr}_T[m,n]$ を得る。後半は、$\mathfrak N\models\mathrm{Prov}_T[\#\varphi]$ が「ある $m\in\mathbb N$ で $\mathfrak N\models\mathrm{Pr}_T[m,\#\varphi]$」と同値であることから従う。 $\square$

第1不完全性定理

まず、公理系の形を問わず次が成り立つ。

Q を含む無矛盾な理論の決定不能性

$T$ が $\mathsf Q$ を含む無矛盾な理論なら、$\operatorname{Cn}(T)$ は決定可能でない。

「私は定理でない」という文

$\operatorname{Cn}(T)$ が決定可能だとすると、その Gödel 数の集合は計算可能な関係なので、rem-git-facts の 1 により、論理式 $\theta(y)$ で、すべての文 $\tau$ について
$$ T\vdash\tau\implies\mathsf Q\vdash\theta(\ulcorner\tau\urcorner),\qquad T\not\vdash\tau\implies\mathsf Q\vdash\lnot\theta(\ulcorner\tau\urcorner) $$
となるものがある。lem-git-diagonal を $\psi:=\lnot\theta$ に使い、$\mathsf Q\vdash\sigma\leftrightarrow\lnot\theta(\ulcorner\sigma\urcorner)$ となる文 $\sigma$ をとる。$T$ は $\mathsf Q$ を含むので、$\mathsf Q$ から導出できる文は $T$ からも導出できる。
$T\vdash\sigma$ とすると $\mathsf Q\vdash\theta(\ulcorner\sigma\urcorner)$ なので $\mathsf Q\vdash\lnot\sigma$、よって $T\vdash\lnot\sigma$ となり、$T$ の無矛盾性に反する。$T\not\vdash\sigma$ とすると $\mathsf Q\vdash\lnot\theta(\ulcorner\sigma\urcorner)$ なので $\mathsf Q\vdash\sigma$、よって $T\vdash\sigma$ となり、仮定に反する。どちらも起こりえないので、$\operatorname{Cn}(T)$ は決定可能でない。$\square$

$T=\mathsf Q$ とすれば $\mathsf Q$ 自身が決定不能である（決定可能な理論の記事の系「算術の言語の妥当な文」で使われている事実。OLT26 Theorem 36.5、p. 575）。

第1不完全性定理

$T$ を $\mathsf Q$ を含む無矛盾な理論とし、$T$ は決定可能な公理系であるとする。このとき $T$ から独立な文がある。すなわち、文 $\sigma$ で $T\not\vdash\sigma$ かつ $T\not\vdash\lnot\sigma$ となるものがある。

独立な文がないとすると、どの文 $\sigma$ についても $T\vdash\sigma$ または $T\vdash\lnot\sigma$ である。$T$ は無矛盾なので Gödelの完全性定理によりモデルをもち、したがって完全な理論の記事の定義「完全な理論」の意味で完全である。$T$ は決定可能な文の集合なので、同じ記事の定理「決定可能な公理系をもつ完全な理論は決定可能」により $\operatorname{Cn}(T)$ は決定可能になる。これは thm-git-undecidable に反する。$\square$

$T$ が決定可能な理論の記事の意味で公理化可能なら、決定可能な公理の集合に定理を使って同じ結論を得る。この証明は独立な文を具体的に示さない。Gödel が実際に作った文については次のことがいえる。

ω無矛盾

理論 $T$ が ω無矛盾 であるとは、自由変数が $x$ だけの論理式 $\varphi(x)$ で、$T\vdash\exists x\,\varphi(x)$ であり、かつすべての $m\in\mathbb N$ について $T\vdash\lnot\varphi(\underline m)$ となるものが存在しないことをいう。

ω無矛盾なら無矛盾である。$\mathfrak N$ をモデルにもつ理論は、健全性により ω無矛盾である。

Gödel 文の性質

$T$ を $\mathsf Q$ を含む無矛盾な決定可能な公理系とし、lem-git-diagonal を $\psi:=\lnot\mathrm{Prov}_T$ に使って
$$ \mathsf Q\vdash G_T\leftrightarrow\lnot\mathrm{Prov}_T(\ulcorner G_T\urcorner) $$
となる文 $G_T$（Gödel 文）をとる。このとき次が成り立つ。

$T\not\vdash G_T$。
$\mathfrak N\models G_T$。
$T$ が ω無矛盾なら $T\not\vdash\lnot G_T$。とくに $\mathfrak N$ が $T$ のモデルなら $G_T$ は $T$ から独立である。

1：$T\vdash G_T$ とすると、lem-git-provability の 1 により $\mathsf Q\vdash\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ である。$G_T$ の性質から $\mathsf Q\vdash\lnot G_T$ となり、$T\vdash\lnot G_T$ と $T\vdash G_T$ が $T$ の無矛盾性に反する。
2：$\mathfrak N$ は $\mathsf Q$ のモデルなので、健全性により $\mathfrak N\models G_T\leftrightarrow\lnot\mathrm{Prov}_T(\ulcorner G_T\urcorner)$ である。1 と lem-git-provability の 2 により $\mathfrak N\not\models\mathrm{Prov}_T[\#G_T]$ なので、$\mathfrak N\models G_T$ である。
3：要点は、$\lnot G_T$ が「証明がある」と主張するのに、各 $m$ が証明でないことは $T$ が個別に証明してしまうことである。

詳しい証明を開く

$T\vdash\lnot G_T$ とすると、$G_T$ の性質から $T\vdash\mathrm{Prov}_T(\ulcorner G_T\urcorner)$、すなわち $T\vdash\exists x\,\mathrm{Pr}_T(x,\ulcorner G_T\urcorner)$ である。一方 1 により $G_T$ の導出はないので、すべての $m$ で $\mathrm{Prf}_T(m,\#G_T)$ は成り立たず、表現の定義により $\mathsf Q\vdash\lnot\mathrm{Pr}_T(\underline m,\ulcorner G_T\urcorner)$、したがって $T\vdash\lnot\mathrm{Pr}_T(\underline m,\ulcorner G_T\urcorner)$ である。これは $T$ の ω無矛盾性に反する。後半は、$\mathfrak N$ をモデルにもつ理論が ω無矛盾であることと 1 による。 $\square$

$G_T$ は「私は $T$ から証明できない」と述べ、2 はそれが実際に正しいことをいう。3 の形は OLT26 Theorem 37.6（p. 585）にある。ω無矛盾を無矛盾に弱めても独立な文を具体的に作れることは Rosser による（同書 Theorem 37.7、p. 585。この記事では証明しない）。

算術への帰結

$\mathsf{PA}$ には独立な文があり、$G_{\mathsf{PA}}$ は $\mathfrak N$ で真だが $\mathsf{PA}$ から独立である。
真の算術 $\operatorname{Th}(\mathfrak N)$ は公理化可能でない。すなわち、決定可能な文の集合 $A$ で $\operatorname{Cn}(A)=\operatorname{Th}(\mathfrak N)$ となるものはない。

1：$\mathsf{PA}$ は $\mathsf Q$ を含み、公理の集合は決定可能で、$\mathfrak N$ をモデルにもつ。thm-git-goedel-sentence の 2・3 による。
2：要点は、$\operatorname{Th}(\mathfrak N)$ にはどの文か否定かが属すので独立な文がないことである。

詳しい証明を開く

そのような $A$ があったとする。$\operatorname{Cn}(A)=\operatorname{Th}(\mathfrak N)$ は $\mathsf Q$ の公理を含み、$\mathfrak N$ をモデルにもつので無矛盾である。thm-git-first により $A$ から独立な文 $\sigma$ がある。しかし $\mathfrak N\models\sigma$ か $\mathfrak N\models\lnot\sigma$ のどちらかが成り立つので、$\sigma$ か $\lnot\sigma$ が $\operatorname{Th}(\mathfrak N)=\operatorname{Cn}(A)$ に属し、矛盾する。$\square$

2 は決定可能な理論の記事の系「真の算術は公理化可能でない」と同じ主張である。$G_{\mathsf{PA}}$ を公理に加えても、新しい理論の Gödel 文がまた独立になる。

例：弱い算術から独立な具体的な文

「$x=Sx$ となる $x$ はない」という文

文 $\tau:=\forall x\,\lnot(x=Sx)$ は $\mathsf Q$ から独立だが、$\mathsf{PA}$ からは導出できる。
$\mathsf Q\not\vdash\lnot\tau$． $\tau$ は $\mathfrak N$ で真で、$\mathfrak N$ は $\mathsf Q$ のモデルなので、健全性による。
$\mathsf Q\not\vdash\tau$． $\mathbb N$ に $S\infty=\infty$ となる元 $\infty$ を 1 つ付け加えた $\mathsf Q$ のモデル $M$ を作れば、$M\not\models\tau$ なので健全性により $\mathsf Q\not\vdash\tau$ である。

モデルの作り方と確かめを開く

$\tau$ が偽になる $\mathsf Q$ のモデルを作る。台集合を $M:=\mathbb N\cup\{\infty\}$ とし、$\mathbb N$ の上では通常どおり、$\infty$ については$$S\infty:=\infty,\quad a+\infty:=\infty+a:=\infty,\quad \infty\cdot0:=0,\quad 0\cdot\infty:=0,\quad a\cdot\infty:=\infty\ (a\ne0),\quad \infty\cdot b:=\infty\ (b\ne0)$$（$a,b\in M$）と定め、$<^M$ は公理 8 の右辺で定める。公理 1〜7 を $\infty$ が現れる場合について確かめる。1：$S$ は $\mathbb N$ 上で単射で、$S\infty=\infty$ はどの $n+1$ とも異なる。2：$S$ の値は $0$ にならない。3：$\infty=S\infty$。4：$\infty+0=\infty$。5：$y=\infty$ なら両辺とも $\infty$、$x=\infty$ なら $\infty+Sy=\infty=S(\infty+y)$。6：$\infty\cdot0=0$。7：$y=\infty$ のとき左辺は $x\cdot\infty$、右辺は $x\cdot\infty+x$ で、$x=0$ なら両辺 $0$、$x\ne0$ なら両辺 $\infty$。$x=\infty$、$y=m\in\mathbb N$ のとき左辺は $\infty$、右辺は $\infty\cdot m+\infty=\infty$。よって $M$ は $\mathsf Q$ のモデルで、$M\models\infty=S\infty$ だから $M\not\models\tau$ である。健全性により $\mathsf Q\not\vdash\tau$ である。

$\mathsf{PA}\vdash\tau$． $\varphi(x):=\lnot(x=Sx)$ についての帰納法を使う。$\varphi(0)$ は公理 2 の実例である。$\varphi(x)$ を仮定し $Sx=SSx$ とすると、公理 1 により $x=Sx$ となって矛盾するので $\varphi(Sx)$ が成り立つ。帰納法の公理により $\forall x\,\varphi(x)$ である。

$\mathsf Q$ は和の可換性も証明できない（OLT26 §35.1、p. 553）。$\mathsf{PA}$ でも独立な文があることを保証するのが第1不完全性定理である。

第2不完全性定理

$0=S0$ を $\bot$ と書き、
$$ \mathrm{Con}_T:=\lnot\mathrm{Prov}_T(\ulcorner\bot\urcorner) $$
とおく。$T$ が $\mathsf Q$ を含めば $T\vdash\lnot\bot$（公理 2）なので、$T$ が無矛盾であることは $T\not\vdash\bot$ と同値であり、lem-git-provability の 2 により $\mathfrak N\models\mathrm{Con}_T$ と同値である。

導出可能性条件

$\mathrm{Prov}_T$ についての次の条件を 導出可能性条件 という（$\varphi,\psi$ は任意の文）。

(D1) $T\vdash\varphi$ なら $T\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)$。
(D2) $T\vdash\mathrm{Prov}_T(\ulcorner\varphi\to\psi\urcorner)\to\bigl(\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_T(\ulcorner\psi\urcorner)\bigr)$。
(D3) $T\vdash\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\to\mathrm{Prov}_T(\ulcorner\mathrm{Prov}_T(\ulcorner\varphi\urcorner)\urcorner)$。

$T$ が $\mathsf Q$ を含めば (D1) は lem-git-provability の 1 から成り立つ。(D3) は (D1) を $T$ の中で証明できるという条件である。

第2不完全性定理

$T$ を $\mathsf Q$ を含む無矛盾な決定可能な公理系とし、$\mathrm{Prov}_T$ が (D2)・(D3) を満たすとする。このとき $T\vdash G_T\leftrightarrow\mathrm{Con}_T$ であり、$T\not\vdash\mathrm{Con}_T$ である。

第1不完全性定理の議論を T の中でたどる

$\mathrm{Prov}_T$ を $P$ と略す。$G:=G_T$ の性質と $T$ が $\mathsf Q$ を含むことから $T\vdash G\to\lnot P(\ulcorner G\urcorner)$ である。命題論理の恒真式 $\lnot A\to(A\to B)$ により
$$ T\vdash G\to\bigl(P(\ulcorner G\urcorner)\to\bot\bigr) $$
である。これに (D1) を使うと $T\vdash P(\ulcorner G\to(P(\ulcorner G\urcorner)\to\bot)\urcorner)$ であり、(D2) を 2 回使うと
$$ T\vdash P(\ulcorner G\urcorner)\to P(\ulcorner P(\ulcorner G\urcorner)\to\bot\urcorner),\qquad T\vdash P(\ulcorner P(\ulcorner G\urcorner)\to\bot\urcorner)\to\bigl(P(\ulcorner P(\ulcorner G\urcorner)\urcorner)\to P(\ulcorner\bot\urcorner)\bigr) $$
を得る。(D3) により $T\vdash P(\ulcorner G\urcorner)\to P(\ulcorner P(\ulcorner G\urcorner)\urcorner)$ なので、3 つを命題論理で合わせて $T\vdash P(\ulcorner G\urcorner)\to P(\ulcorner\bot\urcorner)$ である。対偶をとると $T\vdash\mathrm{Con}_T\to\lnot P(\ulcorner G\urcorner)$ であり、$G$ の性質により $T\vdash\mathrm{Con}_T\to G$ である。
逆向きは (D1)・(D2) だけで示せる。

逆向きの証明を開く

$T\vdash\lnot\bot$ なので $T\vdash\bot\to G$ である。(D1) と (D2) により $T\vdash P(\ulcorner\bot\urcorner)\to P(\ulcorner G\urcorner)$、対偶をとって $T\vdash\lnot P(\ulcorner G\urcorner)\to\mathrm{Con}_T$ であり、$G$ の性質により $T\vdash G\to\mathrm{Con}_T$ である。

最後に、$T\vdash\mathrm{Con}_T$ とすると前半により $T\vdash G$ となり、thm-git-goedel-sentence の 1 に反する。$\square$

証明したことと、この記事では証明しないこと

この記事で証明したのは、(D2)・(D3) を仮定したときの thm-git-second である。具体的な理論で (D2)・(D3) が成り立つことは、この記事では証明しない。

$\mathsf{PA}$． 自然に作った $\mathrm{Prov}_{\mathsf{PA}}$ が (D1)〜(D3) を満たすことは OLT26 §37.6（pp. 587–588）で述べられ（同書でも証明は省かれている）、それによる $\mathsf{PA}\not\vdash\mathrm{Con}_{\mathsf{PA}}$ が Theorem 37.8（p. 588）、上と同じ抽象的な形が Theorem 37.9（p. 589）である。
集合論． 集合論の言語の理論 $T$ が ZF を含む決定可能な公理系で無矛盾なら、集合論の言語で同じように作った無矛盾性の文 $\mathrm{Con}_T$（「$\exists v\,(v\ne v)$ は $T$ から導出できない」と読める文）を $T$ が導出できないことは Kun80 Chapter I, Theorem 14.3（p. 41）にある。そこでも議論の ZF の中での形式化は細部が省かれている。$T=\mathsf{ZFC}$ とすれば、ZFC公理系は無矛盾である限り自分の無矛盾性を証明しない。
第2不完全性定理は $\mathrm{Con}_T$ の書き方に依存する（OLT26 p. 588。反例の表の 4 行目）。

$\mathsf{PA}$ の無矛盾性を $\mathfrak N$ から示す議論（無矛盾性の記事の例「Peano 算術」）は、$\mathsf{PA}$ より強い理論の中で行われる。

反例：条件を外すと成り立たない

外す条件	反例	成り立たなくなること
thm-git-first の「無矛盾」	$L_A$ のすべての文の集合 $T_{\mathrm{all}}$	独立な文があること
thm-git-first の「決定可能な公理系」	真の算術 $\operatorname{Th}(\mathfrak N)$	独立な文があること
thm-git-first の「$\mathsf Q$ を含む」	1 元からなる $L_A$ 構造 $E$ の理論 $\operatorname{Th}(E)$	独立な文があること
thm-git-second の (D2)・(D3)	$\mathrm{Prf}_T$ を表現する別の論理式 $\mathrm{Pr}^\ast_T$ から作る $\mathrm{Con}^\ast_T$	$\mathrm{Con}^\ast_T$ が導出できないこと

反例の確かめ

表の各行が定理のほかの仮定を満たし、結論だけが崩れることを確かめる。

各行の確かめを開く

1 行目：$T_{\mathrm{all}}$ は決定可能な文の集合で、$\mathsf Q$ の公理を含み、どの文 $\sigma$ も $\sigma$ と $\lnot\sigma$ の両方が導出できる。矛盾しているので独立な文はない。

2 行目：$\operatorname{Th}(\mathfrak N)$ は $\mathfrak N$ をモデルにもつので無矛盾で、$\mathsf Q$ の公理を含み、どの文についても文か否定のどちらかを含む。決定可能な公理系でないことは cor-git-arithmetic の 2 による。

3 行目：$E=\{e\}$ とし、$0^E=e$、$S^E(e)=e$、$e+e=e\cdot e=e$、$<^E=\emptyset$ とする。$\operatorname{Th}(E)$ はモデル $E$ をもつので無矛盾で、どの文についても文か否定のどちらかを含み、決定可能な理論の記事の定理「有限構造の理論は決定可能」により決定可能な文の集合である。$E\models0=S0$ なので $\mathsf Q$ の公理 2 は $E$ で偽であり、$\operatorname{Th}(E)$ は $\mathsf Q$ を含まない。

4 行目：$T$ を $\mathsf Q$ を含む無矛盾な決定可能な公理系とし、$z\le x$ を $z< x\lor z=x$ の略記として$$\mathrm{Pr}^\ast_T(x,y):=\mathrm{Pr}_T(x,y)\land\forall z\,\bigl(z\le x\to\lnot\mathrm{Pr}_T(z,\ulcorner\bot\urcorner)\bigr)$$とおき、$\mathrm{Prov}^\ast_T(y):=\exists x\,\mathrm{Pr}^\ast_T(x,y)$、$\mathrm{Con}^\ast_T:=\lnot\mathrm{Prov}^\ast_T(\ulcorner\bot\urcorner)$ とする。

(a) $\mathrm{Pr}^\ast_T$ も $\mathrm{Prf}_T$ を $\mathsf Q$ で表現する。$\mathrm{Prf}_T(m,n)$ でないなら $\mathsf Q\vdash\lnot\mathrm{Pr}_T(\underline m,\underline n)$ なので $\mathsf Q\vdash\lnot\mathrm{Pr}^\ast_T(\underline m,\underline n)$ である。$\mathrm{Prf}_T(m,n)$ なら $\mathsf Q\vdash\mathrm{Pr}_T(\underline m,\underline n)$ である。$T$ は無矛盾なので $\bot$ の導出はなく、各 $k\le m$ で $\mathsf Q\vdash\lnot\mathrm{Pr}_T(\underline k,\ulcorner\bot\urcorner)$ である。$\mathsf Q\vdash\forall z\,\bigl(z\le\underline m\to z=\underline0\lor\cdots\lor z=\underline m\bigr)$（OLT26 Lemma 35.23・35.24、p. 564）と合わせて $\mathsf Q\vdash\forall z\,\bigl(z\le\underline m\to\lnot\mathrm{Pr}_T(z,\ulcorner\bot\urcorner)\bigr)$、よって $\mathsf Q\vdash\mathrm{Pr}^\ast_T(\underline m,\underline n)$ である。

(b) $T\vdash\mathrm{Con}^\ast_T$ である。$\mathrm{Pr}^\ast_T(x,\ulcorner\bot\urcorner)$ を仮定すると、第 1 成分から $\mathrm{Pr}_T(x,\ulcorner\bot\urcorner)$、第 2 成分に $z:=x$（$x=x$ なので $x\le x$）を入れて $\lnot\mathrm{Pr}_T(x,\ulcorner\bot\urcorner)$ が出て矛盾する。この推論は一階述語論理だけで行える。

(a) により $\mathrm{Prov}^\ast_T$ は本文の $\mathrm{Prov}_T$ と同じ作り方の論理式であり、lem-git-provability により (D1) を満たす。(b) と thm-git-second により、$\mathrm{Prov}^\ast_T$ は (D2) か (D3) を満たさない。$\mathfrak N$ で読めば $\mathrm{Pr}^\ast_T$ と $\mathrm{Pr}_T$ は同じ関係を定めるが、$\mathrm{Con}^\ast_T$ は「$T$ の無矛盾性」を $T$ の中で正しく表していない。

補足

定理の位置づけ

完全性定理との違い：Gödelの完全性定理は証明体系の性質であり、不完全性定理は理論の完全性が成り立たないことを述べる。両者は矛盾しない（同記事の節「理論の完全性と不完全性定理」、完全性定理(命題論理) の記事の節「「完全」という語」）。
Tarski の定理との関係：$\mathfrak N$ での真理は $L_A$ の論理式で定義できない（Tarskiの真理定義の記事の定理「Tarski の真理の定義不可能性定理」）が、証明可能性は $\mathrm{Prov}_T$ で定義できる。したがって両者は一致しない。

文献

$\mathsf Q$ は OLT26 Definition 33.5（p. 524）、表現可能性は Definition 35.1（p. 553）・35.28（p. 567）、ω無矛盾は Definition 37.4（p. 584）による。証明の流れは同書 §36.4–36.7（pp. 575–577）と §37.2–37.3・§37.7（pp. 581–589）に沿う。