Gödel–Rosser の第一不完全性定理 | 数理論理

1 対象理論と証明述語

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

定義 1.1. $T$ が無矛盾であるとは、固定した矛盾文 $0=S0$ を $T$ が証明しないことをいう。

$T$ が1-無矛盾であるとは、 $T$ が証明する任意の $\Sigma_1$ 文が標準モデル $\mathbb N$ で真であることをいう。ここで $\Sigma_1$ 文は§E16.19 定義 2.1の意味である。

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)$ は原始再帰的である。

定義 1.2. $\operatorname{Prf}_T(p,y)$ を、§E16.21 定義 3.3で固定した標準証明述語とする。§E16.21 命題 5.2 (2)により、 $\operatorname{Prf}_T$ は§E16.19 定義 2.1の意味の $\Sigma_1$ 論理式である。また§E16.21 命題 5.2 (3)により、 $\operatorname{Prf}_T$ は $\operatorname{Proof}_T$ を肯定例と否定例の双方について数詞ごとに $Q$ で表現する。

\operatorname{Prov}_T(y):=\exists p\,\operatorname{Prf}_T(p,y)

と定める。§E16.21 定理 5.4により、任意の標準自然数 $p,y$ と任意の $L_A$ 文 $\varphi$ について、次が成り立つ。

\begin{aligned} \mathbb N\models\operatorname{Prf}_T(\bar p,\bar y) &\Longleftrightarrow \operatorname{Proof}_T(p,y),\\ \mathbb N\models\operatorname{Prov}_T(\ulcorner\varphi\urcorner) &\Longleftrightarrow T\vdash\varphi. \end{aligned}

さらに、 $p_0$ が $\varphi$ の標準証明符号ならば

Q\vdash\operatorname{Prf}_T(\bar p_0,\ulcorner\varphi\urcorner), \qquad T\vdash\operatorname{Prov}_T(\ulcorner\varphi\urcorner)

である。

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

2 Gödel 文

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

定義 2.1. $G_T$ を、次の固定点同値を満たす $L_A$ 文とする。

T\vdash G_T\leftrightarrow \neg\operatorname{Prov}_T(\ulcorner G_T\urcorner).

\text{(G)}

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

定理 2.2. $T$ を、 $Q$ を含み、公理集合を計算可能に列挙することができる $L_A$ 理論とする。

$T$ が無矛盾ならば、 $T\nvdash G_T$ である。
$T$ が1-無矛盾ならば、 $T\nvdash\neg G_T$ である。

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

証明.(1)を示す。 $T\vdash G_T$ と仮定し、その有限証明の標準符号を $p_0$ とする。定義 1.2により

T\vdash\operatorname{Prov}_T(\ulcorner G_T\urcorner)

\text{(2.2.1)}

である。一方、式 (G)の左から右への含意と $T\vdash G_T$ から

T\vdash\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)

\text{(2.2.2)}

を得る。式 (2.2.1)と式 (2.2.2)から $T$ は矛盾する。従って、 $T$ が無矛盾ならば $T\nvdash G_T$ である。

(2)を示す。 $T\vdash\neg G_T$ と仮定する。古典命題論理を式 (G)へ適用すると

T\vdash\operatorname{Prov}_T(\ulcorner G_T\urcorner)

\text{(2.2.3)}

を得る。§E16.21 命題 5.2 (2)により $\operatorname{Prf}_T(p,y)$ は $\Delta_0$ 論理式 $\operatorname{Check}_T$ を用いて $\exists z\,\operatorname{Check}_T(p,y,z)$ の形に固定されているので、 $\operatorname{Prov}_T(\ulcorner G_T\urcorner)=\exists p\,\exists z\,\operatorname{Check}_T(p,\ulcorner G_T\urcorner,z)$ は§E16.19 定義 2.1の意味の $\Sigma_1$ 文である。ここで同値な別の論理式へ取り替えてはいない。 $T$ の1-無矛盾性により

