矛盾

一貫性のある前提のセット${\displaystyle \Sigma }$そして提案${\displaystyle \varphi }$古典論理では、${\displaystyle \Sigma \vdash \varphi }$（つまり、${\displaystyle \Sigma }$証明する${\displaystyle \varphi }$) の場合に限り${\displaystyle \Sigma \cup \{\neg \varphi \}\vdash \bot }$（つまり、${\displaystyle \Sigma }$そして${\displaystyle \neg \varphi }$（矛盾につながる）したがって、${\displaystyle \Sigma \cup \{\neg \varphi \}\vdash \bot }$また、${\displaystyle \varphi }$前提条件の下では真である${\displaystyle \Sigma }$この事実の利用は、数学者が幅広い定理の妥当性を確立するために広く用いる、背理法と呼​​ばれる証明技法の基礎を形成している。これは排中律が成り立つ論理体系においてのみ適用される。${\displaystyle A\vee \neg A}$公理として受け入れられている。

矛盾証明は、一連の矛盾のない前提Σの下で命題φを証明することが不可能であるか、あるいは矛盾を証明する方が容易である場合に最も効果的に実行できます。よくある例として、√2が無理数であることの証明が挙げられます。これを直接証明しようとすると非常に困難ですが、√2が有理数であると仮定すると、証明しやすい矛盾が生じます（√2の項の「逆数を用いた証明」を参照）。その他の状況で矛盾証明を用いると、非効率的であったり、そもそも不可能であったりする場合があります。

古典論理と同様の公理を持つが、ex falso quodlibetや背理法を用いない最小論理を用いることで、最小論理の定理ではない古典論理の定理を考察することにより、矛盾を扱う様々な規則の公理的強度と性質を調べることができる。 ^{[ 6 ]}これらの拡張はそれぞれ中間論理につながる。

1. 二重否定除去（DNE）は最も強力な原理であり、公理化されている。${\displaystyle \neg \neg A\implies A}$そして、それを最小論理に加えると古典論理が得られる。
2. Ex false quodlibet (EFQ)、公理化${\displaystyle \bot \implies A}$EFQは否定の多くの帰結を許容するが、通常、矛盾のない命題から矛盾のない命題を推論するのには役立たない。EFQを最小論理に加えると、直観主義論理が得られる。EFQは、公理化されたex contradiction quodlibetと同等である。${\displaystyle A\land \neg A\implies B}$最小限の論理に基づいて。
3. パースの法則（PR）は公理である${\displaystyle ((A\implies B)\implies A)\implies A}$これは、不条理を明示的に言及することなく、背理法による証明を捉えるものである。最小論理＋PR＋EFQは古典論理をもたらす。
4. ゲーデル＝ダメット（GD）公理${\displaystyle A\implies B\vee B\implies A}$最も単純な解釈では、真理値には線形順序が存在すると解釈される。最小論理＋ゲーデル＝ダメット論理はゲーデル＝ダメット論理となる。パースの規則は最小論理上のゲーデル＝ダメット論理によって導かれるが、ゲーデル＝ダメット論理からは導かれない。
5. 排中律（LEM）を公理化する${\displaystyle A\vee \neg A}$は二値原理の最もよく引用される定式化ですが、EFQがない場合、完全な古典論理は得られません。最小論理 + LEM + EFQ は古典論理を生成します。PR は、最小論理では LEM によって含意されますが、含意されません。パースの規則の式 B が不条理に限定されている場合、公理図式が得られます。${\displaystyle (\neg A\implies A)\implies A}$この方式は、最小論理に基づくLEMと同等である。
6. 排中律の弱法則（WLEM）は公理化される${\displaystyle \neg A\vee \neg \neg A}$そして、選言が直観主義論理よりも古典論理に近い振る舞いをするシステム、すなわち選言と存在の性質が成り立たないシステムを生み出すが、非直観主義的推論の使用は結論における二重否定の出現によって特徴づけられる。最小論理では、LEMはWLEMを含意するが、WLEMは含意しない。WLEMは、否定を連言に分配するド・モルガンの法則のインスタンスと同等である。${\displaystyle \neg (A\land B)\iff (\neg A)\vee (\neg B)}$。

数学では、証明の中で矛盾を表すために使用される記号は様々です。^{[ 7 ]}矛盾を表すために使用される可能性のある記号には、↯、Opq、${\displaystyle \Rightarrow \Leftarrow }$、⊥、${\displaystyle \leftrightarrow \ \!\!\!\!\!\!\!}$/ および ※。どの記号体系においても、矛盾は真偽値「偽」の代わりに用いられ、例えば「0」で表される（ブール代数ではよく用いられる）。矛盾記号の直後にQEDやその変形が現れることも珍しくない。実際、これは背理法による証明において、元の仮定が偽であることが証明されたこと、したがってその否定が真であることを示すためにしばしば用いられる。

一般的に、一貫性証明には次の2つの要素が必要です。

1. 公理系​
2. 式pとその否定~pの両方がこのシステム内で導出できるわけではないことを示す。

しかし、どのような方法を用いようとも、すべての無矛盾性証明は、矛盾という原始的な概念を必要とするように思われる。さらに、この概念は、トートロジーの定義において、形式体系の「外側」に存在しなければならないように思われる。

