3. 不完全性の十分条件

準備

定義 3.1
任意の算術 $T$ に対して,$\mathcal{D}$ の部分集合 $\mathcal{D}^T_\exists$ と $\mathcal{D}^T_\forall$ を次のように定義します.
\( \mathcal{D}^T_\exists = \{ \langle p,q \rangle \in \mathcal{D} \mid T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \} \)
\( \mathcal{D}^T_\forall = \{ \langle p,q \rangle \in \mathcal{D} \mid T \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \} \)
$\mathcal{D}^T_\exists$ は自然数解を持つことが $T$ において証明可能なD方程式の集合であり, $\mathcal{D}^T_\forall$ は自然数解を持たないことが $T$ において証明可能なD方程式の集合です.■

上記の集合に対して次の命題が成り立ちます. この命題は直感的に明らかだと言ったっら少し叱られるようにも思われますが, 詳細な証明は省略いたします.

命題 3.2
計算的枚挙可能な任意の算術 $T$ に対して, $\mathcal{D}^T_\exists$ と $\mathcal{D}^T_\forall$ はともに計算的枚挙可能です.

略証  以下,$\mathcal{D}^T_\forall$ を受理するTM(チューリング機械)の概要を示します.$\mathcal{D}^T_\exists$ についても同様です.概要を示すための前提として,$T$ は計算的枚挙可能であるとします. さらに,記号列としての「$T$ における証明」を構成する記号からなる集合を $\mathcal{X}$ で表し,$\mathcal{X}$ 上の記号列全体を $\mathcal{X}^*$ で表します.

  まず最初に,算術の基盤にある述語論理を具体的に定め(例えば,自然演繹やヒルベルトの公理体系などを選び),「$T$ における証明」の構文を適切に定義すれば,$T$ を受理するTMを利用して次のようなTM $M_0$ が存在することを示せます. この $M_0$ は $T \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$ であることの「$T$ における証明」を構文的に解析するプログラムを示しています. その詳細は難しくはないと思いますが面倒なので省略いたします.

次に,この $M_0$ を使って次のようなTM $M_1$ を作ることができます. これは $M_0$ にタイマーを組み込めばよいだけのことです. なお,「ステップ」とは計算状況の遷移回数のことです.

最後に,$\alpha_1, \alpha_2, \ldots $ を $\mathcal{X}^*$ に属する記号列の計算可能な列挙(例えば,適当な辞書式順序に基づく列挙)として,$M_1$ を使って次のようなTM $M_2$ を作ります. この $M_2$ と任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます. 以上より,$M_2$ は $\mathcal{D}^T_\forall$ を受理するので,$\mathcal{D}^T_\forall$ は計算的枚挙可能です. ■

補足 MRDP定理の系より $\mathcal{D}^\mathcal{N}_\forall$ は計算的枚挙可能ではありません. これと上記の命題より, $\mathcal{D}^\mathcal{N}_\forall \not= \mathcal{D}^T_\forall$ が成り立ちます. つまり,計算的枚挙可能な算術については,D方程式の解の非存在性に関して真理条件と証明可能性の間に必ずズレが生じます. 以下の議論では,このズレを使って不完全性の証拠を見つけていきます.

$\Pi_1^\mathcal{D}$-健全性

定義 3.3
算術 $T$ が $\Pi_1^\mathcal{D}$-健全 であるということを, が成り立つこととします.この条件は
\( \mathcal{D}^T_\forall \subseteq \mathcal{D}^\mathcal{N}_\forall \)
が成り立つことと等価です.

定理 3.4
$T$ を計算的枚挙可能で$\Pi_1^\mathcal{D}$-健全な算術とします. このとき,D方程式 $\langle p,q \rangle \in \mathcal{D}$ が存在して,
$\mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$ かつ $T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$
が成り立ちます.つまり,$T$ は意味論的に不完全です.

