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