「ゲーデルの不完全性定理」の版間の差分

2016年9月20日 (火) 19:24時点における版

2016年9月20日 (火) 19:29時点における版

126行目:

ゲーデルの定理は無矛盾な理論についてのみ適用できる。一階論理では、''ex falso quodlibet'' ([[:en:Principle of explosion|en]]) により、矛盾した理論 ''T'' はその言語上の如何なる式であれ証明できてしまい、その中には「''T'' は無矛盾である」と主張する式も含まれる。

ゲーデルの定理が成り立つのは、飽くまで定理が必要としている仮定を満足するような形式的体系に限られる。全ての公理系がこれらの仮定を満たす訳ではなく、中には自然数論の標準モデルを部分構造として持つようなモデルを持っていてもなお仮定を満たさないような公理系もある。例えば、[[ユークリッド幾何学]]の一階公理化理論、実閉体の理論、乗算が全域で可能なことを証明できないような算術理論、これらは何れもゲーデルの定理に必要な仮定を満たさない。要点は、これらの公理系では自然数の集合を定義することや自然数の基本的な性質を十分展開証明することができないことにある。三つ目の例に関して言えば、 Dan E. Willard は第二不完全性定理に必要な仮定を満たさないような様々な弱い算術理論を調べた（例えば Willard 2001）。

ゲーデルの定理は実効的に生成された（即ち、[[帰納的可算集合|帰納的可算]]な）理論についてのみ適用できる。もし自然数に関する真である文を全て公理とするような理論があるとするとを考えれば、この理論は無矛盾かつ完全であり、かつペアノ算術を含みつつゲーデルの定理は全く成立しなくなんでいる。何故ならこの理論は帰納的可算ではないからである<ref>訳注：この場合の「帰納的可算」とは、すべての定理のゲーデル数を枚挙する計算可能関数が存在する（実効的に枚挙可能）ことを意味する。[[クレイグのトリック]]によれば、このことは定理集合が帰納的な公理系から生成される（演繹閉包である）ことと同値である。</ref>。

第二不完全性定理が示すのは、ある公理系の無矛盾性はその公理系自身では証明できないということであって、他の無矛盾な公理系からも証明できないとは言っていない。例えば、[[ペアノ算術]]の無矛盾性は[[公理的集合論#ZFC|ZFC]]から証明できるし、算術の理論に[[エプシロン・ノート|&epsilon;₀]]までの[[数学的帰納法#超限帰納法|超限帰納法]]を加えて得られた{{仮リンク|ゲンツェンによる無矛盾性の証明|en|Gentzen's consistency proof}}もある。