ω無矛盾

ω無矛盾（おめがむむじゅん）とは、ある性質を持った形式的体系を指す数理論理学の用語である。第一不完全性定理が成り立つ条件を記述するために、ゲーデルが導入した。

定義

定義には同値なものがいくつかあるが、ここではその1つを示す。ある形式的体系$T$に1変数論理式$P$が存在し、文$\exists xP(x)$を形式的に証明可能であり、かつ任意の自然数$n$について$T$が文$\not P({\overline {n}})$(${\overline {n}}$は$n$の数項)を形式的に証明可能であるとき、$T$はω矛盾しているという。ω矛盾でない形式的体系をω無矛盾であるという。

無矛盾性との関係

矛盾した形式的体系は任意の文を形式的に証明可能だから、矛盾した形式的体系はω矛盾であるが、逆は必ずしも成り立たない。対偶を取れば、ω無矛盾な形式的体系は無矛盾だが、逆は必ずしも成り立たないので、ω無矛盾は無矛盾よりも強い概念である。

たとえば、ペアノの公理系に定数記号$c$と$0<c,1<c,...$の形の可算個の公理を追加した理論は(ペアノの公理系が無矛盾ならば)無矛盾だがω矛盾である($c\leq x$が$P(x)$となる)。