数学基礎論においてω無矛盾（オメガむむじゅん、）とは、公理系の性質を表す概念のひとつである。不完全性定理を示すためにクルト・ゲーデルによって導入された。ω無矛盾性は、通常の無矛盾性よりも強い性質である。
20世紀初頭にはヒルベルト・プログラムの下、数学の完全性と無矛盾性を示そうとする試みがなされていたが、1931年にゲーデルの発表した不完全性定理は、ある意味でそのふたつが両立することは不可能であるというものであった。ゲーデルは1931年の時点では「公理系が無矛盾ならば不完全であること」を示そうとしたが果たせず、それよりも弱い主張である「公理系がω無矛盾ならば不完全であること」を示した。さらに1936年アメリカの論理学者ジョン・バークリー・ロッサーによって、ゲーデルの当初の目的である「無矛盾ならば不完全」が示された。今日では、ゲーデルによるω無矛盾性を用いた前者の定理を「第1不完全性定理」と呼ぶ。
定義 ある公理系が通常の意味で矛盾 () しているとは、ある論理式 が存在して、 と とがともに証明可能であることを意味する。これに対し、公理系がω矛盾 () するとは、自然数 によって定まる論理式 が存在して、次を満たすことをいう: が全て証明可能であるが、「」も証明可能である。 そして、矛盾していない公理系を無矛盾 () であるといい、ω矛盾していない公理系をω無矛盾 () であるという。
無矛盾性とω無矛盾性の関係 ω無矛盾性は無矛盾性よりも強い概念である。
ある公理系が矛盾している場合、 と がともに証明可能であるような が存在し、したがって前述の として をとれば、その公理系がω矛盾している事が分かる。その対偶を取れば、公理系がω無矛盾ならば無矛盾である。よって特に、ロッサーの結果はゲーデルの結果の拡張とみなされる。
一方で、無矛盾だがω矛盾した理論の例がある。すなわち、 と「」が全て証明可能であり、しかも無矛盾な公理系が存在する。
通常の感覚では が全て証明可能であれば当然「」も証明可能であり、矛盾が生じざるを得ないように思える。しかし、公理系においてある命題が証明可能であるとは、その公理系における（有限長の）証明が存在するということであり、 の（無限個の）証明があるという事実から、「」の証明が存在することを導くことは一般にはできない。
無矛盾だがω矛盾した理論の例 ペアノ算術 はω無矛盾であるからΣ1健全性により から は証明不能である。そこで に を付け加えた理論 を考える。不完全性定理により は を証明できないから は無矛盾である。 では、 の標準モデルにおいて偽であるΣ1論理式 を証明できる。すなわち はΣ1健全でない。ω無矛盾性はΣ1健全性を含意するので、したがって はω矛盾している。
上述の理論 のモデルは矛盾に至る の証明図のゲーデル数を持つ。これは標準的自然数ではありえないので超準的自然数である。すなわち のモデルはペアノ算術の超準モデルになっている。
脚注
参考文献 - ゲーデルの原論文
関連項目 無矛盾 不完全性定理 超準モデル