超丁寧に解説するゲーデルの第一不完全性定理

この記事について

この記事は「超丁寧に解説するゲーデルの完全性定理」の姉妹編であり、三部作の中心にあたる。
名前が似ているせいで、完全性定理と不完全性定理はしばしば混同される。「完全なのか不完全なのかどっちなんだ」という感想は、不自然な感想ではない。二つの定理で「完全」という言葉の意味が違うからだ。そこでこの記事は、その混乱を解きほぐすところから始める。完全性定理を知っている人にとっては、そこが一番自然な入口になる。　
三部作の構成は次の通りである。
・ 準備編「超丁寧に解説する$\Sigma_1$完全性と表現定理」 ：算術の体系、$\Sigma_1$完全性、計算可能性、表現定理。不完全性定理のエンジンにあたる部分を、証明つきで用意する。
・前編「超丁寧に解説するゲーデルの第一不完全性定理」（本稿）：Gödel数化、可証性述語、対角化定理、第一不完全性定理、Rosserの改良、そこから派生する決定不能性の結果。
・後編「超丁寧に解説するゲーデルの第二不完全性定理」：導出可能性条件、第二不完全性定理、Löbの定理、その意義。
準備編の結果は「準備編で用意した道具」にまとめてあるので、本稿だけを読んでも筋は追える。証明が気になったところで準備編に戻ればよい。
対象読者は、一階述語論理の構文論と意味論（項、論理式、形式的証明$\vdash$、モデルと充足関係$\models$）を一通り学んだ人である。

完全性定理と不完全性定理

まずここを片付ける。ここを曖昧にしたまま先に進むと、後の議論がすべてぼやける。

「完全」という語が指しているもの

数理論理学で「完全」という語は、二つの違う対象について使われる。

$1$と$2$は、そもそも主語が違う。$1$の主語は証明体系（＝公理と推論規則の集まり）であり、$2$の主語は理論（＝公理として置いた文の集まり）である。同じ「完全」でも、何について語っているのかがまるで違うのだ。

論理の完全性

完全性定理をあらためて述べておく。

左辺は構文論的な正しさである。公理と推論規則だけを使って、$T$から$\varphi$に至る有限の記号列（証明）が存在する。純粋に有限的・機械的な概念であり、（公理が機械的に判定できる限り）原理的にはコンピュータに検証させられる。
右辺は意味論的な正しさである。$T$のすべてのモデルにおいて$\varphi$が真である。「すべてのモデル」という、とてつもなく大きなクラスにわたる量化を含んでいる。
完全性定理は、この二つが一致すると言っている。有限的な道具（推論規則）に取りこぼしがないという主張であり、これは論理の性能についての定理である。

理論の完全性

一方、不完全性定理が扱うのは個々の理論の性質である。始めの方で言った意味で完全でない理論を不完全という。「$T$はすべての問いに白黒をつけられるか」という問いである。これは推論規則の性能ではなく、公理として何を置いたかの話だ。
なお、完全性と決定可能性も別概念である。完全性は「白黒がつく」ことであり、決定可能性は「白黒を機械的に判定できる」ことである。両者の関係は後で確認する。

二つを並べてみる

対比を整理しておく。
・完全性定理は「$\models$ ならば $\vdash$」という橋渡しを主張する。不完全性定理は「$\vdash$の側だけを見たとき、$\varphi$と$\neg\varphi$のどちらにも届かない$\varphi$がある」という欠落を主張する。
・完全性定理は言語や理論の中身にほとんど依存しない。群論でも順序体でも成り立つ。不完全性定理は、理論が算術を十分含んでいることを強く要求する。
・歴史的にも、完全性定理はGödelの1929年の学位論文、不完全性定理は1931年の論文であり、同じ人物が二年の間に証明している。前者が「論理は十分強い」と言い、後者が「しかし公理はいくら足しても足りない」と言っている。この順序で読むと、二つの定理が対立していないことがよく分かる。

なぜ両立するのか

「すべての正しい文が証明できる（完全性定理）のに、証明できない文がある（不完全性定理）とはどういうことか」という疑問が、混乱の中心にある。答えは単純である。
完全性定理が言っているのは
$$ T \models \varphi \Longrightarrow T \vdash \varphi $$
だけである。「$T \models \varphi$か$T \models \neg\varphi$のどちらかである」とは一言も言っていない。 二値性はここでは保証されていないのだ。
もう少し丁寧に言おう。真偽の二値性が成り立つのは個々のモデルの中である。$T$のモデル$\mathfrak{A}$を一つ固定すれば、$\mathfrak{A} \models \varphi$か$\mathfrak{A} \models \neg\varphi$かのどちらかが必ず成り立つ。しかし$T \models \varphi$は「$T$のすべてのモデルで$\varphi$が真」という意味だから、モデルによって意見が割れれば、$T \models \varphi$も$T \models \neg\varphi$も成り立たない。
つまり不完全性が生じているとき、悪いのは論理ではない。論理は与えられた情報から引き出せるものをすべて引き出している（完全性定理）。足りないのは情報のほう、すなわち公理なのである。
そして不完全性定理が言うのは、この「情報不足」が、無矛盾性を保ったまま機械的に判定できる公理をどう足しても解消できない、ということだ。

不完全性は「真偽の食い違うモデルがある」ということ

以上を式にすると、面白い言い換えが得られる。$T$が不完全だとしよう。つまりある文$\sigma$について$T \nvdash \sigma$かつ$T \nvdash \neg\sigma$。ここで完全性定理（の対偶）を使うと、
・$T \nvdash \sigma$より$T \not\models \sigma$、つまり$\sigma$が偽になる$T$のモデルが存在する。
・$T \nvdash \neg\sigma$より$T \not\models \neg\sigma$、つまり$\sigma$が真になる$T$のモデルが存在する。
すなわち、不完全性は「ある文について真偽の食い違う$T$のモデルがある」ことと同じである（逆にそういうモデルがあれば、健全性定理から$T \nvdash \sigma$かつ$T \nvdash \neg\sigma$である）。
単に「モデルが複数ある」のとは違うことに注意しておく。無限モデルを持つ理論は、完全であってもLöwenheim–Skolemの定理によって非同型なモデルを無数に持つ。不完全性が言っているのは、モデルたちが文の真偽について意見が割れるということである。
Peano算術$\mathrm{PA}$で言えば、非標準モデルの存在自体はコンパクト性定理だけから出る（標準モデルで真な文全体を公理にしても、非標準モデルはある）。$\mathrm{PA}$の不完全性から新しく分かるのは、標準モデル$\mathfrak{N}$と真偽の食い違う$\mathrm{PA}$のモデルがある、ということである。
この言い換えは実用的でもある。「$\varphi$は$T$から独立である」ことを示したければ、$\varphi$が成り立つ$T$のモデルと成り立たない$T$のモデルを一つずつ作ればよい（健全性定理）。逆に独立な文があれば、そういうモデルは必ず存在する（完全性定理）。集合論における強制法や、算術における非標準モデルの構成は、まさにこの戦略に乗っている。完全性定理は不完全性定理の敵ではなく、独立性を意味論的な作業に翻訳してくれる道具なのである。この視点は、後で「なぜGödel文の一方向だけ余計な仮定が要るのか」を理解するときにも効いてくる。

