数学基礎論講義をこっそり読む（その９） - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

第６講に入っていよいよ第一不完全性定理です。
お話っぽい説明が多くてサクサク進むのですが、行間を埋めつつ読み進めます。

まず p.87 のメタ定理 $T\vdash\varphi \Leftrightarrow \mathfrak{N} \models Pr{}_{T}(\overline{\lceil \varphi \rceil})$ の証明。

（ $\Rightarrow$ ）証明 $T\vdash\varphi$ のゲーデル数を $n$ とすると $\mathbf{Prov}{}_{T}(n,{\lceil \varphi \rceil})$ が成立している。(1)より、 $Q\vdash Prov{}_T (\bar{n},\overline{\lceil \varphi \rceil})$ . $\mathfrak{N}$ は $Q$ のモデルなので、 $\mathfrak{N} \models Pr{}_{T}(\overline{\lceil \varphi \rceil})$ 　□

（ $\Leftarrow$ ) $\mathfrak{N} \models Pr{}_{T}(\overline{\lceil \varphi \rceil})$ ならば論理式 $\exists y Prov{}_{T}(y,\overline{\lceil \varphi \rceil})$ を成立させる $y$ への自然数の割り当て $n$ がある。このとき、もし、 $\mathbf{Prov}{}_{T}(n,{\lceil \varphi \rceil})$ が成立しないと仮定すると (2)より $Q\vdash \neg Prov{}_T (\bar{n},\overline{\lceil \varphi \rceil})$ となるが、これはモデル $\mathfrak{N}$ の上で矛盾している。したがって、 $\mathbf{Prov}{}_{T}(n,{\lceil \varphi \rceil})$ が成立し、 $n$ が「Tにおける $\varphi$ の証明」を与えるゲーデル数であることがわかる □

定理6.1の注意１についてですが、上記の（ $\Rightarrow$ ）で $Q\vdash Prov{}_T (\bar{n},\overline{\lceil \varphi \rceil})$ が分かっているので、 $\bar{n}$ のところを特称化すれば直ちに $Q\vdash Pr{}_T (\overline{\lceil \varphi \rceil})$ がでます。

次にp.88の対角化定理の証明中ですが、｢x以外の自由変数を含まない論理式すべてを、そのゲーデル数の小さい順に並べて」としれっと書いてありますが、この手続きが再帰的つまり、 $A(n) \equiv \lceil A_n(x) \rceil$ が再帰的関数かどうかが問題になります。実際は原始再帰的関数になります。その証明は形式的にやろうとすると少々面倒ですが、「与えられた自然数nがx以外の自由変数を含まない論理式のゲーデル数であるとき真、そうでないとき偽になる」ような原始再帰的関数 $F(n)$ が存在します。また、論理式 $\varphi$ のゲーデル数が与えられたときその論理式全体の否定 $\neg \varphi$ のゲーデル数を与える原始再帰的関数を $Neg(n)$ とします。（これらの構成は前原昭二著『数学基礎論入門』の９章で詳しく展開されています）。

この二つの原始再帰的関数を使って、

$A(0)=\lceil 0=0 \rceil$ ,　[tex:A(n+1)=\mu y< Neg(A(n))+1(A(n)

ですが、 $\varphi$ は「正しいけれどもTでは証明できない文」という意味は、 $\mathfrak{N}\vDash \varphi$ ではあるが、 $T\not\vdash \varphi$ になっているということで、無論このとき、 $\mathfrak{N}\vDash \neg Pr_{T}(\overline{\lceil \varphi \rceil})$ すなわち「証明を与えるゲーデル数は存在しない」が成立しています。（これらの主張の証明は、もし $\varphi$ が標準モデル $\mathfrak{N}$ で偽になると、 $Pr_{T}(\overline{\lceil \varphi \rceil})$ が真、すなわち $\varphi$ の証明が存在することになり、 $\varphi$ は真でなければならず、矛盾することからです。）

(2)は計算論との絡みで私には興味深いところなので証明を付けました。

1)　 $A(n)$ :RE
2)　論理式 $\varphi(x)$ が存在して、 $A(n)$ ⇔ $T\vdash \varphi(\bar{n})$
は同値。

(はてなではboldfaceがあんまり綺麗にでないですねぇ。再帰的関係 $\mathbf{S}$ と論理式 $S$ を区別しないと何がなんだかわからなくなります。）

＜証明＞
1)⇒ 2)
REの定義より、（原始）再帰的関係 $\mathbf{S}(x,y)$ が存在して、 $A(n)=\exist y \mathbf{S}(n,y)$ となる（補題4.14）。表現可能性定理により $\mathbf{S}(x,y)$ を表現する $Q$ の論理式 $S(x,y)$ が存在する。 $\varphi(x)\equiv \exist y S(x,y)$ と定義すると、

$A(n)$ が成立 ⇒ 自然数 $m$ が存在して $\mathbf{S}(n,m)$ が成立
　⇒ $\vdash S(\bar{n},\bar{m})$
　⇒ $\vdash \exist y S(\bar{n},y)$
　⇒ $\vdash \varphi(\bar{n})$

逆に $\vdash \varphi(\bar{n})$ ならば標準モデルで真となるから、自然数 m が存在して $\mathfrak{N}\vDash S(\bar{n},\bar{m})$ 。このとき $\mathbf{S}(n,m)$ がもし成立しないとすると、 $\vdash \neg S(\bar{n},\bar{m})$ となるが、標準モデルで $\mathfrak{N}\vDash \neg S(\bar{n},\bar{m})$ となるため、矛盾である。　よって $A(n)$ が成立 ⇔ $\vdash \varphi(\bar{n})$ が示せた。□

2)⇒ 1)
$\varphi(x)$ のゲーデル数をnとする。再帰的関係を $\mathbf{S}(x,y)\equiv \mathbf{Prov}_{T}(y,x)$ とすると、

$A(n)$ ⇔ $T\vdash \varphi(\bar{n})$ ⇔ 自然数 $m$ が存在して $\mathbf{S}(n,m)$

が成立するので、 $A(n)$ はREである。□

さて、最後のステートメントの証明ですが、もし仮に、すべての自然数 $n$ に対して $T\vdash \varphi(\bar{n})$ または $T\vdash \neg\varphi(\bar{n})$ が成立すると仮定すると、

$\neg A(n)$ ⇔ $T \not\vdash \varphi(\bar{n})$ ⇔ $T\vdash \neg\varphi(\bar{n})$

が成立するため、 $\phi(x)\equiv \neg\varphi(x)$ とすると前段より、 $\neg A(n)$ がREであることが出ます。つまり、最初から $A(n)$ をREではあるが再帰的でないと仮定するとある自然数 $n$ が存在して、 $T\not\vdash \varphi(\bar{n})$ かつ $T\not\vdash \neg\varphi(\bar{n})$ となります。