Editing Contradiction (section)

===Proof by contradiction===
{{main|Proof by contradiction}}
For a set of consistent premises <math>\Sigma</math> and a proposition <math>\varphi</math>, it is true in [[classical logic]] that <math>\Sigma \vdash\varphi</math> (i.e., <math>\Sigma</math> proves <math>\varphi</math>) if and only if <math>\Sigma \cup \{\neg\varphi\} \vdash \bot</math> (i.e., <math>\Sigma</math> and <math>\neg\varphi</math> leads to a contradiction). Therefore, a [[proof (logic)|proof]] that <math>\Sigma \cup \{\neg\varphi\} \vdash \bot</math> also proves that <math>\varphi</math> is true under the premises <math>\Sigma</math>. The use of this fact forms the basis of a [[Proof techniques|proof technique]] called [[proof by contradiction]], which mathematicians use extensively to establish the validity of a wide range of theorems. This applies only in a logic where the [[law of excluded middle]] <math>A\vee\neg A</math> is accepted as an axiom.

Using [[minimal logic]], a logic with similar axioms to classical logic but without ''ex falso quodlibet'' and proof by contradiction, we can investigate the axiomatic strength and properties of various rules that treat contradiction by considering theorems of classical logic that are not theorems of minimal logic.<ref>Diener and Maarten McKubre-Jordens, 2020. [https://arxiv.org/abs/1606.08092 Classifying Material Implications over Minimal Logic]. [[Archive for Mathematical Logic]] 59 (7-8):905-924.</ref> Each of these extensions leads to an [[intermediate logic]]:
# Double-negation elimination (DNE) is the strongest principle, axiomatized <math>\neg\neg A \implies A</math>, and when it is added to minimal logic yields classical logic.
# Ex falso quodlibet (EFQ), axiomatized <math>\bot \implies A</math>, licenses many consequences of negations, but typically does not help to infer propositions that do not involve absurdity from consistent propositions that do. When added to minimal logic, EFQ yields [[intuitionistic logic]]. EFQ is equivalent to ''ex contradiction quodlibet'', axiomatized <math>A \land \neg A \implies B</math>, over minimal logic.
# [[Peirce's law|Peirce's rule]] (PR) is an axiom <math>((A \implies B) \implies A) \implies A</math> that captures proof by contradiction without explicitly referring to absurdity. Minimal logic + PR + EFQ yields classical logic. 
# The Gödel-Dummett (GD) axiom <math>A \implies B \vee B \implies A</math>, whose most simple reading is that there is a linear order on truth values.  Minimal logic + GD yields [[Gödel-Dummett logic]]. Peirce's rule entails but is not entailed by GD over minimal logic.
# Law of the excluded middle (LEM), axiomatised <math>A \vee \neg A</math>, is the most often cited formulation of the [[principle of bivalence]], but in the absence of EFQ it does not yield full classical logic. Minimal logic + LEM + EFQ yields classical logic. PR entails but is not entailed by LEM in minimal logic. If the formula B in Peirce's rule is restricted to absurdity, giving the axiom schema <math>(\neg A \implies A) \implies A</math>, the scheme is equivalent to LEM over minimal logic.
# Weak law of the excluded middle (WLEM) is axiomatised <math>\neg A \vee \neg\neg A</math> and yields a system where disjunction behaves more like in classical logic than intuitionistic logic, i.e. the [[disjunction and existence properties]] don't hold, but where use of non-intuitionistic reasoning is marked by occurrences of double-negation in the conclusion. LEM entails but is not entailed by WLEM in minimal logic. WLEM is equivalent to the instance of [[De Morgan's law]] that distributes negation over conjunction: <math>\neg(A \land B) \iff (\neg A) \vee (\neg B)</math>.