無矛盾

数学基礎論において、無矛盾性 (英: consistency) は公理系の最も重要な概念の一つである。

定義

ある理論 $T$ において、次のような論理式 $φ$ が存在するとき、理論 $T$ は矛盾する (inconsistent) といい、このような $φ$ が存在しないとき、 $T$ は無矛盾である (consistent) という:^[1]

T\vdash \phi

かつ

T\vdash \lnot \phi

.

ここでターンスタイル記号（ライトタック記号） ⊢ は左辺が右辺を証明できることを示す2項関係である。すなわちこの論理式 $φ \land \neg φ$ は、理論 $T$ の矛盾 (contradiction) を意味する。

この矛盾 (contradiction) はしばしばアップタック記号 ⊥ を用いて表され、理論 $T$ が無矛盾であることは次のように表される:

T\nvdash \bot

.

または単純に $Con(T)$ とも記される。^[2]

また理論 $T$ が矛盾することは次のように表される:

T\vdash \bot

.

矛盾する理論は任意の論理式を証明できるため、これは次と同値である:^[3]

\forall \phi \;T\vdash \phi

.

この性質に着目し、理論 $T$ の論理式で有りながら証明できないような論理式 $φ$ の存在を無矛盾の定義とすることがある。すなわち:

\operatorname {Con} (T):=\exists \phi \;T\nvdash \phi

.

この2つの無矛盾の定義は厳密には一致せず^{[注釈 1]}、区別するときには最初の方を単純無矛盾 (simply consistent)、新しい方を絶対無矛盾 (absolutely consistent) と呼ぶ。^[4]

ゲーデルの不完全性定理は、ロビンソン算術 $Q$ の再帰的拡大（またはRE拡大）である理論 $T$ がω無矛盾（または無矛盾）であるとき、

T\nvdash \operatorname {Con} (T)

である、すなわち理論自身では自身の無矛盾性を証明できないことを述べている。^[2]^[5]

理論 $T, U$ と $T$ の任意の論理式 $φ$ について

T\vdash \phi \rightarrow U\vdash \phi

が成立するとき、 $T \subseteq U$ と記す。^[6]

そして無矛盾な理論 $T$ について、

T\subseteq U

かつ

T\neq U

を満たす無矛盾な理論 $U$ が存在しないとき、 $T$ は極大無矛盾 (maximally consistent) であるという。^[7]

真の算術 $TA$ は、その定義から明らかに極大無矛盾である。^[8]

T をある理論、 A を「 T に追加しようとしているある公理」だとする。ここで T + A を「 T に Aを追加した理論」であるとすると、

\operatorname {Con} (T)\Rightarrow \operatorname {Con} (T+A)

という命題を予め証明することで、後々Tの無矛盾性から直ちにT + Aの無矛盾性が証明される。したがってこの命題をAのTに対する相対的無矛盾性 (英: relative consistency) と呼び、このとき「AはT に伴って無矛盾である」という。