証明  $\Pi_1^\mathcal{D}$-健全性より,$\mathcal{D}^T_\forall \subseteq \mathcal{D}^\mathcal{N}_\forall$ が成り立ちます.さらに,$\mathcal{D}^T_\forall$ は計算的枚挙可能であり,MRDP定理の系より $\mathcal{D}^\mathcal{N}_\forall$ は計算的枚挙可能ではないので,$\mathcal{D}^T_\forall \not= \mathcal{D}^\mathcal{N}_\forall$ が成り立ちます. 従って,$\langle p,q \rangle \in \mathcal{D}^\mathcal{N}_\forall$ かつ $\langle p,q \rangle \not\in \mathcal{D}^T_\forall$ を満たすD方程式 $\langle p,q \rangle \in \mathcal{D}$ が存在します. このD方程式は上で述べた条件を満たします.■

補足 3.4.1  上記の算術 $T$ に対して,差集合 $\mathcal{D}^\mathcal{N}_\forall - \mathcal{D}^T_\forall$ が有限集合だったと仮定すると,$\mathcal{D}^T_\forall$ は計算的枚挙可能なので $\mathcal{D}^\mathcal{N}_\forall = \mathcal{D}^T_\forall \cup (\mathcal{D}^\mathcal{N}_\forall - \mathcal{D}^T_\forall)$ も計算的枚挙可能になってしまいます.これはMRDP定理の系に反します. 従って, 差集合 $\mathcal{D}^\mathcal{N}_\forall - \mathcal{D}^T_\forall$ は無限集合です. つまり,上の定理の条件を満たすD方程式は無数に存在します.

$\Delta_0^\mathcal{D}$-完全性 & 無矛盾性

定義 3.5
算術 $T$ が $\Delta_0^\mathcal{D}$-完全 であるということを が成り立つこととします.ここで,$\vec{a}$ は自然数列 $a_1, \ldots, a_n$ の省略記法であり,$\widehat{\vec{a}}$ は数項列 $\widehat{a_1}, \ldots, \widehat{a_n}$ の省略記法です(以下も同様です).■

補足 $\Delta^\mathcal{D}_0$-完全性は,算術 $T$ が数値的な計算(変数を含まない等式や非等式の証明)を正しく遂行できることの必要条件と言えます.従って,$\Delta^\mathcal{D}_0$-完全性は,自然な(あるいは,合理的な)算術が満たすべき最低限の性質であると言っても言い過ぎではないように思います.

定義 3.6
算術 $T$ が $\Sigma_1^\mathcal{D}$-完全 であるということを が成り立つこととします.この条件は
\( \mathcal{D}^\mathcal{N}_\exists \subseteq \mathcal{D}^T_\exists \)
が成り立つことと等価です. ■

定義 3.7
算術 $T$ が 無矛盾 であるということを, が成り立つこととします. ■

補足 $T$ が矛盾しているとき,$\mathcal{L}_A$のすべての文 $\varphi$ に対して $T \vdash \varphi$ となります.従って,$\mathcal{L}_A$のある文 $\varphi$ に対して $T \not\vdash \varphi$ ならば $T$ は無矛盾です.一般に,無矛盾性の証明はこの事実を使用します. ■

補題 3.8
任意の算術 $T$ に対して
$T$ は $\Delta_0^\mathcal{D}$-完全 $\Longrightarrow$ $T$ は $\Sigma_1^\mathcal{D}$-完全
が成り立ちます.

証明  $T$ が$\Delta_0^\mathcal{D}$-完全だったとします.このとき, 任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} &\mathcal{N} \models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\[2pt] \Longrightarrow &\mathcal{N} \models p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~~\text{for some $\vec{a} \in \mathbb{N}^n$} & \text{(真理条件の定義)} \\[2pt] \Longrightarrow & T \vdash p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~~\text{for some $\vec{a} \in \mathbb{N}^n$} & \text{($\Delta_0^\mathcal{D}$-完全性)} \\[2pt] \Longrightarrow & T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{($\exists$-導入)} \\ \end{array} \)

よって,$T$ は$\Sigma_1^\mathcal{D}$-完全です.■