何が問題なのか

証明の前に、目的地を見ておく。

定理を先に眺める

文全体の中に「証明できる文」と「反証できる文」の二つの領域があり、その隙間が空になっていない、というのが主張である。$T$が無矛盾であれば二つの領域は交わらず、$T$が完全であれば二つで文全体を覆い尽くす。不完全性定理は、後者が決して起きないと言っている。

三つの条件はどれも外せない

定理の三つの仮定は飾りではない。どれか一つでも落とすと定理は成り立たなくなる。
$1.$ 無矛盾性：矛盾した理論はすべての文を証明する。だから矛盾した理論は完全である。不完全性は無矛盾な理論だけの悩みである。
$2.$ 十分な算術を含むこと：本稿ではこれを、$\mathrm{Q}$を含むこととして定式化する。弱すぎる理論は完全になりうる。実際、掛け算を捨てた算術（Presburger算術）は、計算可能な公理系を持ちながら完全である。「自然数を扱っているから不完全」ではない。足し算と掛け算が同居していることが本質的である。
$3.$ 公理が機械的に判定できること：正確な定義は後に与える。これを落とすと、あからさまな反例がある。標準モデルで真な文全体
$$ \mathrm{TA} = \lbrace \varphi : \mathfrak{N} \models \varphi \rbrace $$
を公理系だと思えば、これは無矛盾で、算術をたっぷり含み、しかも完全である（任意の文について$\varphi$か$\neg\varphi$のどちらかは真だから）。何が悪いのかというと、「与えられた文が$\mathrm{TA}$の公理かどうか」を判定するアルゴリズムが存在しない。それどころか、公理を機械的に列挙することすらできないのである（後に証明する）。公理を機械的に扱えない体系は、形式体系と呼ぶに値しない。

「じゃあ公理を足せばいいのでは？」

一番自然な反論がこれである。$\sigma$が証明も反証もできないなら、$\sigma$を新しい公理として加えた$T + \sigma$を考えればよいのではないか。
答えは「それでは解決しない」である。$T + \sigma$もやはり定理の仮定をそのまま満たすので、また新しい独立な文が出てくる。公理が機械的に扱える限り、いくつ足しても同じことが起きる。不完全性は「たまたま一つ穴が空いている」のではなく、構造的に穴が空き続けるのである。

準備編で用意した道具

ここで準備編の結論をまとめておく。証明はすべて準備編にある。

算術の体系

言語は$\mathcal{L}_A = \lbrace 0, s, +, \cdot \rbrace$で、論理記号は$\neg$, $\to$, $\forall$を基本とする（$\wedge$, $\vee$, $\leftrightarrow$, $\exists$は略記）。$\bot \equiv \neg(0=0)$とする。$\le$は次の略記である。 $$ a \le b \equiv \exists w(w+a=b) $$
自然数$n$に対応する数項を$\overline{n} = s(s(\cdots s(0)\cdots))$（$s$が$n$個）と書く。標準モデルを$\mathfrak{N}$とする。
本稿で使う体系は二つである。帰納法をまったく持たないRobinsonの$\mathrm{Q}$（七個の公理からなる）と、$\mathrm{Q}$に帰納法図式を加えたPeano算術$\mathrm{PA}$（$\mathbf{Q3}$は帰納法から導けるので公理からは省いてある）である。 $\mathrm{Q}$は$0+x=x$のような一般法則すら証明できない（$\mathrm{Q} \nvdash \forall x(0+x=x)$）が、具体的な数についての計算はすべてできる。順序についても、各$n$について次の二つが$\mathrm{Q}$で証明できる（準備編の$\mathbf{R4}$, $\mathbf{R5}$）。
$(\text{O1})$ $\forall x\big(x \le \overline{n} \to (x = \overline{0} \vee \cdots \vee x = \overline{n})\big)$ （$\overline{n}$以下の数の列挙）
$(\text{O2})$ $\forall x(x \le \overline{n} \vee \overline{n} \le x)$ （数項との大小比較）

論理式の階層と$\Sigma_1$完全性

$t = u$と$t \le u$から$\neg$, $\to$と有界量化子$\forall x \le t$, $\exists x \le t$で作られる論理式を$\Delta_0$論理式（$t \le u$は展開せず一つの基本形として扱う）、$\Delta_0$論理式の頭に存在量化子だけを（$0$個以上）付けたものを$\Sigma_1$論理式、全称量化子だけを付けたものを$\Pi_1$論理式という。$\Sigma_1$は「探せば見つかる」性質、$\Pi_1$は「反例がない」性質である。また論理式$\varphi$が$T$上で$\Sigma_1$であるとは、ある$\Sigma_1$論理式$\psi$で$T \vdash \varphi \leftrightarrow \psi$となるものが存在することをいう。

$\Delta_0$文については、真ならば$\mathrm{Q}$で証明でき、偽ならばその否定が証明できる（$\Delta_0$完全性）。$\mathrm{PA}$上で$\Sigma_1$な文についても、真ならば$\mathrm{PA}$で証明できる。一方$\Pi_1$完全性は成り立たない。$\mathrm{Q}$では$\forall x(0+x=x)$が反例であり、帰納法を持つ$\mathrm{PA}$でも、Gödel文と同値な$\Pi_1$文が反例になる。

計算可能性と表現定理

初期関数から合成・原始再帰・最小化で得られる全域関数を再帰的関数（＝計算可能関数）という。述語$P$は、特性関数$P^{\circ}$が計算可能なとき計算可能（決定可能）という。$\Sigma_1$論理式で$\mathfrak{N}$において定義される集合を再帰的可算（r.e.）という。
関数$f$が理論$T$において論理式$\varphi(\vec x,y)$で表現されるとは、任意の$\vec n$について$T \vdash \forall y(y = \overline{f(\vec n)} \leftrightarrow \varphi(\overline{\vec n},y))$が成り立つことをいう。述語$P$が$\varphi(\vec x)$で表現されるとは、$P(\vec n)$が成り立つとき$T \vdash \varphi(\overline{\vec n})$、成り立たないとき$T \vdash \neg\varphi(\overline{\vec n})$となることをいう。

