無矛盾

数学基礎論において、無矛盾性 (テンプレート:Lang-en-short) は公理系の最も重要な概念の一つである。

定義

ある理論 テンプレート:Mvar において、次のような論理式 テンプレート:Mvar が存在するとき、理論 テンプレート:Mvar は矛盾する (テンプレート:En) といい、このような テンプレート:Mvar が存在しないとき、テンプレート:Mvar は無矛盾である (テンプレート:En) という:テンプレート:Sfn

$T⊢\varphi$ かつ $T⊢\mathrm{\neg }\varphi$.

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

この矛盾 (テンプレート:En) はしばしばアップタック記号 テンプレート:Mbot を用いて表され、理論 テンプレート:Mvar が無矛盾であることは次のように表される:

$T⊬\mathrm{\perp }$.

または単純に テンプレート:Math とも記される。テンプレート:Sfn

また理論 テンプレート:Mvar が矛盾することは次のように表される:

$T⊢\mathrm{\perp }$.

矛盾する理論は任意の論理式を証明できるため、これは次と同値である:テンプレート:Sfn

$\mathrm{\forall }\varphi T⊢\varphi$.

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

$\mathrm{Con}(T):=\mathrm{\exists }\varphi T⊬\varphi$.

この2つの無矛盾の定義は厳密には一致せずテンプレート:Efn、区別するときには最初の方を単純無矛盾 (テンプレート:En)、新しい方を絶対無矛盾 (テンプレート:En) と呼ぶ。

不完全性定理

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

$T⊬\mathrm{Con}(T)$

である、すなわち理論自身では自身の無矛盾性を証明できないことを述べている。テンプレート:Sfnテンプレート:Sfn

極大無矛盾

理論 テンプレート:Mvar と テンプレート:Mvar の任意の論理式 テンプレート:Mvar について

$T⊢\varphi \to U⊢\varphi$

が成立するとき、テンプレート:Math と記す。テンプレート:Sfn

そして無矛盾な理論 テンプレート:Mvar について、

$T\subseteq U$ かつ $T\ne U$

を満たす無矛盾な理論 テンプレート:Mvar が存在しないとき、テンプレート:Mvar は極大無矛盾 (テンプレート:En) であるという。テンプレート:Sfn

真の算術 テンプレート:Math は、その定義から明らかに極大無矛盾である。テンプレート:Sfn

相対的無矛盾性

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

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

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

参考文献

• テンプレート:Cite book
• テンプレート:Cite book
• テンプレート:Cite book

関連項目

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