無矛盾のソースを表示

[[数学基礎論]]において、'''無矛盾性''' ({{lang-en-short|consistency}}) は[[公理系]]の最も重要な概念の一つである。

==定義==
ある理論 {{mvar|T}} において、次のような論理式 {{mvar|&phi;}} が存在するとき、理論 {{mvar|T}} は'''矛盾する''' ({{En|inconsistent}}) といい、このような {{mvar|&phi;}} が存在しないとき、{{mvar|T}} は'''無矛盾である''' ({{En|consistent}}) という:{{Sfn|田中|2007|pages=90-91}}
: <math>T \vdash \phi</math> かつ <math>T \vdash \lnot \phi</math>.
ここで[[:en:Turnstile (symbol)|ターンスタイル記号（ライトタック記号）]] &#x22A2; は左辺が右辺を証明できることを示す2項関係である。すなわちこの論理式 {{math|''&phi;'' &and; &not;''&phi;''}} は、理論 {{mvar|T}} の'''[[矛盾]]''' ({{En|contradiction}}) を意味する。

この矛盾 ({{En|contradiction}}) はしばしば[[垂直記号|アップタック記号]] {{mbot}} を用いて表され、理論 {{mvar|T}} が無矛盾であることは次のように表される:
: <math>T \nvdash \bot</math>.
または単純に {{math|Con(''T'')}} とも記される。{{Sfn|田中|2007|pages=93}}

また理論 {{mvar|T}} が矛盾することは次のように表される:
: <math>T \vdash \bot</math>.
矛盾する理論は任意の論理式を証明できるため、これは次と同値である:{{Sfn|田中|2007|pages=81}}
: <math>\forall \phi \; T \vdash \phi</math>.
この性質に着目し、理論 {{mvar|T}} の論理式で有りながら証明できないような論理式 {{mvar|&phi;}} の存在を無矛盾の定義とすることがある。すなわち:
: <math>\operatorname{Con}(T) := \exist \phi \; T \nvdash \phi</math>.
この2つの無矛盾の定義は厳密には一致せず{{Efn|
{{mvar|A}} かつ {{mvar|&not;A}} から任意の論理式を導けるような {{mvar|T}} の論理式 {{mvar|A}},{{mvar|&not;A}} が存在するとき、両者は一致する。<ref name="清水1984" /><!-- この「{{mvar|A}} かつ {{mvar|&not;A}} から任意の論理式を導けるような」の部分必要か？ -->
}}、区別するときには最初の方を'''単純無矛盾''' ({{En|simply consistent}})、新しい方を'''絶対無矛盾''' ({{En|absolutely consistent}}) と呼ぶ。<ref name="清水1984" />

==不完全性定理==
[[ゲーデルの不完全性定理]]は、[[ロビンソン算術]] {{math|Q}} の再帰的拡大（またはRE拡大）である理論 {{mvar|T}} が[[ω無矛盾]]（または無矛盾）であるとき、
: <math>T \nvdash \operatorname{Con}(T)</math>
である、すなわち理論自身では自身の無矛盾性を証明できないことを述べている。{{Sfn|田中|2007|pages=93}}{{Sfn|田中|角田|鹿島|菊池|1997|page=86}}

==極大無矛盾==
理論 {{mvar|T, U}} と {{mvar|T}} の任意の論理式 {{mvar|&phi;}} について
: <math>T \vdash \phi \rightarrow U \vdash \phi</math>
が成立するとき、{{math|''T'' &#x2286; ''U''}} と記す。{{Sfn|菊池|2014|pages=32-33}}

そして無矛盾な理論 {{mvar|T}} について、
: <math>T \subseteq U</math> かつ <math>T \ne U</math>
を満たす無矛盾な理論 {{mvar|U}} が存在しないとき、{{mvar|T}} は'''極大無矛盾''' ({{En|maximally consistent}}) であるという。{{Sfn|菊池|2014|page=47}}

[[真の算術]] {{math|TA}} は、その定義から明らかに極大無矛盾である。{{Sfn|菊池|2014|page=109}}

==相対的無矛盾性==
''T'' をある理論、 ''A'' を「 ''T'' に追加しようとしているある公理」だとする。ここで ''T'' + ''A'' を「 ''T'' に ''A''を追加した理論」であるとすると、
: <math>\operatorname{Con}(T) \Rightarrow \operatorname{Con}(T + A)</math>
という命題を予め証明することで、後々''T''の無矛盾性から直ちに''T'' + ''A''の無矛盾性が証明される。したがってこの命題を''A''の''T''に対する相対的無矛盾性 ({{lang-en-short|relative consistency}}) と呼び、このとき「''A''は''T''
に伴って無矛盾である」という。

==注釈==
<references group="注釈"/>

==脚注==
<references>
<ref name="清水1984">{{Cite book
| author    = 清水 義夫
| title     = 記号論理学
| year      = 1984
| publisher = 東京大学出版会
| isbn      = 978-4130120180
| page      = 100
| ref       = 
}}</ref>
</references>

==参考文献==
* {{Cite book|和書
| editor    = 田中 一之
| title     = ゲーデルと20世紀の論理学 3 不完全性定理と算術の体系
| year      = 2007
| publisher = 東京大学出版会
| isbn      = 978-4130640978
| ref       = {{SfnRef|田中|2007}}
}}
* {{Cite book|和書
| author1   = 田中 一之
| authorlink1= 田中一之
| author2   = 角田 法也
| authorlink2= 角田法也
| author3   = 鹿島 亮
| authorlink3= 鹿島亮
| author4   = 菊池 誠
| authorlink4= 菊池誠 (神戸大学)
| title     = 数学基礎論講義―不完全性定理とその発展
| year      = 1997
| publisher = 日本評論社
| isbn      = 978-4535782419
| ref       = {{SfnRef|田中|角田|鹿島|菊池|1997}}
}}
* {{Cite book|和書
| author    = 菊池 誠
| authorlink= 菊池誠 (神戸大学)
| title     = 不完全性定理
| year      = 2014
| publisher = 共立出版
| isbn      = 978-4320110960
| ref       = {{SfnRef|菊池|2014}}
}}

==関連項目==
* [[ω無矛盾]] - 無矛盾性より強い概念
* [[無矛盾律]]
* [[健全性]]
* [[不完全性定理]]

{{Mathlogic-stub}}
{{Normdaten}}
{{デフォルトソート:むむしゆん}}
[[Category:論理記号]]
[[Category:数学基礎論]]
[[Category:数学に関する記事]]