本稿の主役は$(2)$である。対角化定理も、可証性述語も、第一不完全性定理とRosserの定理も、$\mathrm{Q}$での表現可能性だけで動く。$(1)$は、$T$が$\mathrm{PA}$を含む場合の補足と後編で使う。

Gödel数化と可証性述語

アイデア

体系に自分自身のことを語らせたい。しかし算術の体系が語れるのは自然数についてだけである。ならば、記号列を自然数に翻訳してしまえばよい。これがGödel数化のアイデアであり、現代のわれわれからすると文字列のエンコーディングそのものである。

素因数分解による符号化

まず各記号$w$に$1$以上の番号$\sharp w$を割り当てる。たとえば次のようにする。
$$ \begin{eqnarray} \sharp\neg &=& 1 \qquad \sharp{\to} = 2 \qquad \sharp\forall = 3 \\ \sharp( &=& 4 \qquad \sharp) = 5 \qquad \sharp{=} = 6 \\ \sharp 0 &=& 7 \qquad \sharp s = 8 \qquad \sharp{+} = 9 \qquad \sharp{\cdot} = 10 \\ \sharp v_i &=& 11 + i \quad (i \text{ 番目の変数}) \end{eqnarray} $$
論理記号は基本記号の$\neg$, $\to$, $\forall$だけに番号を振ればよい。略記の$\wedge$や$\exists$は、展開してから符号化する。
次に、記号列$w_0 w_1 \cdots w_{n-1}$のGödel数を、$i$番目の素数を$p_i$（$p_0 = 2, p_1 = 3, p_2 = 5, \dots$）として
$$ [w_0 w_1 \cdots w_{n-1}] = p_0^{\sharp w_0} \cdot p_1^{\sharp w_1} \cdots p_{n-1}^{\sharp w_{n-1}} $$
と定める。すべての指数が$1$以上であることに注意（だから記号の番号を$1$から始めた）。
この符号化が使い物になる理由は、素因数分解の一意性である。Gödel数が与えられれば、$2$で何回割れるか、$3$で何回割れるか、と順に調べることで、元の記号列が一意に復元できる。しかも「$x$は$p_i$で何回割れるか」という関数は有界探索で書けるので計算可能である。符号化も復号も計算可能、というのがこの方式の要点だ。
具体例を計算してみよう。論理式$0 = 0$は記号列$0, =, 0$、すなわち番号の列$7, 6, 7$である。よって
$$ [0=0] = 2^7 \cdot 3^6 \cdot 5^7 = 128 \cdot 729 \cdot 78125 = 7290000000 $$
（$2^7 \cdot 5^7 = 10^7$なので計算が楽である。）「論理式が数である」ということが、これで具体的な事実になる。
同じ方法をもう一段使うと、論理式の列も符号化できる。証明とは論理式の有限列だから、列$\varphi_0, \varphi_1, \dots, \varphi_n$に対して
$$ \langle \varphi_0, \varphi_1, \dots, \varphi_n \rangle = p_0^{[\varphi_0]} \cdot p_1^{[\varphi_1]} \cdots p_n^{[\varphi_n]} $$
と定めればよい。素因数分解を二重に使って、記号列を数に、数の列をまた数にするわけである。
記号の番号$\sharp w$、記号列のGödel数$[\cdots]$、列のコード$\langle \cdots \rangle$を書き分けておく。同じ自然数が記号列のGödel数としても列のコードとしても読めることはあるが、どちらとして読むかは文脈で決まる（たとえば後に出てくる$\mathbf{Prov}_T(n,m)$の$n$は列のコードとして読む）。以下、証明（論理式の列）のコードも、慣例に従って証明のGödel数と呼ぶ。
以下、論理式$\varphi$のGödel数（自然数）を$[\varphi]$、それを表す数項を$\ulcorner\varphi\urcorner = \overline{[\varphi]}$と書く。$[\varphi]$はメタレベルの自然数、$\ulcorner\varphi\urcorner$は体系内の項である。

大事なのは符号化そのものではない

符号化の具体的な方式に思い入れを持つ必要はない。素因数分解でも、準備編で使った対関数と$\beta$関数でも、二進表現でも、計算可能に符号化・復号ができれば何でもよい。重要なのは、符号化した後に次のような操作・判定がすべて計算可能になることである。
・与えられた数が項のGödel数か、論理式のGödel数か、文のGödel数かを判定する
・$[\varphi]$から$[\neg\varphi]$を計算する
・$[\varphi(x)]$と$n$から$[\varphi(\overline{n})]$を計算する（代入）
・論理式の列が「推論規則を正しく適用した列」になっているかを判定する
これらはすべて「有限の記号列に対する有限のチェック」なので、原始再帰的である（厳密な確認は退屈だが原理的な困難はない）。

計算可能拡大とr.e.拡大

Gödel数が使えるようになったので、保留にしていた「公理が機械的に判定できる」という条件を定義できる。
理論$T$が与えられたとき、その固有の公理（論理の公理以外の公理）のGödel数を集めた$1$変数述語を考える。
$$ \mathbf{Axiom}_T(n) \iff n \text{ は } T \text{ の固有の公理のGödel数である} $$

$(\text{a})$を「$\mathrm{Q}$の公理を$T$の公理として含む」ではなく「$T$で証明できる」としたのは、$\mathrm{PA}$も$\mathrm{Q}$の計算可能拡大に入れたいからである。$\mathrm{PA}$は$\mathbf{Q3}$を公理としては持たないが、帰納法から証明する。$\mathrm{Q}$を$\mathrm{PA}$に置き換えれば、「$\mathrm{PA}$の計算可能拡大」なども同様に定義される。$\mathrm{PA}$の計算可能拡大は、もちろん$\mathrm{Q}$の計算可能拡大でもある。

可証性述語

