全てのGödel文は自己の無矛盾性を表す文と同値
定義と仮定
理論$ TのGödel文とは以下を満たす$ \Sigma_1文$ Gのことである． $ \mathsf{PA} \vdash G \leftrightarrow \lnot\mathsf{Pr}_T(\overline{\ulcorner G \urcorner})
任意の$ \Sigma_1文$ \sigmaに対し
$ \mathsf{PA} \vdash \sigma \to \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner})
主張.1
1. 理論$ TのGödel文は無数に存在する．
主張1の証明
主張2,3
理論$ TのGödel文$ G,G'，理論$ Tの無矛盾性を表す文$ \mathsf{Con}_Tとする．
2. $ T \vdash G \leftrightarrow \mathsf{Con}_T
3. $ T \vdash G \leftrightarrow G'
補題
1. 任意の文$ \varphiに対し$ \mathsf{PA} \vdash \lnot\mathsf{Pr}_T(\overline{\ulcorner \varphi \urcorner}) \to \mathsf{Con}_T
証明
1. $ T \vdash \varphi \to \bot
2. 導出可能性D1より$ \mathsf{PA} \vdash \mathsf{Pr}_T(\ulcorner \bot \to \top \urcorner)
3. 導出可能性D2と1より$ \mathsf{PA} \vdash \mathsf{Pr}_T(\ulcorner \bot \urcorner) \to \mathsf{Pr}_T(\ulcorner \varphi \urcorner)
4. 3の対偶より$ \mathsf{PA} \vdash \lnot\mathsf{Pr}_T(\ulcorner \varphi \urcorner) \to \lnot\mathsf{Pr}_T(\ulcorner \bot \urcorner)
5. 定義$ \mathsf{Con}_T \equiv \lnot\mathsf{Pr}_T(\ulcorner \bot \urcorner)より$ \mathsf{PA} \vdash \lnot\mathsf{Pr}_T(\ulcorner \varphi \urcorner) \to \mathsf{Con}_T
2. 任意の$ TのGödel文$ Gに対し$ T \vdash \mathsf{Con}_T \to \lnot\mathsf{Pr}_T(\overline{\ulcorner G \urcorner})
証明
1. $ \lnot Gは$ \Sigma_1文であるので，形式化されたΣ₁完全性定理より$ T \vdash \lnot G \to \mathsf{Pr}_T(\overline{\ulcorner \lnot G \urcorner}) 2. $ Gの定義より$ T \vdash \mathsf{Pr}_T(\overline{\ulcorner G \urcorner}) \to \lnot G
3. 1,2より$ T \vdash \mathsf{Pr}_T(\overline{\ulcorner G \urcorner}) \to \mathsf{Pr}_T(\overline{\ulcorner \lnot G \urcorner})
4. 以下の補題より$ T \vdash \mathsf{Con}_T \to \lnot\mathsf{Pr}_T(\overline{\ulcorner G \urcorner})
$ \mathsf{PA}の拡大理論$ Uと任意の文$ \varphiに対し，$ U \vdash \mathsf{Pr}_T(\overline{\ulcorner \varphi \urcorner}) \to \mathsf{Pr}_T(\overline{\ulcorner \lnot \varphi \urcorner}) \implies U \vdash \mathsf{Con}_T \to \lnot\mathsf{Pr}_T(\overline{\ulcorner \varphi \urcorner})
主張2の証明
1. 補題1を$ Gに適用して$ \mathsf{PA} \vdash \lnot\mathsf{Pr}_T(\overline{\ulcorner G \urcorner}) \to \mathsf{Con}_T
2. 補題2と合わせて$ T \vdash \lnot\mathsf{Pr}_T(\overline{\ulcorner G \urcorner}) \leftrightarrow \mathsf{Con}_Tを得る．
3. $ Gの定義より$ T \vdash G \leftrightarrow \mathsf{Con}_T．❏ 主張3の証明
参考文献