定理 3.9
任意の算術 $T$ に対して次が成り立ちます.
  1. $T$ は$\Pi_1^\mathcal{D}$-健全である $\Longrightarrow$ $T$ は無矛盾である
  2. $T$ は$\Delta_0^\mathcal{D}$-完全かつ無矛盾である $\Longrightarrow$ $T$ は$\Pi_1^\mathcal{D}$-健全である

従ってまた,$\Delta_0^\mathcal{D}$-完全な任意の算術 $T$ に対して, 無矛盾性と$\Pi_1^\mathcal{D}$-健全性は等価な条件であることが分かります.

証明 (1) $T$ が$\Pi_1^\mathcal{D}$-健全だったとします. このとき, 任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} &\mathcal{N} \models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\[2pt] \Longrightarrow &\mathcal{N} \not\models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(真理条件の定義)} \\[2pt] \Longrightarrow & T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{($\Pi_1^\mathcal{D}$-健全性)} \\[2pt] \end{array} \)

これはD方程式 $\langle p,q \rangle \in \mathcal{D}$ が自然数解を持つとき, 「それが自然数解を持たない」ということを $T$ が証明できないことを示しています. 従って,例えば, D方程式 $x=x$ は明らかに自然数解を持つので,
$T \not\vdash \forall{x}\neg(x=x)$
が成り立ちます.よって,$T$ は無矛盾です.

 (2) $T$ が$\Delta_0^\mathcal{D}$-完全かつ無矛盾だったとします.このとき, 任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} &\mathcal{N} \not\models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \\[2pt] \Longrightarrow &\mathcal{N} \models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{(真理条件の定義)} \\[2pt] \Longrightarrow & T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{($\Sigma_1^\mathcal{D}$-完全性 via 補題3.8)} \\[2pt] \Longrightarrow & T \not\vdash \neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{(無矛盾性)} \\[2pt] \Longrightarrow & T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(ド・モルガンの法則)} \\[2pt] \end{array} \)

この対偶を取ることによって
\( T \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \Longrightarrow \mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \\[2pt] \)
が得られます.よって,$T$ は$\Pi_1^\mathcal{D}$-健全です. ■

補足 上記の「ド・モルガンの法則」は, 算術 $T$ における証明の中で述語論理のド・モルガンの法則を利用することによって $\forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$ から $\neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x}))$ が演繹できることを示しています.上ではこれの対偶を利用しています. ■

上の定理と定理3.4から次の系が直ちに得られます.

系 3.9.1
計算的枚挙可能かつ$\Delta_0^\mathcal{D}$-完全かつ無矛盾な算術は意味論的に不完全です. ■

補足  上記の条件を満たす算術が「構文論的に」不完全なのかどうかは筆者には分かりません.

$\Delta_0^\mathcal{D}$-完全性 & $\Sigma_1^\mathcal{D}$-健全性

定義 3.10
算術 $T$ が $\Sigma_1^\mathcal{D}$-健全 であるということを, が成り立つこととします.この条件は
\( \mathcal{D}^T_\exists \subseteq \mathcal{D}^\mathcal{N}_\exists \)
が成り立つことと等価です. ■

定理 3.11
$\Delta_0^\mathcal{D}$-完全かつ$\Sigma_1^\mathcal{D}$-健全な任意の算術 $T$ に対して次が成り立ちます.
  1. $T$ は無矛盾です.従ってまた,$T$ は $\Pi_1^\mathcal{D}$-健全でもあります.
  2. $ \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T = \mathcal{D}-(\,\mathcal{D}^T_\exists \cup \mathcal{D}^T_\forall\,)$

          $ = \{ \langle p,q \rangle \in \mathcal{D} \mid T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \} $

証明  (1) 任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} & \mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & \mathcal{N} \not\models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{($\Sigma_1^\mathcal{D}$-健全性)}\\ \end{array} \)

