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$ 文は§E19.19 定義 2.1の意味である。

1-無矛盾性は無矛盾性より強い。実際、 $0=S0$ は $\Delta_0$ 文であるから、 $0=S0$ に現れない変数 $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$ を添えた。§E19.21 定理 2.2と§E19.21 命題 3.2により、この証人を含む外的証明関係 $\operatorname{Proof}_T(p,y)$ は原始再帰的である。

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

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

と定める。§E19.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\vdash\operatorname{Prov}_T(\ulcorner\varphi\urcorner)$ を得る際には、 $T$ の健全性を用いない。具体的な有限証明符号が外側で存在するという事実から、数詞ごとの表現可能性によって $Q$ の有限証明を得ている。

2 Gödel 文

§E19.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)}

を得る。§E19.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)$ は§E19.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 文に必要な有限数詞推論

証明符号の大小を算術内部で比較するために、§E19.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$ は§E19.15 定義 2.1 (Q4)、§E19.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)は§E19.19 補題 3.3 (2)そのものであり、束縛変数の名前だけが異なる。

主張 (2)と主張 (3)では、固定数詞を上界とする候補が有限個の数詞に分かれることを用いる。§E19.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}$ は§E19.18 定義 4.1で定義されており、§E19.18 定理 5.2により原始再帰的である。従って§E19.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$ なので、§E19.22 定理 2.1を $\theta$ へ適用することができる。この段階で $\operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner)$ と直接書くことはできない。 $R_T$ はこれから対角線補題で得る文であり、その符号はまだ定まっていないからである。書くことができるのは、式の符号に否定の符号を対応させる操作 $\operatorname{Neg}$ のグラフ式 $\varphi_{\operatorname{Neg}}$ だけである。 $\theta$ の部分式 $\exists u(\varphi_{\operatorname{Neg}}(x,u)\land\operatorname{Prf}_T(q,u))$ の $x$ に $\ulcorner R_T\urcorner$ を代入した式を、 $Q$ で同値な式 $\operatorname{Prf}_T(q,\ulcorner\neg R_T\urcorner)$ へ書き換える段は、固定点を取った後に置く。

定義 4.1. $R_T$ を、§E19.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$ である。§E19.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)

が成り立つ。§E19.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$ の標準証明符号は一つも存在しない。§E19.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. 次の問いに答えよ。

