不完全性定理、その最短の証明

スマリヤン先生の『ゲーデルの不完全性定理』という本に、第一不完全性定理の証明とタルスキの真理述語の定義不可能性定理が極めて一般的かつ明瞭かつ簡潔に説明されていて感動したのでメモを残します。

natの世界とUの世界: nat型である自然数の世界と、U型である記号列の世界があり、U→natな全単射な写像$g$が存在することを要請します¹。記号列の世界に $\mathcal S$ と呼ばれる集合、および$\mathcal P, \mathcal T$という2つの$\mathcal S$の部分集合の存在を要請します。$\mathcal S$の要素を文、$\mathcal P$の要素を証明可能な文、$\mathcal T$の要素を真な文と呼称します。健全性のため$\mathcal P$が $\mathcal T$の部分集合であることを要請します。なお、$g$で作られた数をゲーデル数と呼称します。

述語と名前: U×nat→Uな写像$\Phi$の存在を要請します。「$H$が述語である」を「任意の数nにおいて $\Phi(H,n) \in \mathcal S$」で定義します²。以降 $\Phi(H,n)$を $H(n)$ と略記します。さて、Set nat型の$A$ に対してある述語$H$が存在して $n \in A ⇔ H(n) \in\mathcal T$ を満たす時、$A$は名を持つと定義し、$H$を$A$の名前と呼称します。

対角化関数とその逆像: 述語$H$に対して $H(g(H))$ なる文を作る操作を対角化といいます。これを踏まえ対角化関数$d(n)$を$g(g^{-1}(n) (n))$で定義します。そして Set nat型の$A$に対しSet nat型の$A^*$を対角化関数の逆像で定義します。つまり任意の数$n$に対し $n∈A^*⇔d(n)∈A$ で定義します。

定理GT（不完全性定理）: $P$を$g(\mathcal P)$、補集合を$A^{c}$ のように表記すると「$P^{c*}$が名を持つなら真だが証明可能でない文が存在します」（証明）名前を$H$、そのゲーデル数を$h$とおくと、名前の定義から「$h∈P^{c*}⇔H(h)∈\mathcal T$」この左辺は*の定義よりさらに同値変形できて「$h∈P^{c*}⇔d(h)∈P^c⇔d(h)∉P⇔H(h)\not\in\mathcal P$」となります。よって「$H(h)$が真である」⇔「$H(h)$は証明可能でない」。これは「$H(h)$が真かつ証明可能でない」もしくは「$H(h)$が偽かつ証明可能である」のどちらかのケースだと示しますが、後者のケースは健全性から排除されるので結局$H(h)$が真であるが証明可能でないことが示せます（証明終）

定理GTの3つの前提: 定理GTの前提「$P^{c*}$が名を持つ」は以下の3つの前提から直ちに従います。

• $G_1$: 任意の$A$について$A$が名を持つなら$A^*$も名を持つ
• $G_2$: 任意の$A$について$A$が名を持つなら$A^c$も名を持つ
• $G_3$: $P$は名を持つ

具体的な理論においてGTの前提が成立するかはこれらを満たすかを調べます³。

ゲーデル文と真理述語: Set nat型の$A$に対してそのゲーデル文$G$を「$G∈\mathcal T ⇔ g(G)∈A$」を満たす文として定義します。$A^*$が$H$という名を持つなら$H(g(H))$が$A$のゲーデル文になることは簡単に示せます。さて、$g(\mathcal T)$を$T$と定義し、$A$として$T^{c*}$を考えてみます。名を持つと仮定した場合$T^c$のゲーデル文が存在することになりますが、$T$の定義よりそれはあり得ないので、$T^{c*}$は名を持てないとわかります。

定理T（タルスキの定理）:「$G_1$,$G_2$の前提下で$T$は名を持てない」（証明）前述のように$T^{c*}$は名を持てません。よって$G_1$の対偶より$T^c$も名を持てず、$G_2$の対偶より$T$も名を持てないことが分かります（証明終）

---

1. 記号列の他に数の存在や数概念を措定している、ということではありません。算術や集合論でやるように記号列の集合として数に相当する部分（＝数項の集合）を構成しうるからです。 ↩

2. Φがあまりに抽象的なので例を挙げます。記号列$H$, 数$n$ に対して、$∀ x(x=\bar n ⊃H)$ という記号列を作る操作は、$H$がill-formedであっても純統語的な操作として定義できます。$H$ が（いわゆる算術の言語における）xを自由変数に持つ1項述語である場合にはこの操作で文ができるので、この操作はΦの一例です。その際$H(n)$は $H$に$\bar n$を代入した文と意味論的同値になるのでΦの非形式的な説明「$H$ に $n$ を代入する」という説明を正当化します。 ↩

3. 算術の言語での例を記載します。$A$の定義式を$Ψ(x)$とおくと $A^c$の定義式は $¬Ψ(x)$、$A^*$の定義式は対角化関数の定義式を$D$とおくと $∀y(D(x,y)⊃Ψ(y))$、$P$は算術における可証性述語です。よって算術においては$G_1,G_2,G_3$はすべて満たせます。 ↩