数学基礎論において、ω無矛盾（オメガむむじゅん、omega-consistency）とは、公理系の性質を表す概念のひとつである。不完全性定理を示すためにクルト・ゲーデルによって導入された。ω無矛盾性は、通常の無矛盾性よりも強い性質である。ヒルベルト・プログラムの下、数学の完全性と無矛盾性を示そうとする試みがなされていたが、1931年にゲーデルの発表した不完全性定理は、ある意味でそのふたつが両立することは不可能であるというものであった。ゲーデルは「公理系が無矛盾ならば不完全」であることを示そうとしたが果たせず、それよりも少し弱い「ω無矛盾ならば不完全」であることを示した。1936年に、ジョン・バークリー・ロッサーは、ゲーデルの当初の目的である「無矛盾ならば不完全」であることを示した。今日では、通常これを第1不完全性定理と呼ぶ。ある公理系が通常の意味で矛盾しているとは、ある論理式 P が存在して、P と ￢P とがともに証明可能であることを意味する。これに対し、ω矛盾とは、自然数 "n" によって定まる論理式 Q("n") が存在して、次を満たすことをいう。矛盾していない公理系を無矛盾であるといい、ω矛盾していない公理系をω無矛盾であるという。通常の感覚では、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のモデルはペアノ算術の超準モデルになっている。

出典:wikipedia