いよいよ本題の論理式を定義する。以下、$T$は$\mathrm{Q}$の計算可能拡大とする。
$2$変数述語$\mathbf{Prov}_T$を次のように定める。
$$ \mathbf{Prov}_T(n,m) \iff m \text{は論理式（} \varphi \text{とする）のGödel数であって、} n \text{は} T \text{における} \varphi \text{の証明のGödel数である} $$
この述語が計算可能であるためには、証明の中に現れる各行が「論理の公理か、$T$の公理か、前の行から推論規則で得られたものか」を判定できなければならない。ここで$\mathbf{Axiom}_T$が計算可能であるという条件がまさに必要になる。
$\mathbf{Prov}_T$が計算可能であれば、表現定理$(2)$より、これを$\mathrm{Q}$において表現する論理式が取れる。以下では、関係を太字$\mathbf{Prov}_T$で、それを表現する論理式を立体$\mathrm{Prov}_T$で書き分ける。表現の定義より、任意の$n, m$について
$$ \mathbf{Prov}_T(n,m) \text{が成り立つとき} \mathrm{Q} \vdash \mathrm{Prov}_T(\overline{n},\overline{m}) \qquad \text{成り立たないとき} \mathrm{Q} \vdash \neg\mathrm{Prov}_T(\overline{n},\overline{m}) $$
である。$T$は$\mathrm{Q}$を含むので、これらは$T$でも証明できる。以下で「表現可能性より$T \vdash \cdots$」と書くのは、この意味である。
表現定理$(2)$は論理式の複雑さについて何も言わないので、$\mathrm{Prov}_T$が$\Sigma_1$かどうかは、ここからは分からない。それでも第一不完全性定理には困らない。（$T$が$\mathrm{PA}$を含むなら、表現定理$(1)$を使って$\mathrm{Prov}_T$を$\mathrm{PA}$上で$\Sigma_1$に取ることもできる。その場合の話は後にする。）

文献によってはGödel自身の用語（beweisbar）にちなんで$\mathrm{Bew}_T(x)$と書かれる。

つまり$\mathrm{Pr}_T$は、$T$で証明できる文の集合を、標準モデルの中で正しく切り出している。問題は、$T$自身がこのことをどこまで証明できるかである。

つまり、証明できる文については、「それが証明できる」という事実自体を体系が証明できる。体系は自分の成功については正直に報告できるのだ。

しかし逆は一般に成り立たない。
$$ T \vdash \mathrm{Pr}_T(\ulcorner\varphi\urcorner) \centernot\Longrightarrow T \vdash \varphi $$
$\mathrm{Pr}_T$の$\exists y$は、標準モデルの外側にある非標準の数で満たされているかもしれないからだ。$T$が「$\varphi$の証明が存在する」と証明しても、その証明は無限に長いお化けかもしれない。この非対称性が、第一不完全性定理の証明の非対称性を生む（$T$に$\omega$無矛盾性を仮定すれば逆も成り立つことを、後に見る）。

対角化定理

道具はそろった。あと必要なのは、自分自身について語る文を実際に作る技術である。

なぜこの発想になるのか

出発点は嘘つきのパラドックスである。
$$ \textbf{この文は偽である} $$
これは真とも偽とも決められない。しかし「偽である」は後で見るように算術の中では書けない。そこでGödelは、これを
$$ \textbf{この文は証明できない} $$
に置き換えた。「証明できない」は$\neg\mathrm{Pr}_T$として書ける。だからこの文は算術の言語で書ける。パラドックスは定理に化けるのである。
問題は「この文は」という自己言及をどうやって作るかだ。使うのは対角線論法である。

定理と証明

$\psi$は「私は$\varphi$という性質を持つ」と主張する文である。$\varphi$が何であっても、そう主張する文が作れてしまう。$\psi$は$\varphi$の不動点なので、不動点定理とも呼ばれる。

第一不完全性定理

Gödel文

$T$を$\mathrm{Q}$の計算可能拡大とする。対角化定理を$\varphi(x) \equiv \neg\mathrm{Pr}_T(x)$に適用すると、文$\sigma$が得られて
$$ \mathrm{Q} \vdash \sigma \leftrightarrow \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner) $$
が成り立つ。$T$は$\mathrm{Q}$を含むので、もちろん$T \vdash \sigma \leftrightarrow \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner)$でもある。この$\sigma$を$T$のGödel文という。$\sigma$は「私は$T$で証明できない」と主張している。

健全性と$\omega$無矛盾性

証明の前に、無矛盾性より強い条件を導入しておく必要がある。
もっとも素朴なのは、「$T$が証明する文はすべて$\mathfrak{N}$で真である」という条件、すなわち$\mathfrak{N}$が$T$のモデルであることで、これを$T$が（標準モデルに関して）健全であるという。しかしこれは強すぎる。証明で必要になるのは、「$T$が$\exists x\varphi(x)$を証明しておきながら、どの数$n$についても$\neg\varphi(\overline{n})$を証明する」という事態を禁じることだけである。Gödelが実際に使ったのは、この形の条件である。

$\omega$矛盾は普通の意味での矛盾ではない。標準モデルの外に$\varphi$を満たす「数」がいれば、二つは同時に成り立ちうる。$\omega$矛盾する理論は、標準モデルの解釈が通用しない非標準的な理論である。
条件の強さの関係は次の通りである。
$$ \text{健全} \Longrightarrow \omega\text{無矛盾} \Longrightarrow \text{無矛盾} $$
左の含意：$T$が健全で、しかも$\omega$矛盾していたとする。健全性より$\mathfrak{N} \models \exists x \varphi(x)$なので、ある$n$で$\mathfrak{N} \models \varphi(\overline{n})$である。一方$T \vdash \neg\varphi(\overline{n})$と健全性より$\mathfrak{N} \models \neg\varphi(\overline{n})$でもあり、矛盾する。
右の含意：矛盾した理論はすべての文を証明するので、どの$\varphi(x)$についても二つの条件が成り立ち、$\omega$矛盾する。
いずれの逆も成り立たない（無矛盾だが$\omega$無矛盾でない理論の例は後の注意で挙げる）。なお、$\mathrm{Q}$や$\mathrm{PA}$など普通の算術理論は標準モデル$\mathfrak{N}$を持つので健全であり、したがって$\omega$無矛盾である。

定理と証明

定理の前に、可証性述語の基本性質（補題6）の逆向きを、$\omega$無矛盾性のもとで示しておく。

この証明では、$\mathrm{Prov}_T$がどんな形の論理式であるかを一度も使っていない。使ったのは、$\mathrm{Q}$で成り立つ対角化定理と、可証性述語の基本性質（補題6）と、補題8だけであり、後の二つは$\mathbf{Prov}_T$の$\mathrm{Q}$での表現可能性だけから出る。だから第一不完全性定理は、帰納法をまったく持たない$\mathrm{Q}$を含む理論について成り立つのである。

なぜ片側だけ余計な仮定が要るのか

