ゲーデル以後の展開
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:04 UTC 版)
「ゲーデルの不完全性定理」の記事における「ゲーデル以後の展開」の解説
第一不完全性定理の拡張として、証明の定義に、命題の証明より小さな、否定命題の証明が存在しないという性質を追加した上で、前提のω無矛盾性を無矛盾性に弱めた定理がジョン・バークリー・ロッサー (1936年) によって示された。この事実はω矛盾した算術理論を考える場合などにおいて重要となる。なお算術を内包する真である体系（自然数の標準モデルで真である公理に基づく体系）はω無矛盾なので、第1不完全性定理は原型のままでも適用できる。今日ではこちらの無矛盾性のみを仮定する強い定理もゲーデルの不完全性定理と呼ばれるが、単にロッサーの定理、ゲーデル・ロッサーの定理などと呼ばれることもある。 第二不完全性定理に関しては、ゲーデルによる証明の定義に代えて、ロッサーによる上記の証明の定義を用いれば、体系自身の無矛盾性が証明できることが、クライゼル (1960) によって指摘されている。2つの証明の定義の同値性は体系内では証明できないため、第2不完全性定理とは矛盾しない。 レオン・ヘンキンは、対角化により「Hは証明できる」と同値となる命題H（ヘンキン文）を構成し、その証明可能性に関する問題を1952年に提起した。この問題は3年後の1955年に、マーティン・レープによって解かれた。彼は、「Hの証明が存在すればHである」が証明可能であれば、Hもまた証明可能であることを示した（レープの定理）。Hに矛盾を代入すれば、レープの定理から第二不完全性定理が示せる。
※この「ゲーデル以後の展開」の解説は、「ゲーデルの不完全性定理」の解説の一部です。
「ゲーデル以後の展開」を含む「ゲーデルの不完全性定理」の記事については、「ゲーデルの不完全性定理」の概要を参照ください。
- ゲーデル以後の展開のページへのリンク