つまり,任意のD方程式 $\langle p,q \rangle \in \mathcal{D}_\forall^\mathcal{N}$ に対して $T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x}))$ が成り立ちます.従って,例えば $\langle x,x+\widehat{1} \rangle \in \mathcal{D}_\forall^\mathcal{N}$ なので, $T \not\vdash \exists{x}(x = x + \widehat{1})$ が成り立ちます,よって,$T$ は無矛盾です. 従ってまた,定理3.9より $T$ は $\Pi_1^\mathcal{D}$-健全でもあります.

 (2) $\Sigma^\mathcal{D}_1$-完全性(補題3.8)と$\Sigma^\mathcal{D}_1$-健全性より が成り立ちます. さらに,$\mathcal{D}^\mathcal{N}_\exists$ と $\mathcal{D}^\mathcal{N}_\forall$ の定義より $\mathcal{D} = \mathcal{D}^\mathcal{N}_\exists \cup \mathcal{D}^\mathcal{N}_\forall$ かつ $\mathcal{D}^\mathcal{N}_\exists \cap \mathcal{D}^\mathcal{N}_\forall = \emptyset$ なので が成り立ちます.これらの事実から

\( \begin{array}{lcl} \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}^T_\forall &=& (\mathcal{D}-\mathcal{D}^\mathcal{N}_\exists) - \mathcal{D}^T_\forall \\ &=& \mathcal{D} - (\mathcal{D}^\mathcal{N}_\exists \cup \mathcal{D}^T_\forall) \\ &=& \mathcal{D}-(\,\mathcal{D}^T_\exists \cup \mathcal{D}^T_\forall\,) \end{array} \)

が得られます.従って, $\mathcal{D}^T_\exists$ と $\mathcal{D}^T_\forall$ の定義(とド・モルガンの法則)から

\( \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T = \{ \langle p,q \rangle \in \mathcal{D} \mid T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \} \)

となります. ■

余談 上記の(2)は次のように形式的に証明することもできます. 任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して:

\( \begin{array}{lll} & \langle p,q \rangle \in \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T \\ \iff & \mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(各集合の定義)} \\ \iff & \mathcal{N} \not\models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(真理条件の定義)} \\ \iff & T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{($\Sigma_1^\mathcal{D}$-健全性と$\Sigma_1^\mathcal{D}$-完全性)} \\ \iff & T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) ~\text{かつ}~ T \not\vdash \neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{(ド・モルガンの法則)} \\ \end{array} \)

なお,上記の$\Sigma_1^\mathcal{D}$-完全性は補題3.8によります. ■

系 3.11.1
計算的枚挙可能かつ$\Delta_0^\mathcal{D}$-完全かつ$\Sigma_1^\mathcal{D}$-健全な算術 $T$ は構文論的に不完全です.

証明  系2.5より $\mathcal{D}_\forall^\mathcal{N}$ は計算的枚挙可能ではありません. 一方,$T$ が計算的枚挙可能なので $\mathcal{D}_\forall^T$ は計算的枚挙可能です. 従って, $\mathcal{D}_\forall^\mathcal{N} \not= \mathcal{D}_\forall^T$ が成り立ちます.更に,定理3.11(1)より $T$ は$\Pi_1^\mathcal{D}$-健全なので, $\mathcal{D}_\forall^T \subseteq \mathcal{D}_\forall^\mathcal{N}$ が成り立ちます. よって, $\mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T \not= \emptyset$ が成り立ちます. これと定理3.11(2)より $T$ は構文論的に不完全であることが分かります. ■

$\Delta_0^\mathcal{D}$-完全性 & $\omega^\mathcal{D}$-無矛盾性

定義 3.12
算術 $T$ が $\omega^\mathcal{D}$-矛盾 であるということを が成り立つこととします.$T$ が$\omega^\mathcal{D}$-矛盾でないとき,$T$ は $\omega^\mathcal{D}$-無矛盾 であると言います.参考までに言うと,$T$ が$\omega^\mathcal{D}$-無矛盾であるとは, が成り立つときを言います. ■

定理 3.13
$\Delta_0^\mathcal{D}$-完全な任意の算術 $T$ に対して次が成り立ちます.
$T$ は$\Sigma_1^\mathcal{D}$-健全である $\iff$ $T$ は$\omega^\mathcal{D}$-無矛盾である