ここが第一不完全性定理を理解する上で一番大事なポイントである。
・$(\text{a})$の方向では「$T \vdash \sigma$」というメタレベルの事実から出発した。事実があれば、表現可能性がそれを体系内に押し込んでくれる。外から中への翻訳なので、無矛盾性だけで足りる。
・$(\text{b})$の方向では「$T \vdash \mathrm{Pr}_T(\ulcorner\sigma\urcorner)$」という体系内の主張から出発して、メタレベルの事実（実際に証明がある）を引き出したい。これは中から外への翻訳である。だが体系が$\exists y \mathrm{Prov}_T(y, \ulcorner\sigma\urcorner)$を証明したからといって、その$y$が本物の自然数である保証はない。非標準モデルの中にしか存在しない「無限に長い証明」かもしれない。実際、本物の証明がなければ、$T$は表現可能性によって「$\overline{0}$は$\sigma$の証明ではない」「$\overline{1}$は$\sigma$の証明ではない」…と一つずつ証明してしまう。それでもなお「証明はある」と主張するのが、まさに$\omega$矛盾である。だから、この食い違いを禁じる条件（$\omega$無矛盾性）が要る。
可証性述語について言えば、外から中が可証性述語の基本性質（補題6）（無条件）、中から外が補題8（$\omega$無矛盾性が必要）にあたる。この非対称性が、そのまま定理$(\text{a})$と$(\text{b})$の仮定の非対称性になっている。$T$が$\mathrm{PA}$を含む場合には、この対比を$\Sigma_1$完全性と$\Sigma_1$健全性の対比として、もっとはっきり書ける。

Gödel文は「真である」

$T$が無矛盾なら$(\text{a})$より$T \nvdash \sigma$。可証性述語の正しさ（補題5）より$\mathfrak{N} \not\models \mathrm{Pr}_T(\ulcorner\sigma\urcorner)$、すなわち$\mathfrak{N} \models \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner)$。ここで$\mathfrak{N}$は$\mathrm{Q}$のモデルなので、$\mathrm{Q} \vdash \sigma \leftrightarrow \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner)$から$\mathfrak{N} \models \sigma \leftrightarrow \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner)$。（対角化定理が$\mathrm{Q}$で成り立つことが、ここで効いている。$T$が証明する同値式だけでは$\mathfrak{N}$に移せない。$T$が健全とは限らないからである。）よって
$$ \mathfrak{N} \models \sigma $$
$\sigma$は真だが$T$では証明できない。これがしばしば「真だが証明できない文」と呼ばれるものの正体である。

$\mathrm{PA}$を含む場合：$\Sigma_1$健全性

ここまでは$T$が$\mathrm{Q}$を含むことしか仮定しなかった。$T$が$\mathrm{PA}$を含む場合には、可証性述語を$\Sigma_1$に取ることができ、定理$(\text{b})$の仮定を$\omega$無矛盾性より弱い条件に置き換えられる。後編もこの設定で進む。
$T$を$\mathrm{PA}$の計算可能拡大とする。表現定理$(1)$より、$\mathbf{Prov}_T$を$\mathrm{PA}$において表現する$\mathrm{PA}$上で$\Sigma_1$な論理式が取れる。この節では$\mathrm{Prov}_T$をそのように取る。すると$\mathrm{Pr}_T(x) \equiv \exists y \mathrm{Prov}_T(y,x)$も$\mathrm{PA}$上で$\Sigma_1$になる。
これまでの議論は、表現する理論を$\mathrm{Q}$から$\mathrm{PA}$に読み替えればそのまま通る。二つの補題（補題5、補題6）、補題8と第一不完全性定理で使ったのは、「表現する理論が$T$に含まれ、$\mathfrak{N}$をモデルに持つ」ことだけだからである（対角化定理は$\mathrm{Q}$のままでよい）。
$\mathrm{Pr}_T$が$\Sigma_1$になると、補題8は次の条件のもとでも成り立つ。

「$\Sigma_1$健全」は健全性を$\Sigma_1$に制限したもの、「1無矛盾」は無矛盾性を階層の第$1$段まで強めたもの、という見方の違いである。$T$が$\mathrm{PA}$を含むなら、「$\mathrm{PA}$上で$\Sigma_1$な文」にも同じ条件が及ぶ。$T \vdash \varphi$で$\mathrm{PA} \vdash \varphi \leftrightarrow \psi$（$\psi$は$\Sigma_1$）なら、$T \vdash \psi$だから$\mathfrak{N} \models \psi$、そして$\mathfrak{N}$は$\mathrm{PA}$のモデルだから$\mathfrak{N} \models \varphi$となるからである。
$T$が$\mathrm{PA}$を含むとき、条件の強さの関係は次の通りである。
$$ \text{健全} \Longrightarrow \omega\text{無矛盾} \Longrightarrow \Sigma_1\text{健全} (= 1\text{無矛盾}) \Longrightarrow \text{無矛盾} $$
左の含意は前に見た。右の含意は、矛盾した理論が偽な$\Sigma_1$文$0 = s(0)$も証明してしまうことから分かる。いずれの逆も成り立たない。真ん中の含意を確認しておこう。$T$が偽な$\Sigma_1$文$\exists x_1 \cdots \exists x_k \theta$（$\theta$は$\Delta_0$）を証明したとする。$\mathrm{PA}$では、存在量化子のブロックを一つにまとめられる。すなわち
$$ \mathrm{PA} \vdash \exists x_1 \cdots \exists x_k \theta \leftrightarrow \exists u \theta'(u) \qquad \theta'(u) \equiv \exists x_1 \le u \cdots \exists x_k \le u\ \theta $$
であり（右向きは$u = x_1 + \cdots + x_k$と取ればよい）、$\theta'(u)$は$\Delta_0$である。よって$T \vdash \exists u \theta'(u)$。一方、もとの文は偽だから、すべての$n$について$\mathfrak{N} \models \neg\theta'(\overline{n})$であり、$\Delta_0$完全性より$T \vdash \neg\theta'(\overline{n})$。これは$T$が$\omega$矛盾することにほかならない。（ブロックをまとめるところで$\mathrm{PA}$を使っている。$\mathrm{Q}$では、二つの数に共通の上界があることすら証明できない。）

第一不完全性定理$(\text{b})$の証明で、補題8の代わりにこの補題を使い、最後に「$\Sigma_1$健全な理論は無矛盾である」を使えば、次が得られる。