\mathbb N\models\operatorname{Prov}_T(\ulcorner G_T\urcorner)

となる。定義 1.2の標準モデルでの正確性から、ある標準証明符号が存在して $T\vdash G_T$ である。1-無矛盾性は無矛盾性を含意するため、 $T\vdash G_T$ と仮定した $T\vdash\neg G_T$ は両立しない。従って $T\nvdash\neg G_T$ である。▨

(2)の議論では、1-無矛盾性を単なる無矛盾性へ置き換えることはできない。式 (2.2.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$ は§E16.15 定義 2.1 (Q4)、§E16.15 定義 2.1 (Q5)を $n$ 回だけ用いて証明することができる。この向きの定義により、自由変数 $p$ に対する「 $p$ は $\bar n$ より小さいか、 $\bar n$ 以上である」という固定境界の分割を、帰納法なしで $Q$ 内に構成することができる。

補題 3.1. $n$ を標準自然数とし、 $A(x)$ を一変数算術式とする。

$Q\vdash\forall p\,(p\prec\bar n\lor\bar n\preccurlyeq p)$ である。
各標準自然数 $k\le n$ について $Q\vdash\neg A(\bar k)$ ならば、 $Q\vdash\forall k\,(k\preccurlyeq\bar n\to\neg A(k))$ である。
各標準自然数 $k<n$ について $Q\vdash\neg A(\bar k)$ ならば、 $Q\vdash\forall k\,(k\prec\bar n\to\neg A(k))$ である。

証明.(1)は§E16.19 補題 3.3 (2)そのものであり、束縛変数の名前だけが異なる。

(2)と(3)では、固定数詞を上界とする候補が有限個の数詞に分かれることを用いる。§E16.19 補題 3.3 (1)により、 $k\preccurlyeq\bar n$ から $k=\bar0\lor\cdots\lor k=\bar n$ が、 $k\prec\bar n$ から $k=\bar0\lor\cdots\lor k=\overline{n-1}$ が得られる。各選言では等号の置換可能性と仮定した有限個の否定証明を用いる。有限選言を消去して $k$ を全称化すると、表示した二つの有界全称文を得る。これは標準自然数 $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}}$ だけである。これを数詞へ潰す段は、固定点を取った後に置く。

定義 4.1. $R_T$ を、§E16.22 定理 2.1を上の $\theta$ へ適用して得られる $L_A$ 文とする。すなわち $R_T$ は次の固定点同値を満たす。

Q\vdash R_T\leftrightarrow\theta(\ulcorner R_T\urcorner).

\text{(R0)}

固定点を取った後は、グラフ式を数詞へ潰すことができる。 $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)$ の同値を証明する。これを式 (R0)の右辺へ代入すると

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)

\text{(R)}

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

定理 4.2 (Gödel–Rosser の第一不完全性定理). $T$ を、 $Q$ を含み、公理集合を計算可能に列挙することができる $L_A$ 理論とする。

$T$ が無矛盾ならば $T\nvdash G_T$ であり、 $T$ が1-無矛盾ならば $T\nvdash\neg G_T$ である。
$T$ が無矛盾ならば、 $T\nvdash R_T$ かつ $T\nvdash\neg R_T$ である。

従って、無矛盾で公理集合を計算可能に列挙することができる任意の $T\supseteq Q$ は構文論的に不完全である。

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

証明.(1)は定理 2.2で証明した。

(2)の最初の方向を示す。 $T$ が無矛盾であるにもかかわらず $T\vdash R_T$ であると仮定し、 $R_T$ の標準証明符号を $p_0$ とする。無矛盾性により $T\nvdash\neg R_T$ である。従って、各標準自然数 $q\le p_0$ について

\neg\operatorname{Proof}_T(q,\ulcorner\neg R_T\urcorner)

が成り立つ。§E16.21 命題 5.2 (3)により $\operatorname{Prf}_T$ は否定例も数詞ごとに表現するため、各標準自然数 $q\le p_0$ について