証明  ($\Longrightarrow$)  $T$ を$\Sigma_1^\mathcal{D}$-健全とします. このとき,任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} & T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & \mathcal{N} \models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{($\Sigma_1^\mathcal{D}$-健全性)} \\ \Longrightarrow & \mathcal{N} \models p(\widehat{\vec{a}})=q(\widehat{\vec{a}}) ~~\text{for some $\vec{a} \in \mathbb{N}^n$} & \text{(真理条件の定義)} \\ \Longrightarrow & T \vdash p(\widehat{\vec{a}})=q(\widehat{\vec{a}}) ~~\text{for some $\vec{a} \in \mathbb{N}^n$} & \text{($\Delta_0^\mathcal{D}$-完全性)} \\ \Longrightarrow & T \not\vdash \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~~\text{for some $\vec{a} \in \mathbb{N}^n$} & \text{( 無矛盾性 via 定理3.11(1) )} \\ \end{array} \)

よって,$T$ は$\omega^\mathcal{D}$-無矛盾です.

 ($\Longleftarrow$)  $T$ を$\omega^\mathcal{D}$-無矛盾とします. このとき,任意のD方程式 $\langle p,q \rangle \in \mathcal{D}$ に対して次が成り立ちます.

\( \begin{array}{lll} & \mathcal{N} \not\models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & \mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(真理条件の定義)} \\ \Longrightarrow & \mathcal{N} \models \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~~\text{for all $\vec{a} \in \mathbb{N}^n$} & \text{(真理条件の定義)} \\ \Longrightarrow & T \vdash \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~~\text{for all $\vec{a} \in \mathbb{N}^n$} & \text{($\Delta_0^\mathcal{D}$-完全性)} \\ \Longrightarrow & T \not\vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) & \text{($\omega^\mathcal{D}$-無矛盾性)} \\ \end{array} \)

この対偶を取ることによって

\( T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \Longrightarrow \mathcal{N} \models \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \\ \)

が得られます. よって,$T$ は$\Sigma_1^\mathcal{D}$-健全です. ■

この定理と系3.11.1より次の系が直ちに得られます.

系 3.13.1
計算的枚挙可能かつ$\Delta_0^\mathcal{D}$-完全かつ$\omega^\mathcal{D}$-無矛盾な算術 $T$ は構文論的に不完全です. ■

十分条件のまとめ

$\Delta_0^\mathcal{D}$-完全な算術に関して, これまで扱ってきた諸条件の関係性をまとめると次のようになります.

\( \begin{array}{clcr} & \text{$\Pi_1^\mathcal{D}$-健全性} ~\iff~ \text{無矛盾性} &~~~~& \cdots\cdots(1) \\ \Longleftarrow & \text{$\Sigma_1^\mathcal{D}$-健全性} ~\iff~ \text{$\omega^\mathcal{D}$-無矛盾性} &~~~~& \cdots\cdots(2) \\ \end{array} \)

下記の命題は,上の条件(1)から条件(2)が導けないことを示しています.

命題 3.14(無矛盾だが$\omega^\mathcal{D}$-矛盾な算術)
$T$ を計算的枚挙可能かつ$\Delta_0^\mathcal{D}$-完全かつ$\Pi_1^\mathcal{D}$-健全な算術とします.このとき,定理3.4より$\mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T \not= \emptyset$ が成り立ちます.そこで,D方程式 $\langle p,q \rangle \in \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T$ を任意に取ってきて
$T_1 = T \cup \{ \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \}$
とおきます.このとき,$T_1$ は無矛盾だが$\omega^\mathcal{D}$-矛盾な算術になります.

証明  $T_1$ と上記のD方程式 $\langle p,q \rangle \in \mathcal{D}_\forall^\mathcal{N} - \mathcal{D}_\forall^T$ に対して次が成り立ちます.

\( \begin{array}{lll} & T_1 \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & T \cup \{ \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \} \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{($T_1$ の定義)}\\ \Longrightarrow & T \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \rightarrow \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(演繹定理)} \\ \Longrightarrow & T \vdash \neg\exists{\vec{x}}(p(\vec{x})=q(\vec{x})) \lor \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(含意の定義)} \\ \Longrightarrow & T \vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) & \text{(ド・モルガンの法則や$\lor$-除去)} \\ \end{array} \)