上の含意の連鎖より、これは$T$が$\mathrm{PA}$を含む場合の定理$(\text{b})$の強化になっている。
第一不完全性定理$(\text{a})$と$(\text{b})$の仮定の対比も、こう書くとはっきりする。
$$ \begin{eqnarray} \Sigma_1\text{完全性（外から中）：} && \mathfrak{N} \models \varphi \Longrightarrow T \vdash \varphi \\ \Sigma_1\text{健全性（中から外）：} && T \vdash \varphi \Longrightarrow \mathfrak{N} \models \varphi \end{eqnarray} $$
前者は$\mathrm{Q}$を含む理論なら無条件で成り立つ定理であり、後者は理論に課さなければならない仮定である。$\mathrm{Pr}_T$が$\Sigma_1$なら、可証性述語の基本性質（補題6）は前者から出て（注意の別証明）、補題10は後者から出る。
最後に、予告した$\Pi_1$完全性の反例を確認しておく。$T = \mathrm{PA}$とし、$\sigma$をそのGödel文とする。$\sigma$は$\neg\mathrm{Pr}_{\mathrm{PA}}(\ulcorner\sigma\urcorner)$と$\mathrm{Q}$で同値で、$\mathrm{Pr}_{\mathrm{PA}}$は$\mathrm{PA}$上で$\Sigma_1$なので、$\sigma$と$\mathrm{PA}$で同値な$\Pi_1$文$\pi$が取れる。$\sigma$は真だから$\pi$も真であり、$\mathrm{PA} \vdash \pi$なら$\mathrm{PA} \vdash \sigma$となって第一不完全性定理$(\text{a})$に反する。$\pi$は、$\mathrm{PA}$で証明できない真な$\Pi_1$文である。

Rosserによる改良

動機とアイデア

第一不完全性定理$(\text{b})$は$\omega$無矛盾性を要求する。これは無矛盾性より真に強い条件である。Rosserは、無矛盾性だけで両方向が示せるように議論を改良した。要点は、文ではなく可証性述語を取り替えることにある。
Gödelの証明を、可証性述語の性質という目で見直そう。$(\text{a})$で使ったのは可証性述語の基本性質（補題6）
$$ T \vdash \varphi \Longrightarrow T \vdash \mathrm{Pr}_T(\ulcorner\varphi\urcorner) $$
だった。これは外から中への翻訳なので、無条件に成り立った。
$(\text{b})$では、$T \vdash \neg\sigma$から矛盾を導きたい。$\sigma$の定義から$T \vdash \mathrm{Pr}_T(\ulcorner\sigma\urcorner)$はすぐ出るので、あとは$T \vdash \neg\mathrm{Pr}_T(\ulcorner\sigma\urcorner)$が言えればよい。それには、可証性述語が次の性質を持っていれば十分である。
$$ T \vdash \neg\varphi \Longrightarrow T \vdash \neg\mathrm{Pr}_T(\ulcorner\varphi\urcorner) $$
「反証された文については、証明がないことも$T$の中で言える」という性質である。これも外から中への翻訳なので、成り立つなら無矛盾性だけで済むはずである。
ところが$\mathrm{Pr}_T$については、この性質は表現可能性から出てこない。$\neg\mathrm{Pr}_T(\ulcorner\varphi\urcorner)$は$\forall y \neg\mathrm{Prov}_T(y, \ulcorner\varphi\urcorner)$、すなわち「どの$y$も$\varphi$の証明ではない」という主張である。$\varphi$が反証されていて$T$が無矛盾なら、これは真である。しかし表現可能性が$T$に証明させてくれるのは、$\neg\mathrm{Prov}_T(\overline{n}, \ulcorner\varphi\urcorner)$を一つの$n$ごとに、だけである。無限個の候補を一度に退ける手段がない。Gödelはこの性質の代わりに中から外への翻訳（補題8）を使い、その代償として$\omega$無矛盾性を払ったのだった。
Rosserの考えは、証明関係を少し変えて、退けるべき候補を有限個にすることである。「$y$は$x$の証明である」を
$$ y \textbf{は} x \textbf{の証明であり、しかも} y \textbf{以下に} \neg x \textbf{の証明はない} $$
に取り替える。証明と反証をGödel数の小さい順に並べ、反証より先に現れた証明だけを数えるのである。$T$が無矛盾なら、反証のある文にはそもそも証明がないので、追加した条件は実際には何も削らない。$\mathfrak{N}$で見る限り、可証性述語の意味は変わらない。
変わるのは$T$の中での振る舞いである。$\varphi$が反証されている、つまり$\neg\varphi$の証明が実在するとし、そのGödel数を$n$とする。新しい可証性述語で「$\varphi$は証明可能でない」と言うには、どの$y$も条件
$$ y \textbf{は} \varphi \textbf{の証明であり、しかも} y \textbf{以下に} \neg\varphi \textbf{の証明はない} $$
を満たさないことを示せばよい。どの$y$も、$n$以下か$n$以上かのどちらかである。
・$y \ge n$のとき：$y$以下に$n$があり、$n$は$\neg\varphi$の証明なので、条件の後半が成り立たない。無限個ある$y$が、「$n$は$\neg\varphi$の証明である」という一つの事実でまとめて退けられる。
・$y \le n$のとき：そのような$y$は$0, 1, \dots, n$の有限個しかない。$T$は無矛盾なので$\varphi$の証明は存在せず、どの$y$も条件の前半を満たさない。これは表現可能性で一つずつ$T$に証明させられる。
もとの$\mathrm{Pr}_T$では、条件は「$y$は$\varphi$の証明である」だけなので、$y \ge n$の側をまとめて退ける手段がない。無限個の候補を退ける仕事が、有限の仕事に変わるのが、Rosserの工夫の核心である。

Rosserの可証性述語

$\mathrm{neg}(x)$を「Gödel数$x$の論理式の否定のGödel数」を返す計算可能関数とする（$x$が論理式のGödel数でなければ$0$を返すことにする）。表現定理$(2)$より$\mathrm{neg}$を$\mathrm{Q}$において表現する論理式が取れるので、$u = \mathrm{neg}(x)$はその論理式の略記とする。

$\mathrm{Pr}_T(x) \equiv \exists y \mathrm{Prov}_T(y,x)$との違いは、証人$y$に「$y$以下に$\neg x$の証明がない」という条件を付けたことだけである。$\mathrm{Pr}_T$と同じく、論理式としての複雑さは問わない。
この述語が、上で欲しかった性質を持つ。証明で使うのは、$\mathbf{Prov}_T$と$\mathrm{neg}$の表現可能性と、準備編で用意した道具の$(\text{O1})$, $(\text{O2})$だけである。準備編で最小化を表現したときと同じ二つの性質が、ここでも働く。

