無矛盾
ある理論 T において、次のような論理式 φ が存在するとき、理論 T は矛盾する (inconsistent) といい、このような φ が存在しないとき、T は無矛盾である (consistent) という:
T ⊢ φ {\displaystyle T\vdash \phi } かつ T ⊢ ¬ φ {\displaystyle T\vdash \lnot \phi } .
ここでターンスタイル記号(ライトタック記号) ⊢ は左辺が右辺を証明できることを示す2項関係である。すなわちこの論理式 φ ∧ ¬φ は、理論 T の矛盾 (contradiction) を意味する。
この矛盾 (contradiction) はしばしばアップタック記号 ⊥ を用いて表され、理論 T が無矛盾であることは次のように表される:
T ⊬ ⊥ {\displaystyle T\nvdash \bot } .
または単純に Con(T) とも記される。