Q\vdash\neg\operatorname{Prf}_T(\bar q,\ulcorner\neg R_T\urcorner)

である。補題 3.1 (2)から

Q\vdash\neg\exists q\left( q\preccurlyeq\bar p_0\land \operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner) \right)

\text{(4.2.1)}

を得る。一方、 $p_0$ は実際の証明符号なので

Q\vdash\operatorname{Prf}_T(\bar p_0,\ulcorner R_T\urcorner)

\text{(4.2.2)}

である。式 (R)、仮定 $T\vdash R_T$ 、および式 (4.2.2)から、 $T$ は式 (4.2.1)で否定した存在文を証明する。 $Q\subseteq T$ なので式 (4.2.1)も $T$ の定理であり、 $T$ は矛盾する。従って $T\nvdash R_T$ である。

次に $T\nvdash\neg R_T$ を示す。 $T\vdash\neg R_T$ と仮定し、その標準証明符号を一つ取って $q_0$ とする。最小のものを選ぶ必要はない。無矛盾性により、 $R_T$ の標準証明符号は一つも存在しない。§E16.21 命題 5.2 (3)により得られる否定例の表現可能性により、特に、各標準自然数 $p<q_0$ について

Q\vdash\neg\operatorname{Prf}_T(\bar p,\ulcorner R_T\urcorner)

である。補題 3.1 (3)から

Q\vdash\forall p\left( p\prec\bar q_0\to \neg\operatorname{Prf}_T(p,\ulcorner R_T\urcorner) \right)

\text{(4.2.3)}

を得る。また、 $q_0$ は $\neg R_T$ の実際の証明符号なので

Q\vdash\operatorname{Prf}_T(\bar q_0,\ulcorner\neg R_T\urcorner).

\text{(4.2.4)}

任意の $p$ を取る。補題 3.1 (1)の固定境界分割により、 $p\prec\bar q_0$ または $\bar q_0\preccurlyeq p$ である。前者では式 (4.2.3)により式 (R)の含意の前件が偽である。後者では、式 (4.2.4)と $q=\bar q_0$ を用いると式 (R)の存在量化された後件が成り立つ。従って

Q\vdash\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).

\text{(4.2.5)}

式 (R)の右から左への含意と式 (4.2.5)から $Q\vdash R_T$ 、従って $T\vdash R_T$ である。仮定 $T\vdash\neg R_T$ と合わせると $T$ は矛盾する。従って $T\nvdash\neg R_T$ である。

Rosser の二方向では、標準モデルにおける $T$ の健全性、1-無矛盾性、または $\omega$ -無矛盾性を用いていない。外側で用いたのは、具体的な標準証明符号を一つ取ることと $T$ の構文的無矛盾性だけである。対象理論内では、固定された有限個の数詞についての表現可能性と有限境界分割だけを用いた。▨

例 4.3. $q_0=4$ が $\neg R_T$ の証明符号であると仮定する。 $p=0,1,2,3$ では $R_T$ の証明検査が失敗することを、それぞれの否定例として $Q$ が証明する。 $p\ge4$ では、 $q=4$ を式 (R)の後件の証人に用いる。この有限な二分が、一般の標準符号 $q_0$ に対する証明と同じ構造をもつ。

5 演習

問題 5.1. 次の問いに答えよ。

$T\vdash G_T$ から $T\vdash\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ へ移る際に、 $T$ の健全性を用いない理由を述べよ。
$T\vdash\neg G_T$ の排除に1-無矛盾性を用いる箇所を特定せよ。
$T\vdash R_T$ を仮定する方向で、なぜ $p_0$ 以下の有限個の否定例だけを $Q$ へ移せば足りるのか。
$T\vdash\neg R_T$ を仮定する方向で、 $p\prec\bar q_0$ と $\bar q_0\preccurlyeq p$ の各場合に式 (R)の含意をどのように証明するか。

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

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

▨

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

1 対象理論と証明述語

2 Gödel 文

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

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

5 演習

参考文献

前提記事