$(2)$の証明の$(\text{i})$と$(\text{ii})$は、動機とアイデアで分けた二つの場合（$y \le n$と$y \ge n$）にそのまま対応している。$(1)$は$\mathrm{Pr}_T$の基本性質に対応するが、追加した条件を確かめるために無矛盾性を使っている点が違う。

定理と証明

文として読めば、Rosser文は「私の証明が現れるとしても、それより先に私の否定の証明が現れる」と主張している。

Gödelの証明と並べると、違いは$(\text{b})$で使う性質だけである。
$$ \begin{eqnarray} \text{Gödel（中から外）：} && T \vdash \mathrm{Pr}_T(\ulcorner\varphi\urcorner) \Longrightarrow T \vdash \varphi \\ \text{Rosser（外から中）：} && T \vdash \neg\varphi \Longrightarrow T \vdash \neg\mathrm{Pr}^R_T(\ulcorner\varphi\urcorner) \end{eqnarray} $$
前者には$\omega$無矛盾性という仮定が要ったが、後者は無矛盾性だけで成り立つ。こうして、両方向とも外から中への翻訳で済むようになった。

トレードオフ

Rosser文は仮定が弱くて済む代わりに、失うものもある。Gödel文は「私は証明できない」という透明な意味を持つ。そして後編で見るように、$T$が$\mathrm{PA}$を含み、$\mathrm{Pr}_T$を自然に構成しておけば（後編の設定）、$T$の中で無矛盾性の主張$\mathrm{Con}(T)$と同値になる。つまりGödel文は、「$T$は無矛盾である」という意味のはっきりした主張の言い換えになっている。Rosser文には、この性質は一般には保証されない（標準モデルで真であることは、Gödel文と同じく成り立つ）。仮定を弱めることと、証明が持つ情報量とは、しばしばトレードオフになる。
可証性述語の側から見ると、この違いには理由がある。$T$が無矛盾なら、補題12の$(2)$で$\varphi = \bot$とすると、$\neg\bot$は証明できるので$T \vdash \neg\mathrm{Pr}^R_T(\ulcorner\bot\urcorner)$となる。つまり$\mathrm{Pr}^R_T$で書いた「$T$は無矛盾である」は、$T$自身で証明できてしまう（後編で詳しく説明する）。$T$の中での振る舞いを良くしたことが、そのまま、無矛盾性を表すのに向かない理由になっているのである。

すぐに得られる結果

第一不完全性定理の周辺には、同じ道具立てで証明できる重要な定理がいくつもある。ここでは五つ挙げる。最初の二つは真理について、続く二つは決定可能性について、最後の一つは公理系の取り方についてである。

Tarskiの真理定義不可能性定理

可証性述語は、「$T$で証明できる」という性質を算術の論理式で書いたものだった。同じように、「$\mathfrak{N}$で真である」という性質を論理式で書けるだろうか。
まず、「論理式が真理を表す」とはどういうことかをはっきりさせておく。可証性述語の正しさ（補題5）は
$$ T \vdash \varphi \iff \mathfrak{N} \models \mathrm{Pr}_T(\ulcorner\varphi\urcorner) $$
だった。「$\mathrm{Pr}_T(\ulcorner\varphi\urcorner)$が$\mathfrak{N}$で成り立つのは、$\varphi$が実際に$T$で証明できるとき、かつそのときに限る」という意味であり、$\mathrm{Pr}_T$が「証明できる」を正しく表していることを述べている。この「$T$で証明できる」を「$\mathfrak{N}$で真である」に置き換えると
$$ \mathfrak{N} \models \varphi \iff \mathfrak{N} \models \mathrm{True}(\ulcorner\varphi\urcorner) $$
となる。$\mathrm{True}(\ulcorner\varphi\urcorner)$が$\mathfrak{N}$で成り立つのは、$\varphi$が実際に$\mathfrak{N}$で真であるとき、かつそのときに限る。つまり$\mathrm{True}(x)$は、文のGödel数$x$を受け取って、その文が真かどうかを答える論理式である。任意の文$\varphi$についてこれを満たす論理式$\mathrm{True}(x)$を、真理述語と呼ぶ。
たとえば$\overline{2}+\overline{2}=\overline{4}$は真なので$\mathrm{True}(\ulcorner \overline{2}+\overline{2}=\overline{4} \urcorner)$も真でなければならず、$\overline{0}=\overline{1}$は偽なので$\mathrm{True}(\ulcorner \overline{0}=\overline{1} \urcorner)$も偽でなければならない。なお、$x$が文のGödel数でないときの$\mathrm{True}(x)$の真偽は問わない。
文の範囲を制限すれば、真理述語は実際に書ける。たとえば$\Delta_0$文の真偽は、有界量化子の範囲を一つずつ調べれば有限回の計算で決まるので、真な$\Delta_0$文のGödel数の集合は計算可能である。表現定理$(2)$よりこれを$\mathrm{Q}$で表現する論理式$\tau_0(x)$が取れ、$\mathfrak{N}$は$\mathrm{Q}$のモデルなので、任意の$\Delta_0$文$\varphi$について$\mathfrak{N} \models \varphi \iff \mathfrak{N} \models \tau_0(\ulcorner\varphi\urcorner)$となる。Tarskiの定理が否定するのは、すべての文をまとめて扱う真理述語である。
対角化定理は$\mathrm{Pr}_T$に限らず、任意の論理式に適用できる。これを真理述語に適用すると、次の強烈な結果が出る。

$\mathrm{True}(\ulcorner\psi\urcorner)$は「$\psi$は真である」を表すので、$\psi$は「私は偽である」と主張する文、つまり嘘つき文である。嘘つきパラドックスがそのまま定理になっている。上の$\tau_0$に同じ議論を使っても矛盾は出ない。得られる嘘つき文は$\Delta_0$文ではないので、$\tau_0$の条件がそもそも当てはまらないからである。

真理は決定可能でない

Tarskiの定理は「真理は算術の言語で定義できない」と言っている。ここから、より初等的だが直観に訴える結論が出る。

この定理は、真の算術$\mathrm{TA}$を「公理系として認めるわけにいかない」と述べたことの正確な根拠でもある。$\mathrm{TA}$の固有の公理はすべての真な文だから、$\mathbf{Axiom}_{\mathrm{TA}}$は$\mathbb{T}$そのものであり、計算可能でない。

$\mathrm{Q}$の本質的決定不能性

決定可能性の側に話を移す。次の定理は、第一不完全性定理と同じ対角線の技法で証明でき、しかも公理が計算可能であることを仮定しないという点で注目に値する。

