Gödel-Rosserの第1不完全性定理

参考文献

数学基礎論序論(本)パートBより．

なお菊池誠; "不完全性定理"にはもう少し細かく書いてある

主張

Robinson算術$ \mathsf{Q}の再帰的拡大理論$ Tが無矛盾なら，$ Tは不完全．

具体的には，理論$ TのRosser文$ Rが存在し，$ T \not\vdash Rかつ$ T \not\vdash \lnot R

注意

Gödelのω無矛盾版の第1不完全性定理

Robinson算術$ \mathsf{Q}の再帰的拡大理論を$ Tとし，$ TのGödel文を$ Gとする．

a. $ Tが無矛盾なら，$ T \not \vdash \lnot G

b. $ Tがω無矛盾なら，$ T \not \vdash \lnot G

ω無矛盾性は無矛盾性より強い（$ Tがω無矛盾ならば$ Tは無矛盾）ので纏めて

$ Tがω無矛盾なら$ Tは不完全．

以下のテクニックはRosserのトリックと言われることもある．

前提

$ (x,y) \in \mathsf{Proof}_T$ \iff$ E_xは論理式で$ E_yは$ Tでの証明．

$ \mathsf{Proof}_Tを表現する$ \Sigma_1論理式$ \mathrm{Proof}(x,y)が表現定理より構成される．

Gödelの不動点補題

$ \mathsf{Q} \vdash \Psi \leftrightarrow \Phi(\overline{\ulcorner \Psi \urcorner})

また，$ \Phi(v_0)が$ \Sigma_n論理式なら$ \Psiは$ \Sigma_n文であり，$ \Pi_n論理式なら$ \Piは$ \Sigma_n文である．

Def: $ \mathsf{Dispr}_T

$ \mathsf{Q}の再帰的拡大理論$ Tとする．

反証を表す2項関係 $ \mathsf{Dispr}_Tを以下のように定義する．

$ (x,y) \in \mathsf{Dispr}_T$ \iff$ E_xは論理式で，$ E_yは$ Tでの$ \lnot E_xの証明．

注意

以下は証明なしで用いる．

$ \mathsf{Dispr}_Tは再帰的関係．

したがって$ \mathsf{Dispr}_Tを表現する$ \mathrm{Dispr}_T(x,y)が$ \Pi_1論理式として存在する．

表現定理より．

Def: Rosser証明可能性述語

$ \mathrm{Pr}^*_T(x) \equiv \exists_y \lbrack \mathrm{Proof}(x,y) \land \forall_{z<y}\lbrack \lnot \mathrm{Dispr}_T(x,z)\rbrack \rbrack

このとき，$ \mathrm{Pr}^*_Tは$ \Sigma_1論理式．

$ E_xの証明のGödel数は$ yとして存在し，$ y以下のGödel数で$ \lnot E_xの証明となるものは存在しない．

$ \mathrm{Pr}^*_TはRosser証明可能性述語と呼ぶ．

Lem

$ Tが無矛盾な$ \sf Qの再帰的拡大，

a. $ T \vdash \varphi \implies T \vdash \mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner})

proof

1. $ T \vdash \varphiを仮定．

2. このとき，$ \mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner})は正しい$ \Sigma_1文となる．SnO2WMaN.icon？

3. よってΣ₁完全性定理より$ \mathcal{N} \models \mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner}) \implies \mathsf{Q} \vdash \mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner})

4. よって$ T \vdash \mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner})

Remark: 導出可能性条件D1.

b. $ T \vdash \lnot \varphi \implies T \vdash \lnot\mathrm{Pr}^*_T(\overline{\ulcorner \varphi \urcorner})

proof

1. $ T \vdash \lnot\varphiを仮定

2. 1より，$ \lnot\varphiの証明のGödel数として$ nが存在する．

3. 定義より，$ (\ulcorner \lnot\varphi \urcorner,n) \in \mathsf{Dispr}_T

4. $ Tの無矛盾性より$ T \not\vdash \varphi．

5. したがって任意の$ iに対して$ (\ulcorner \varphi \urcorner, i) \notin \mathsf{Proof}_T

6. 3より$ \mathsf {Q} \vdash \mathrm{Dispr}_T( \overline{\ulcorner \lnot\varphi \urcorner}, \overline{n})

7. 4より任意の$ i < nで$ \mathsf {Q} \vdash \lnot \mathrm{Proof}_T( \overline{\ulcorner \varphi \urcorner}, \overline{i})

8. 6,7より$ \mathsf{Q} \vdash \forall y\lbrack \lnot \mathrm{Proof}_T(\ulcorner \varphi \urcorner, y) \lor \exists_{z < y}\lbrack \mathrm{Dispr}_T(\ulcorner \lnot\varphi \urcorner, y) \rbrack \rbrack

Remarkこれはあまり自明ではない．

9. 8とde Morganの法則より$ \mathsf{Q} \vdash \exists y\lbrack \lnot\mathrm{Proof}_T(\ulcorner \varphi \urcorner, y) \land \forall_{z < y}\lbrack \lnot \mathrm{Dispr}_T(\ulcorner \lnot\varphi \urcorner, y) \rbrack \rbrack

Def: Rosser文

$ \mathsf{Q}の再帰的拡大理論$ Tとする．

$ \lnot \mathrm{Pr}^*_T(x)に対して不動点補題を適用することで得られる，以下を満たす構成される文$ Rを理論$ TのRosser文と呼ぶ．

$ T \vdash R \leftrightarrow \lnot \mathrm{Pr}^R_T(\overline{\ulcorner R \urcorner})

Remark上の議論より確かに存在する．

Thm: Gödel-Rosserの第1不完全性定理

$ \mathsf{Q}の再帰的拡大理論$ Tが無矛盾なら，理論$ TのRosser文$ Rが存在し，$ T \not\vdash Rかつ$ T \not\vdash \lnot R．

proof

$ T \vdash Rとすると

Lem aより$ T \vdash \mathrm{Pr}^*_T(\overline{\ulcorner R \urcorner})

Rosser文の定義より$ T \vdash \lnot \mathrm{Pr}^*_T(\overline{\ulcorner R \urcorner})

よって無矛盾性に反する．$ T \not \vdash R