ゲーデルの不完全性定理
¬ P r o v a b l e ( b ) ⇒ ¬ P r o v a b l e ( n p m m ) {\displaystyle \lnot Provable(b)\Rightarrow \lnot Provable(npmm)}
が自然数論の体系内で証明可能なことがわかる。したがって、仮定および ¬ P r o v a b l e A R G ( m , m ) ⇔ ¬ P r o v a b l e ( n p m m ) {\displaystyle \lnot ProvableARG(m,m)\Leftrightarrow \lnot Provable(npmm)} から
¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)}
が自然数論の体系内で証明可能なことがわかる。第一不完全性定理の所で示したように、 ¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)} が証明可能だと、矛盾が証明される。したがって矛盾が証明されないならば、 ¬ P r o v a b l e ( b ) {\displaystyle \lnot Provable(b)} は証明されない。
注意
形式的体系 S と S' に対して(言語を適当に拡張した)S' が S を含むとは、S の論理式全体の集合Fml(S)から S' の論理式全体の集合Fml(S')への次のような写像T:Fml(S)→Fml(S')が存在するときを言う:φ∈Fml(S)がS で証明できるときT(φ)は S' で証明できる。このTはしばしば「翻訳」と呼ばれる。この意味でペアノ算術PAはツェルメロ=フレンケル集合論ZFCに含まれる。
「初等的な自然数論」について、ゲーデル自身はペアノの公理と原始帰納法による関数の定義を前提に自然数論の体系を構築した (Gödel 1931)。この体系は、加法・乗法・べき乗・階乗・順序関係などを帰納的に定義する十分な表現力を持っている。それぞれの定理の前提条件は、ロビンソン算術を含む半決定可能な理論(第一)、 I Σ 1 {\textstyle \mathbf {I} \Sigma _{1}} を含む半決定可能な理論(第二)に置き換えても証明することができる。
照井一成. “再帰的関数論(2005年度、慶應義塾大学文学部)” (PDF). 京都大学数理解析研究所. 2018年12月24日閲覧。
Gödel, Kurt (1986), Feferman, Solomon, ed., Kurt Gödel: Collected Works: Volume I: Publications 1929-1936, Oxford University Press, pp. 144-195, ISBN 978-0-19-503964-1, https://books.google.com/books?id=5ya4A0w62skC&pg=PA144
Gödel, Kurt Meltzer, B.訳 (1992), On Formally Undecidable Propositions of Principia Mathematica and Related Systems, Dover Books on Mathematics, Dover Publications, ISBN 978-0-486-66980-9, https://books.google.com/books?id=R7cHCYzIdWYC&pg=PA1
矛盾を「 ⊥ {\displaystyle \bot } 」で表し、「 ⊥ {\displaystyle \bot } 」のゲーデル数を b {\displaystyle b} とする。すると、「自然数論の体系内で自然数論の無矛盾性を証明できる」という言説を
自然数論の体系内で「 ¬ P r o v a b l e ( b ) {\displaystyle \lnot Provable(b)} 」を証明できる
の意味に解することができる。
まず
¬ P r o v a b l e ( b ) {\displaystyle \lnot Provable(b)}
が自然数論の体系内で証明可能であると仮定する。
第一不完全性定理のところで示したように、 ¬ P r o v a b l e A R G ( m , m ) {\displaystyle \lnot ProvableARG(m,m)} が証明できれば矛盾が証明できる。この議論を自然数論の体系内で行うことで、
P r o v a b l e ( n p m m ) ⇒ P r o v a b l e ( b ) {\displaystyle Provable(npmm)\Rightarrow Provable(b)}
が自然数論の体系内で証明可能なことがわかる。故に対偶を取ることで
第1不完全性定理はロビンソン算術を含んでいれば十分である。またω無矛盾性の仮定は単なる無矛盾性の仮定に弱められる(後述)。第2不完全性定理はロビンソン算術にΣ1論理式に対する数学的帰納法の公理図式を追加した体系( I Σ 1 {\displaystyle I\Sigma _{1}} )を含んでいれば十分である。ペアノ算術はこれを含むから、ペアノ算術を含む理論は第2不完全性定理の適用範囲である。
ゲーデルの定理は無矛盾な理論についてのみ適用できる。一階論理では、ex falso quodlibet (en) により、矛盾した理論 T {\displaystyle T} はその言語上の如何なる式であれ証明できてしまい、その中には「 T {\displaystyle T} は無矛盾である」と主張する式も含まれる。
ゲーデルの定理が成り立つのは、あくまで定理が必要としている仮定を満足するような形式的体系に限られる。全ての公理系がこれらの仮定を満たす訳ではなく、中には自然数論の標準モデルを部分構造として持つようなモデルを持っていてもなお仮定を満たさないような公理系もある。