ω無矛盾

数学基礎論においてω無矛盾（オメガむむじゅん、英: ω-consistent）とは、公理系の性質を表す概念のひとつである。不完全性定理を示すためにクルト・ゲーデルによって導入された。ω無矛盾性は、通常の無矛盾性よりも強い性質である。

ヒルベルト・プログラムの下、数学の完全性と無矛盾性を示そうとする試みがなされていたが、1931年にゲーデルの発表した不完全性定理は、ある意味でそのふたつが両立することは不可能であるというものであった。ゲーデルは「公理系が無矛盾ならば不完全」であることを示そうとしたが果たせず、それよりも少し弱い「ω無矛盾ならば不完全」であることを示した。しかし1936年アメリカの論理学者ジョン・バークリー・ロッサーによって、ゲーデルの当初の目的である「無矛盾ならば不完全」が示された。今日では、ゲーデルによるω無矛盾性を用いた前者の定理を「第1不完全性定理」と呼ぶ。

定義

ある公理系が通常の意味で矛盾 (inconsistent) しているとは、ある論理式 P が存在して、P と ¬P とがともに証明可能であることを意味する。これに対し、公理系がω矛盾 (ω-inconsistent) するとは、自然数 n によって定まる論理式 Q(n) が存在して、次を満たすことをいう:

Q(0), Q(1), Q(2), … が全て証明可能であるが、「∃n : ¬Q(n)」も証明可能である。

そして、矛盾していない公理系を無矛盾 (consistent)) であるといい、ω矛盾していない公理系をω無矛盾 (ω-consistent) であるという。

通常の感覚では、Q(0), Q(1), Q(2), … が全て証明可能であれば、「∀n : Q(n)」も証明可能であるように思え、 したがってもし公理系が無矛盾なら「∃n : ¬Q(n)」は証明不能であるように思える。 しかし n の取り得る範囲が無限に多いときは上の直観は一般には正しくない。 実際 Q(0) の証明、Q(1) の証明、Q(2) の証明、… を並べただけでは、無限に長いものになってしまうため、それは妥当な証明とはみなされない。 したがって、Q(0), Q(1), Q(2), … の各々が全て証明可能であっても「∀n : Q(n)」が証明可能であるとは限らないのである。 よって公理系が通常の意味で矛盾していなくともω矛盾している、という状況が起こり得る。

ω無矛盾性は無矛盾性よりも強い(弱くない)概念である。 実際、ある公理系が矛盾している場合、P と ¬P がともに証明可能であるような P が存在し、したがって前述の Q(n) として P をとれば、その公理系がω矛盾している事が分かる。 したがって対偶をとる事で、ω無矛盾性が無矛盾性を含意する事が分かる。 よって特に、ロッサーの結果はゲーデルの結果の拡張とみなされる。

無矛盾だがω矛盾した理論の例

ペアノ算術 PA はω無矛盾であるからΣ₁健全性により PA から ¬Con(PA) は証明不能である。そこで PA に ¬Con(PA) を付け加えた理論 T を考える。不完全性定理により PA は Con(PA) を証明できないから T は無矛盾である。T では、PA の標準モデルにおいて偽であるΣ₁論理式 ¬Con(PA) を証明できる。すなわち T はΣ₁健全でない。ω無矛盾性はΣ₁健全性を含意するので、したがって T はω矛盾している。

上述の理論 T のモデルは矛盾に至る PA の証明図のゲーデル数を持つ。これは標準的自然数ではありえないので超準的自然数である。すなわち T のモデルはペアノ算術の超準モデルになっている。

参考文献

• Gödel, K. (1931). “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”. Monatshefte für Mathematik und Physik 38: 173–198. doi:10.1007/BF01700692.  - ゲーデルの原論文
• 田中 一之、角田 法也、鹿島 亮、菊池 誠『数学基礎論講義―不完全性定理とその発展』日本評論社、1997年。ISBN 978-4535782419。 
• 菊池 誠『不完全性定理』共立出版、2014年。ISBN 978-4320110960。 

関連項目

• 無矛盾
• 不完全性定理
• 超準モデル