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

Remark

次を満たす$ \varphiが存在しなければ，$ Tは$ \omega無矛盾という．

1. $ T \vdash \exists_y \varphi(\vec{x},y)

2. 任意の自然数$ yに対し，$ T \vdash \lnot \varphi(\vec{\overline{x}}, \overline{y})

Remark

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

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

proof

1. $ T \vdash Gを仮定する．

2. $ T \vdash G \implies T \vdash \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})より$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})

Remark$ T \vdash G \implies T \vdash \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})は通常の証明可能性述語の条件として要請される．導出可能性条件のD1

3. Gödel文の定義より$ T \vdash G \leftrightarrow \lnot \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})．したがって$ T \vdash \lnot \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})

4. $ Tの無矛盾性より破綻．❏

1. $ T \vdash \lnot Gを仮定する．

2. Gödel文の定義より$ T \vdash \lnot G \leftrightarrow \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})．したがって$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})

3. $ Tが$ \omega無矛盾で$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})のとき，$ T \vdash G

Lem

$ Tが$ \omega無矛盾で$ T \vdash \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner})のとき，$ T \vdash \sigma

$ T \not\vdash\sigmaとすると，任意の$ yに対し$ (\ulcorner \sigma \urcorner,y) \notin \mathsf{Proof}_T

$ \mathsf{Proof}_Tは再帰的で，表現定理より任意の$ yに対し$ \mathsf{Q} \vdash \lnot \mathrm{Proof}_T(\overline{\ulcorner \sigma \urcorner}, \overline{y})

すなわち任意の$ yに対し$ T \vdash \lnot \mathrm{Proof}_T(\overline{\ulcorner \sigma \urcorner}, \overline{y})

$ \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner}) \equiv \exists_y\mathrm{Proof}_T(\overline{\ulcorner \sigma \urcorner}, \overline{y})

前提より$ T \vdash \exists_y\mathrm{Proof}_T(\overline{\ulcorner \sigma \urcorner}, \overline{y})

これらより$ Tは$ \omega無矛盾性に反する．したがって$ T \vdash \sigma．

4. $ T \vdash Gはaに反する．❏．

モチベーション

Gödel-Rosserの第1不完全性定理ではω無矛盾性を無矛盾性に弱めることが出来ることが示される．

そのため区別するためにわざわざω無矛盾版のと断っている．