$G_T$ を、§E19.22 定理 2.1により $Q\vdash G_T\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ を満たすように取る。 $T$ が無矛盾ならば $G_T$ が標準モデルで真であることを示せ。
1 の $G_T$ について、 $T$ が無矛盾ならば、理論 $T'=T\cup\{\neg G_T\}$ は無矛盾であるが1-無矛盾でないことを示せ。
$T$ が無矛盾ならば $R_T$ が標準モデルで真であることを示せ。
式 (R)の $q\preccurlyeq p$ を $q\prec p$ に置き換えた固定点、すなわち $Q\vdash R'_T\leftrightarrow \forall p\left( \operatorname{Prf}_T(p,\ulcorner R'_T\urcorner) \to \exists q\left(q\prec p\land \operatorname{Prf}_T(q,\ulcorner\neg R'_T\urcorner) \right) \right)$ を満たす文 $R'_T$ を考える。 $T$ が無矛盾ならば $T\nvdash R'_T$ かつ $T\nvdash\neg R'_T$ であることを示せ。 $R'_T$ が存在することは、定義 4.1と同じ構成で得られるものとしてよい。

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

$T$ が無矛盾ならば、定理 2.2 (1)により $T\nvdash G_T$ である。定義 1.2の標準モデルでの正確性により $\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ は標準モデルで偽であり、 $\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ は標準モデルで真である。標準モデルは $Q$ のモデルであるから、健全性により $G_T\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ は標準モデルで真であり、 $G_T$ は標準モデルで真である。この議論では $T$ の公理が標準モデルで真であることを用いていない。
$T\nvdash G_T$ であるから、§E19.12 補題 5.1により $T'$ は構文的に無矛盾であり、とくに $T'\nvdash0=S0$ である。 $Q\subseteq T\subseteq T'$ であるから $T'\vdash G_T\leftrightarrow\neg\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ であり、 $T'\vdash\neg G_T$ と古典命題論理により $T'\vdash\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ である。定理 2.2 (2)の証明で見たとおり、 $\operatorname{Prov}_T(\ulcorner G_T\urcorner)$ は $\Sigma_1$ 文である。一方、 $T\nvdash G_T$ と標準モデルでの正確性により、この文は標準モデルで偽である。よって $T'$ は標準モデルで偽な $\Sigma_1$ 文を証明し、1-無矛盾でない。 $T'$ の公理は $T$ の公理の列挙に一つの文を加えて計算可能に列挙することができ、 $T'$ は無矛盾性と1-無矛盾性が異なる理論の例である。
$T$ が無矛盾ならば、定理 4.2 (2)により $T\nvdash R_T$ である。標準モデルでの正確性により、どの標準自然数 $p$ についても $\operatorname{Prf}_T(\bar p,\ulcorner R_T\urcorner)$ は標準モデルで偽である。したがって式 (R)の右辺の全称文は、含意の前件がすべての $p$ で偽であるから標準モデルで真である。標準モデルは $Q$ のモデルであるから、健全性により式 (R)の同値は標準モデルで真であり、 $R_T$ は標準モデルで真である。
$T$ を無矛盾とする。 $T\vdash R'_T$ と仮定し、その標準証明符号を $p_0$ とする。無矛盾性により $\neg R'_T$ の標準証明は存在しないので、各 $q<p_0$ について§E19.21 命題 5.2 (3)により $Q\vdash\neg\operatorname{Prf}_T(\bar q,\ulcorner\neg R'_T\urcorner)$ であり、補題 3.1 (3)により $Q\vdash\neg\exists q\,(q\prec\bar p_0\land\operatorname{Prf}_T(q,\ulcorner\neg R'_T\urcorner))$ である。一方 $Q\vdash\operatorname{Prf}_T(\bar p_0,\ulcorner R'_T\urcorner)$ であり、固定点と $T\vdash R'_T$ から $T\vdash\exists q\,(q\prec\bar p_0\land\operatorname{Prf}_T(q,\ulcorner\neg R'_T\urcorner))$ を得るので、 $T$ は矛盾する。よって $T\nvdash R'_T$ である。

$T\vdash\neg R'_T$ と仮定し、その標準証明符号を $q_0$ とする。無矛盾性により $R'_T$ の標準証明は存在しないので、各 $p\leq q_0$ 、すなわち各 $p<q_0+1$ について $Q\vdash\neg\operatorname{Prf}_T(\bar p,\ulcorner R'_T\urcorner)$ であり、補題 3.1 (3)を $n=q_0+1$ に適用して $Q\vdash\forall p\,(p\prec\overline{q_0+1}\to\neg\operatorname{Prf}_T(p,\ulcorner R'_T\urcorner))$ を得る。任意の $p$ を取る。補題 3.1 (1)を $n=q_0+1$ に適用すると、 $p\prec\overline{q_0+1}$ または $\overline{q_0+1}\preccurlyeq p$ である。前者では含意の前件が偽である。後者では $\overline{q_0+1}=S\bar q_0$ であるから、 $\prec$ の定義により $\bar q_0\prec p$ であり、 $Q\vdash\operatorname{Prf}_T(\bar q_0,\ulcorner\neg R'_T\urcorner)$ と $q=\bar q_0$ により後件が成り立つ。よって $Q$ は固定点の右辺を証明し、 $Q\vdash R'_T$ 、したがって $T\vdash R'_T$ となって $T\vdash\neg R'_T$ と矛盾する。よって $T\nvdash\neg R'_T$ である。

▨

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

1 対象理論と証明述語

2 Gödel 文

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

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

5 演習

参考文献

前提記事