無矛盾

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

定義

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

$T\vdash \phi$ かつ $T\vdash \lnot \phi$.

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

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

$T\nvdash \bot$.

または単純に Con(T) とも記される。

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

$T\vdash \bot$.

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

$\forall \phi \;T\vdash \phi$.

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

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

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

不完全性定理

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

$T\nvdash \operatorname {Con} (T)$

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

極大無矛盾

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

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

が成立するとき、T ⊆ U と記す。

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

$T\subseteq U$ かつ $T\neq U$

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

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

連座無矛盾性

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

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

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

参考文献

• 田中 一之 編『ゲーデルと20世紀の論理学 3 不完全性定理と算術の体系』東京大学出版会、2007年。ISBN 978-4130640978。 
• 田中 一之、角田 法也、鹿島 亮、菊池 誠『数学基礎論講義―不完全性定理とその発展』日本評論社、1997年。ISBN 978-4535782419。 
• 菊池 誠『不完全性定理』共立出版、2014年。ISBN 978-4320110960。 

関連項目

• ω無矛盾 - 無矛盾性より強い概念
• 健全性
• 不完全性定理