一方, $\langle p,q \rangle \not\in \mathcal{D}_\forall^T$ なので $T \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$ が成り立ちます.これと上記の対偶から, $T_1 \not\vdash \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$ が得られます.よって, $T_1$ は無矛盾です.

  次に,
(a)  $T_1 \vdash \exists{\vec{x}}(p(\vec{x})=q(\vec{x}))$
が成り立つことは明らかです.さらに $\langle p,q \rangle \in \mathcal{D}_\forall^\mathcal{N}$ なので
$\mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x}))$
が成り立ち,その上さらに
\( \begin{array}{lll} & \mathcal{N} \models \forall{\vec{x}}\neg(p(\vec{x})=q(\vec{x})) \\ \Longrightarrow & \mathcal{N} \models \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~\text{for all $\vec{a} \in \mathbb{N}^n$} & \text{(真理条件の定義)} \\ \Longrightarrow & T \vdash \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~\text{for all $\vec{a} \in \mathbb{N}^n$} & \text{($\Delta_0^\mathcal{D}$-完全性)} \\ \Longrightarrow & T_1 \vdash \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}})) ~\text{for all $\vec{a} \in \mathbb{N}^n$} & \text{(自明)} \\ \end{array} \)
が成り立つので,
(b)  $T_1 \vdash \neg(p(\widehat{\vec{a}})=q(\widehat{\vec{a}}))$ for all $\vec{a} \in \mathbb{N}^n$
が成り立ちます.よって,$T_1$ は$\omega^\mathcal{D}$-矛盾です. ■

D方程式の窓から見た景色
数値的な計算(変数を含まない等式や非等式の証明)が正しく行えて,無矛盾な算術のことを,仮に,「合理的な算術」と呼ぶことにします.$\Delta^\mathcal{D}_0$-完全性は数値的な計算が正しく行えることの必要条件と考えることができます.従って,ここで言う合理的な算術は$\Delta^\mathcal{D}_0$-完全であると言えます.従って,補題3.8より,合理的な算術は$\Sigma^\mathcal{D}_1$-完全でもあります. さらに,無矛盾性より,$\Pi^\mathcal{D}_1$-健全でもあります.

以上をまとめると,D方程式全体 $\mathcal{D}$ と合理的な算術 $T$ に関して次が成り立つことになります. これらの関係性を図示すると次のようになります. この図は,D方程式という窓から合理的な算術を眺めたときの景色を示しています.

D方程式の見取り図
D方程式に基づく意味論的不完全性は $\mathcal{D}^T_\forall \subsetneq \mathcal{D}^\mathcal{N}_\forall$ であることから必ず成り立つと言えます.一方,構文論的不完全性(注:あくまでD方程式に基づく構文論的不完全性)は,上図の斜線部が空でないときに成立します.言い方を変えると, $\mathcal{D}^T_\exists$ は $\mathcal{D}^\mathcal{N}_\forall - \mathcal{D}^T_\forall$ の領域へその勢力を伸ばしていく可能性があるのですが,その勢力を途中で抑えることができれば構文論的な不完全性が成立することになります.その勢力を抑える一つの条件は $\Sigma^\mathcal{D}_1$-健全性または$\omega^\mathcal{D}$-無矛盾性です. これらの条件は $\mathcal{D}^T_\exists$ の勢力を $\mathcal{D}^\mathcal{N}_\exists$(上図の赤枠) の中に閉じ込めてしまいます.それゆえに構文論的不完全性が成立します. しかしながら,少なくとも筆者にはこれら以外の条件は分かりません. 計算理論的な観点から言えば, $\mathcal{D}^T_\forall$ や $\mathcal{D}^T_\exists$ や $\mathcal{D}^T_\forall \cup \mathcal{D}^T_\exists$ など(の一つ)が計算不可能であることが示せればよいのですが,そういったことが示せるのかどうかも分かりません.こういったことを理解すべく,勉強を続けていこうと思います.
(おしまい)