自然数という概念を理解する会

「自然数」という概念を理解している人は、自然数の命題が正しかったり、誤っていたりするときに、その理由を挙げられるはず。

つまり、自然数の命題の真偽に対して、適切な正当化を行えるはずです。

ということで、「自然数」という概念の理解に、
・何が自然数に含まれるか
だけでなく、
・どういう命題が真となるか
みたいな要素を多少なりとも適切に判定できることが必要だと考えたときに、どういう事象に遭遇するかを書きます。

元ネタはダメットの「ゲーデルの定理の哲学的意義」です*1が、当然ちゃんと理解していないし、ロジックの知識も大してないです。

1. ゲーデル文
- 1-1. 第一不完全性定理
- 1-2. ゲーデル文の真偽
2. システムを拡大していく
3. まとめ

1. ゲーデル文

1-1. 第一不完全性定理

とりあえず、スタート地点をペアノ算術（PA）としておきます。

PAの証明可能性述語 $Pr_{PA}$ を定義できたとします*2。

$Pr_{PA}$ の性質として、

$\vdash_{PA} \psi$ ならば、 $\vdash_{PA} Pr_{PA} (\overline{\lceil \psi \rceil})$

PAが $\omega$ 無矛盾かつ $\vdash_{PA} Pr_{PA} (\overline{\lceil \psi \rceil})$ ならば、 $\vdash_{PA} \psi$

みたいなのが成り立っているとします。

で、

$\vdash_{PA} G_{PA} \leftrightarrow \neg Pr_{PA} (\overline{\lceil G_{PA} \rceil})$

というのを満たすような文 $G_{PA}$ を定義できるとします*3。

このとき、

PAが $\omega$ 無矛盾であるならば、 $G_{PA}$ も $\neg G_{PA}$ も証明できない

となります（第一不完全性定理）。

このように作られた文 $G_{PA}$ が、ゲーデル文と呼ばれるものです。

1-2. ゲーデル文の真偽

さて、ゲーデル文 $G_{PA}$ は、実際のところ真です。

と書くと、怒られそうなので、真であることが明示できるように、PAに真理述語 $Tr$ を付け加えてみます。

$Tr$ は、論理式（のゲーデル数）を引数に取って、 $Tr (\overline{\lceil \psi \rceil})$ で、「命題 $\psi$ は真である」という内容が表現されるような述語としましょう。

これを達成するため、PAに以下の公理を付け加えます*4。

$(1) \quad \forall n ,k [AtomSent_{PA}(\overline{\lceil n = k \rceil}) \to (Tr(\overline{\lceil n = k \rceil}) \leftrightarrow EQ(n, k))$ ]

$(2) \quad \forall x [Sent(x) \to (Tr(\dot\neg x) \leftrightarrow \neg Tr(x))$ ]

$(3) \quad \forall x, y [(Sent(x) \land Sent(y)) \to (Tr(x \dot\land y) \leftrightarrow Tr(x) \land Tr(y))$ ]

$(4) \quad \forall x, y [(Sent(x) \land Sent(y)) \to (Tr(x \dot\lor y) \leftrightarrow Tr(x) \lor Tr(y))$ ]

$(5) \quad \forall x(v) [Sent(x(v)) \to (Tr(\forall v x(v)) \leftrightarrow \forall t Tr(x(\dot{t})))$ ]

$(6) \quad \forall x(v) [Sent(x(v)) \to (Tr(\exists v x(v)) \leftrightarrow \exists t Tr(x(\dot{t})))$ ]

$(7) \quad \forall x [Sent(x) \to (Pr_{PA}(x) \to Tr(x))$ ] （反映原理）

ただし、
・ $EQ(n, k)$ は、項 $n, k$ の表現する値が等しくなっている

・ $AtomSent_{PA} (\overline{\lceil \psi \rceil})$ は、 $\psi$ がPAの原子論理式である

・ $Sent (\overline{\lceil \psi \rceil})$ は、 $\psi$ が論理式である

・量化の範囲とかドットとかについては、こう、上手く解釈してください･･･

さらに、

数学的帰納法は $Tr$ を含む論理式にも使用可能

としておきましょう。

このようにして作った体系を $CT_0$ と呼ぶことにします。

この $CT_0$ は、

「 $\psi$ が真である」のは、 $\psi$ のとき、そのときに限る

のような、「真である」について成り立っていて欲しい性質をたいぶ満たします。

というか、たぶんPAの論理式 $\psi_{PA}$ に対して、

$\vdash_{CT_0} Tr (\overline{\lceil \psi_{PA} \rceil}) \leftrightarrow \psi_{PA}$

となっているように見えます*5。

なお、 $Tr$ の引数に $Tr$ を使った論理式が入るパターンの場合には、(1)の $Tr$ を外す作業ができなくなるため、

$Tr (\overline{\lceil \psi \rceil}) \to \psi$

が、必ずしも成り立っているわけではありません*6。したがって、嘘つきのパラドックスのような論理式から矛盾を導くことができなくなっています*7。

さて、ここで反映原理に、 $0=1$ という文を放り込んでみましょう。

$0=1$ はPAの文であるので、

$\vdash_{CT_0} Pr_{PA}(\overline{\lceil 0=1 \rceil}) \to Tr(\overline{\lceil 0=1 \rceil})$

