§E16.23Gödel–Rosser の第一不完全性定理

1 対象理論と証明述語

算術言語を$L_A=\{0,S,+,\times\}$とする。理論$T$は$L_A$の文からなり、$Q\subseteq T$を満たすと仮定する。さらに、$T$の公理を計算可能に列挙する決定的プログラムを一つ固定する。無矛盾性は各定理で明示的に仮定し、この段階では仮定しない。

1-無矛盾性は無矛盾性より強い。実際、$0=S0$は$\Delta_0$文であるから、これに現れない変数$w$を取ると$\exists w\,(0=S0)$は$\Sigma_1$文であり、$\mathbb N\not\models\exists w\,(0=S0)$である。従って、$T$が矛盾するならば$T\vdash0=S0$から$T\vdash\exists w\,(0=S0)$を得るので、1-無矛盾性に反する。

公理集合が計算可能に列挙可能であることと、公理所属が決定可能であることを区別する必要がある。証明述語の記事では、列挙プログラムが公理を出力するまでの有限計算列を$\operatorname{AxWit}_T(a,w)$として符号化し、各非論理公理行に証人$w$を添えた。§E16.21 定理 2.2と§E16.21 命題 3.2により、この証人を含む外的証明関係$\operatorname{Proof}_T(p,y)$は原始再帰的である。

最後の内部化は、$T$の健全性を用いない。具体的な有限証明符号が外側で存在することを、数詞ごとの表現可能性によって$Q$の有限証明へ移している。

2 Gödel 文

§E16.22 定理 2.1を$\neg\operatorname{Prov}_T(x)$へ適用する。

同値 (G) は$G_T$の真理を仮定していない。また、$T$の無矛盾性も仮定せず、対角線補題が$Q$内で構成した有限証明を$T$へ移した結果である。

証明方針は、二つの方向で異なる。第1項では、$G_T$の具体的な証明を証明可能性述語へ内部化し、固定点同値が与える否定と衝突させる。第2項では、$\neg G_T$から得られる$\Sigma_1$文$\operatorname{Prov}_T(\ulcorner G_T\urcorner)$に1-無矛盾性を適用し、標準証明の存在へ戻す。

第2項の議論では、1-無矛盾性を単なる無矛盾性へ置き換えることはできない。(3) が$T$内で証明されたことから、同じ$\Sigma_1$文が標準モデルで真であることを導く段階が追加で必要だからである。

3 Rosser 文に必要な有限数詞推論

証明符号の大小を算術内部で比較する式には、§E16.19 定義 2.1が固定した略記

$$a\preccurlyeq b:\!\!\Longleftrightarrow \exists d\,(d+a=b), \qquad a\prec b:\!\!\Longleftrightarrow S a\preccurlyeq b$$

を用いる。$a,b$が標準自然数ならば、これらは標準モデルで通常の大小関係を表す。加法の第2引数が固定数詞であるため、$d+\bar n=S^n d$は (Q4)、(Q5) を$n$回だけ用いて証明することができる。この向きの定義により、自由変数$p$に対する「$p$は$\bar n$より小さいか、$\bar n$以上である」という固定境界の分割を、帰納法なしで$Q$内に構成することができる。

4 Rosser 文と第一不完全性定理

式の符号からその否定の符号を返す全域構文操作$\operatorname{Neg}$は§E16.18 定義 4.1で定義されており、§E16.18 定理 5.2により原始再帰的である。従って§E16.19 定理 7.1 (1)が、$\operatorname{Neg}$を$Q$で強く数詞ごとに表現する一変数のグラフ式$\varphi_{\operatorname{Neg}}(x,u)$を与える。そこで

$$\theta(x):\!\!\Longleftrightarrow \forall p\left( \operatorname{Prf}_T(p,x) \to \exists q\left(q\preccurlyeq p\land \exists u\left(\varphi_{\operatorname{Neg}}(x,u)\land \operatorname{Prf}_T(q,u)\right) \right) \right)$$

と定める。$\theta$の自由変数は高々$x$なので、§E16.22 定理 2.1を$\theta$へ適用することができる。この段階で$\operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner)$と直接書くことはできない。$R_T$はこれから対角線補題で得る文であり、その符号はまだ定まっていないからである。書くことができるのは、否定の符号を対応させるグラフ式$\varphi_{\operatorname{Neg}}$だけである。これを数詞へ潰す段は、固定点を取った後に置く。

固定点を取った後は、グラフ式を数詞へ潰すことができる。$R_T$は$L_A$文なので$\operatorname{Neg}(\ulcorner R_T\urcorner)=\ulcorner\neg R_T\urcorner$である。§E16.19 定義 1.2が定める強い数詞ごとの表現の条件を、この入力へ適用すると

$$Q\vdash\forall u\left( \varphi_{\operatorname{Neg}}(\ulcorner R_T\urcorner,u) \leftrightarrow u=\ulcorner\neg R_T\urcorner \right)$$

である。従って$Q$は、任意の$q$について$\exists u(\varphi_{\operatorname{Neg}}(\ulcorner R_T\urcorner,u)\land\operatorname{Prf}_T(q,u))$と$\operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner)$の同値を証明する。これを$(\mathrm{R}_0)$の右辺へ代入すると

$$Q\vdash R_T\leftrightarrow \forall p\left( \operatorname{Prf}_T(p,\ulcorner R_T\urcorner) \to \exists q\left(q\preccurlyeq p\land \operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner) \right) \right) \tag{R}$$

を得る。以下ではこの (R) の形だけを用いる。式 (R) は、「$R_T$の各証明には、それ以下の符号をもつ$\neg R_T$の証明が存在する」と述べる。量化子$p,q$は対象理論内の自然数を走る。以下の証明では、外側で選んだ標準証明符号を数詞として入れた後に、固定境界の有限推論だけを$Q$内で用いる。

証明方針は、第1項には定理 2.2を適用することである。第2項では、$R_T$または$\neg R_T$の標準証明符号を一つ固定する。反対側の標準証明が存在しないことを無矛盾性から得て、そのうち必要な有限範囲だけを補題 3.1によって$Q$内へ移す。

5 演習

解答 (確認問題の解答).

1. $G_T$の具体的な有限証明符号$p_0$を取り、真である原始再帰関係$\operatorname{Proof}_T(p_0,\ulcorner G_T\urcorner)$の数詞例を$Q$で証明するからである。意味論的健全性は介在しない。
2. $T\vdash\neg G_T$から得た$\Sigma_1$文$\operatorname{Prov}_T(\ulcorner G_T\urcorner)$を、標準モデルで真な文へ移す段階で用いる。
3. (R) を$R_T$の具体的な証明符号$p_0$へ適用すると、必要な反対側の証明符号は標準自然数$q\le p_0$に限定されるからである。
4. $p\prec\bar q_0$では$\operatorname{Prf}_T(p,\ulcorner R_T\urcorner)$を否定して含意を証明する。$\bar q_0\preccurlyeq p$では、$\neg R_T$の証明符号$q_0$自身を存在量化の証人に用いる。

▨

6 境界と次の段階

本記事は、計算可能に公理化された$T\supseteq Q$に対する Gödel 文と Rosser 文の第一不完全性だけを扱った。完全性定理、標準モデルにおける健全性、$\omega$-無矛盾性、または第二不完全性定理を証明の前提には用いていない。後続の記事は、ここで固定した同じ$\operatorname{Prf}_T$と$\operatorname{Prov}_T$を用い、導出可能性条件と$\operatorname{Con}_T$の非証明を扱う。