「本質的」というのは、「$\mathrm{Q}$自身だけでなく、$\mathrm{Q}$のどんな無矛盾な拡大も決定可能でない」という意味である。

$A(x) \equiv \neg\delta(x)$は「私に自分の番号を代入した文は$T$で証明できない」と主張する論理式で、Gödel文とほとんど同じ構造をしている。

Churchの定理

$\mathrm{Q}$が有限公理化されていることが、ここで効いている。$\mathrm{PA}$は有限個の公理では公理化できないことが知られているので、この議論は使えない。準備編で弱い体系を用意する理由$2$として挙げたのは、このことである。

Craigの手法

これまで公理が計算可能であることを仮定してきた。証明関係$\mathbf{Prov}_T$を計算可能にするには、公理かどうかを判定できなければならないからである。しかし、これは理論ではなく公理系についての条件である。同じ定理を持つ別の公理系に取り替えてよいなら、条件はr.e.まで弱められる。

証明の前に、何が問題なのかを確認しておく。$\mathbf{Axiom}_T$がr.e.であるとは、$\Delta_0$論理式$\theta(x, w)$によって
$$ [\varphi] \in \mathbf{Axiom}_T \iff \text{ある } m \text{ について } \mathfrak{N} \models \theta(\overline{[\varphi]}, \overline{m}) $$
と書けることである（定義に使う$\Sigma_1$論理式の頭に$\exists$が複数あっても、$\exists w_1 \cdots \exists w_k$を$\exists u \exists w_1 \le u \cdots \exists w_k \le u$と書き直せば一つにまとまる。$\mathfrak{N}$で真偽が一致すればよいので、ここでは$\mathrm{PA}$は要らない）。このような$m$を、$\varphi$が公理であることの証拠と呼ぼう。
与えられた$m$が証拠かどうかは、有限の計算で確かめられる。$\theta$は$\Delta_0$なので、有界量化子の範囲を一つずつ調べれば、$\mathfrak{N} \models \theta(\overline{[\varphi]}, \overline{m})$の真偽が決まるからである。困るのは、証拠がどこにあるか分からないことである。$\varphi$が公理かどうかを知ろうとして$m = 0, 1, 2, \dots$と順に調べても、$\varphi$が公理でなければこの探索は終わらない。r.e.と計算可能の差は、この「終わらないかもしれない探索」にある。
そこでCraigは、証拠を公理そのものに書き込んでおくことを考えた。そうすれば、公理かどうかを判定する側は、書き込まれた証拠を読み取って確かめるだけでよく、探索はいらない。書き込み方は、文の意味を変えないものなら何でもよい。ここでは恒真な等式$\overline{m} = \overline{m}$を書き添える。

証拠は「探すもの」から「書いてあるもの」に変わった。これがCraigの手法の核心である。Craig自身は、$\overline{m} = \overline{m}$を書き添える代わりに、$\varphi$を$m+1$回$\wedge$でつないだ文を使った。繰り返しの回数で証拠を表すので、数項を持たない言語でも使える。
$\mathrm{Q}$を$\mathrm{PA}$に置き換えても、まったく同じ議論が通る。
この定理によって、本稿の結果はr.e.拡大にもそのまま及ぶ。たとえば$T$が無矛盾な$\mathrm{Q}$のr.e.拡大なら、$T'$は無矛盾な$\mathrm{Q}$の計算可能拡大なので、Gödel-Rosserの第一不完全性定理より不完全である。完全かどうかは定理の集合だけで決まるので、$T$も不完全である。

対比：Presburger算術

最後に、「十分な算術を含む」という仮定の意味を実感するための対比を置いておく。
言語から掛け算を取り除いた$\lbrace 0, s, + \rbrace$を考える。$\mathbf{Q1}$, $\mathbf{Q2}$, $\mathbf{Q4}$, $\mathbf{Q5}$に、$\lbrace 0, s, + \rbrace$の論理式についての帰納法図式を加えた体系をPresburger算術という（順序$\le$は$+$で定義できる）。

構造$(\mathbb{N}, 0, s, +)$がモデルなので無矛盾であり、公理系は計算可能である。つまり『三つの条件はどれも外せない』の条件$1$と$3$を満たしたまま完全になっている。完全だから、その定理全体は構造$(\mathbb{N}, 0, s, +)$で真な文全体と一致する。
不完全性は「無限を扱っているから」起きるのではない。自己言及に必要な表現力、つまり計算可能な関数を表現する力は、足し算と掛け算が同居して初めて得られる。 実際、準備編の$\beta$関数$\beta(a,b,i) = \mathrm{rm}(a, (i+1)\cdot b + 1)$には積が現れる。有限列を一つの自然数に押し込む操作が、掛け算なしには書けないのである。

まとめ

$1.$ 完全性定理の「完全」は証明体系について、不完全性定理の「完全」は理論についての語であり、両者は両立する。合わせると「不完全性 = 真偽の食い違うモデルがある」と読める。
$2.$ Gödel数化と表現定理により可証性述語$\mathrm{Pr}_T$が書け、$T \vdash \varphi \Rightarrow T \vdash \mathrm{Pr}_T(\ulcorner\varphi\urcorner)$が出る。逆は一般には成り立たないが、$\omega$無矛盾なら成り立つ。
$3.$ 対角化定理が自己言及を作る。使うのは$\mathrm{Q}$での表現可能性だけである。
$4.$ Gödel文について：無矛盾性から$T \nvdash \sigma$、$\omega$無矛盾性から$T \nvdash \neg\sigma$（$T$が$\mathrm{PA}$を含めば$\Sigma_1$健全性で足りる）。非対称性の源は、「外から中」の翻訳は無条件だが「中から外」の翻訳は仮定だという点にある。Rosserの改良で仮定は無矛盾性だけになる。以上はすべて$\mathrm{Q}$を含む理論について成り立つ。
$5.$ 同じ道具から、Tarskiの定理、$\mathrm{Q}$の本質的決定不能性、Churchの定理が出る。Presburger算術との対比で、掛け算を落とすと自己言及に必要な表現力が失われることが分かる。

後編の予告

後編では第二不完全性定理$T \nvdash \mathrm{Con}(T)$を扱う。可証性述語の基本性質（補題6）の別証明の注意で予告した通り、そこでは$\Sigma_1$完全性が体系の内部に取り込まれ、準備編の「各点的な把握」と「一様な把握」の差が実際に効いてくる。そのため後編では、$T$は$\mathrm{PA}$を含むとし、$\mathrm{Pr}_T$を$\mathrm{PA}$上で$\Sigma_1$に取る。

後編へ続く：（工事中）