です。 $Tr$ の同値関係を使って、 $Tr$ を外してやると、

$\vdash_{CT_0} Pr_{PA}(\overline{\lceil 0=1 \rceil}) \to 0=1$

となります。対偶を取ると、

$\vdash_{CT_0} 0 \neq 1 \to \neg Pr_{PA}(\overline{\lceil 0=1 \rceil})$

であり、 $0 \neq 1$ なんて当然証明できるので、

$\vdash_{CT_0} \neg Pr_{PA}(\overline{\lceil 0=1 \rceil})$

が結論されます。

これに、第二不完全性定理を導くときのやつ*8

$\vdash_{CT_0} \neg Pr_{PA}(\overline{\lceil 0=1 \rceil}) \to \neg Pr_{PA}(\overline{\lceil G_{PA} \rceil})$

$\vdash_{CT_0} \neg Pr_{PA}(\overline{\lceil 0=1 \rceil}) \to G_{PA}$

から、

$\vdash_{CT_0} G_{PA}$

とできるし、 $G_{PA}$ は、PA上で定義できていたので、

$\vdash_{CT_0} Tr(\overline{\lceil G_{PA} \rceil})$

とできる。

つまり、ゲーデル文は真である。

･･･ $CT_0$ で。

2. システムを拡大していく

2-1. CT0の性質

$CT_0$ は、二階算術の $ACA$ と同等の証明能力を持つことが示されています*9。

$ACA$ は、逆数学とかでよく見る $ACA_0$ の数学的帰納法を、フルの数学的帰納法にしたものです。

このシステムは上で見たように、 $\vdash_{CT_0} \neg Pr_{PA}(\overline{\lceil 0=1 \rceil})$ なので、PAの無矛盾性を証明できます。

ということで、 $CT_0$ や $ACA$ は、PAよりも証明力が強いシステムということになっています。証明論的順序数を調べると、PAは $\epsilon_0$ で、 $ACA$ は $\epsilon_{\epsilon_0}$ らしいです*10。

ほかにどんな命題が新たに証明可能となっているでしょうか。

巨大数Wikiの「証明論的順序数」を見ると、証明論的順序数はそこまでの整列順序を示せるというもののように見えます*11。

ってことは、たぶん $CT_0$ において、「 $\epsilon_0$ までの超限帰納法」は使ってもいいということになるので、グッドスタインの定理やヒドラゲームの停止性なども示せるということになるのだと思います*12。

2-2. CT0の先

$CT_0$ について、 $Pr_{CT_0}$ を定めると、

$\vdash_{CT_0} G_{CT_0} \leftrightarrow \neg Pr_{CT_0} (\overline{\lceil G_{CT_0} \rceil})$

という $G_{CT_0}$ を考えることができそうです。不完全性定理から、この $G_{CT_0}$ は、 $CT_0$ からは証明ができない命題ということになります。

で、 $CT_0$ についての不完全性定理が成り立つことを起点として、

→新しい反映原理として、

$\forall x [Sent(x) \to (Pr_{CT_0}(x) \to Tr(x))$ ]

を加えた新理論 $CT_1$ を定める

→ $\vdash_{CT_1} \neg Pr_{CT_0}(\overline{\lceil 0=1 \rceil})$ を示す

→ $CT_1$ 上で、 $G_{CT_0}$ や $CT_0$ の無矛盾性を示せる

というように、1-2でやったのと同じような流れで理論を拡大して*13、前の理論の無矛盾性を示すことができるはずです*14。

で、以下同じように、

$CT_1$ をベースに $CT_2$ を作り

$CT_2$ をベースに $CT_3$ を作り

･･･

という無限の拡大プロセスを考えることができます。

ダメットは、

一たびある体系が定式化されると、われわれはそれを参照することによって、その体系の真なる言明である、という性質のような、その体系の中で表現可能でない新しい性質を定義できる。ここからわれわれは、そのような新しい性質に帰納法を適用することによって、その体系の中では証明可能でないところの結論に到達できるのである。

と述べています*15が、たぶん上のような状況を想定していたのだと思います。

「ロビンソン算術でも不完全性定理は成り立つのに、なぜそんなに帰納法を強調するの？」と思っていましたが、強力な $CT_0$ を作るには（新しく導入した述語 $Tr$ も含めた）フルの帰納法が必要だったからなのでしょう。

で、そのちょっと前では、

(...)「自然数」という表現の理解は、すべての自然数についてあることが真であると主張する根拠として何が認められるのか、というその規準を決定するには不十分であろう。そしてゲーデルの定理によって限りなく拡張し得ることが示されるのは、まさしくそのような根拠の概念である。すべての自然数についてある主張をするための、一組の根拠を明確に特徴付けても、そのつどその自然な拡張が存在するであろう。

と書いています*16。

「根拠を持って真だと言える」ときの根拠を、公理系から示せることと同一視してしまうと、肝心の公理系がPA→ $CT_0$ → $CT_1$ →･･･と、際限なく拡大していけるということになってしまいます。

つまり、「自然数」の意味を、自然数を使った主張をするための根拠を把握していることまで含むと捉えると、ここに曖昧さのようなものが存在するという結論となります。