Gödelの第1不完全性定理
Thm: 現代でよく普及しているバージョン
Robinson算術$ \mathsf{Q}の再帰的拡大理論を$ Tとし，$ TのGödel文を$ Gとする．
a. $ Tが無矛盾なら，$ T \not \vdash G
b. $ TがΣ₁健全なら，$ T \not \vdash \lnot G
Remark
任意の$ \Sigma_1文$ \sigmaについて，$ T \vdash \sigma \implies \mathcal{N} \models \sigmaが成り立つとき，$ Tは$ \Sigma_1健全であるという．
Remark
$ TがΣ₁健全なら$ Tは不完全．
Σ₁健全性は無矛盾性より強い条件より．
proof
a.
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の無矛盾性より破綻．❏
b.
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. $ \Sigma_1健全性より$ \mathcal{N} \models \mathrm{Pr}_T(\overline{\ulcorner G \urcorner})
4. $ \mathcal{N} \models \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner}) \implies T \vdash \sigmaと3より，$ T \vdash G．
Remark文$ \sigmaに対し，$ \mathcal{N} \models \mathrm{Pr}_T(\overline{\ulcorner \sigma \urcorner}) \implies T \vdash \sigmaは前提とする．
5. a.に反する．よって破綻．❏
Remark
Gödelのオリジナルのバージョンでは，$ \Sigma_1健全性ではなくω無矛盾性を要請していた．すなわち以下のGödelのω無矛盾版の第1不完全性定理が最初の主張だった．
もっといえばそもそもベースの議論はRobinson算術でもPeano算術でもなかった（Principia MathemeticaをGödelが使いやすく改良した体系である）ゲーデルに挑むなどを参照．
Thm: 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
J. Barkley Rosserがω無矛盾性を単に無矛盾性に弱めたものが，Gödel-Rosserの第1不完全性定理である．
Robinson算術$ \mathsf{Q}の再帰的拡大理論を$ Tとし，$ Tが無矛盾なら$ Tは不完全．
参考文献
数学基礎論序論(本) パートB
菊池誠; "不完全性定理"
数学における証明と真理 様相論理と数学基礎論 第2部
元論文
K. Gödel; "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme. I."