エミール・ポストは、1921年の著書『初等命題の一般理論入門』の中で、命題計算（すなわち論理）の無矛盾性の証明を『プリンキピア・マテマティカ』 （PM）の範囲を超えて拡張した際、一般化された公理（すなわち公理）の集合に関して、「矛盾」という概念を自動的に持ち出すことはもはやできないと指摘した。なぜなら、そのような概念は公理の中に含まれていない可能性があるからである。

公理の集合の第一の要件は、それが無矛盾であることです。無矛盾の通常の概念は矛盾の概念を含み、それはまた否定を含むため、そしてこの関数は一般に[一般化された公理の集合]の原始関数として現れないため、新しい定義を与える必要があります。^{[ 8 ]}

ポストによるこの問題の解決策は、アーネスト・ネーゲルとジェームズ・R・ニューマンが1958年の著書『ゲーデルの証明』の中で提示した「矛盾の絶対的証明の成功例」というデモンストレーションで説明されている。彼らもまた、「矛盾」という概念と、その通常の「真理値」である「真」と「偽」に関して問題があることに気づいていた。彼らは次のように指摘した。

トートロジーであるという性質は、真偽の概念で定義されてきた。しかし、これらの概念は明らかに数式計算の外部にある何かを参照している。したがって、本文で述べた手順は、システムのモデルを提供することによって、計算の解釈を実際に提供していることになる。そうであるならば、著者らは約束したこと、すなわち「数式自体の純粋に構造的な特徴によって数式の性質を定義する」ことをしていないことになる。[実際]...モデルに基づいており、公理の真偽からその無矛盾性を論証する無矛盾性の証明は、単に問題をずらしているにすぎない。^{[ 9 ]}

_{PMの原始論理式S 1} VS ₂ [包括的OR]や~S（否定）のような「原始論理式」が与えられた場合、これらの原始概念を用いて公理を定義せざるを得ない。ポストはPMにおいて徹底的に実証し、まだ定義されていないトートロジーの性質は「継承される」と定義している（ネーゲルとニューマンも同様に定義している。後述）。トートロジーの公理（公準）の集合と、置換とモーダス・ポネンスを含む演繹システムから始めれば、一貫性のあるシステムはトートロジーの論理式のみを生み出すことになる。

トートログの定義に関して、NagelとNewmanは、互いに排他的で網羅的な2つのクラスK ₁とK _{2を作成し、変数（例えばS 1}とS ₂ ）がこれらのクラスから割り当てられたときに、公理（の結果）がこれらのクラスに分類されます。これは原始式にも適用されます。例えば、「S ₁ VS _{2の形式の式は、S 1}とS ₂の両方がK 2に含まれる場合、_クラスK 2に配置されます_{。そうでない場合は、K 1}に配置されます」、また「~Sの形式の式は、 SがK ₁に含まれる場合、 K _{2に配置されます。そうでない場合は、K 1}に配置されます」。^{[ 10 ]}

したがって、ネーゲルとニューマンは、同義反復の概念を次のように定義することができる。「式が同義反復であるのは、その要素がどちらのクラスに属するかに関わらず、クラス K _{1に属する場合に限る」。} ^{[ 11 ]}このように、「同義反復である」という性質は、モデルや解釈を参照することなく記述される。

例えば、~S ₁ VS ₂のような式と、 S 1 にK ₁、 S ₂にK ₂を割り当てると、その式を評価して、結果をいずれかのクラスに分類することができます。S 1 に K 1 を割り当てると、_~ S ₁は K 2 に分類され_、この_{割り当てによって式がクラス K 2}に収まることがわかります。したがって、定義により_、この式はトートロジーではありません。

ポストは、システムが矛盾している場合、そのシステムにおける演繹（つまり、トートロジーから導出された一連の式の最後の式）が最終的にS自身を導き出す可能性があることに気づいた。変数Sへの代入はクラスK1またはK2のいずれかから得られるため_、この_{演繹はトートロジーの継承特性に違反する（つまり、導出はクラスK1}に属する式の評価を導き出さなければならない）。このことから、ポストは矛盾の概念を用いずに、矛盾の以下の定義を導き出すことができた。

定義。システムが、修正されていない変数 p の主張（ニューマンとネイゲルの例では S ）を生み出す場合、そのシステムは矛盾していると言われる。

言い換えれば、無矛盾性の証明を構築する際には「矛盾」の概念は不要であり、それに代わるのは「相互排他的かつ網羅的な」クラスの概念である。公理系は「矛盾」の概念を含む必要はない。^{[ 12 ]： 177}

実用的矛盾とは、議論の主張そのものが、その主張する内容と矛盾する場合に生じる。この場合、矛盾が生じるのは、発言内容ではなく、発言行為そのものが結論を損なうからである。^{[ 14 ]}

弁証法的唯物論において、ヘーゲル哲学に由来する矛盾とは、通常、一つの領域、一つの統一された力または対象の中に内在する対立を指す。形而上学的思考とは異なり、この矛盾は客観的に不可能なものではない。なぜなら、これらの矛盾する力は客観的現実の中に存在し、互いに打ち消し合うのではなく、むしろ互いの存在を規定しているからである。マルクス主義理論によれば、このような矛盾は、例えば次のような事実に見出すことができる。

ヘーゲル主義とマルクス主義の理論は、歴史の弁証法的な性質が、その矛盾の止揚、すなわち総合をもたらすと規定している。したがってマルクスは、歴史は論理的に資本主義を社会主義社会へと進化させ、そこでは生産手段が社会の労働者階級と生産階級に等しく奉仕し、それによって（a）と（b）の間の以前の矛盾が解決されると仮定した。^{[ 15 ]}