In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition by showing that assuming the proposition to be false leads to a contradiction.
[3] A mathematical proof employing proof by contradiction usually proceeds as follows: An important special case is the existence proof by contradiction: in order to demonstrate that an object with a given property exists, we derive a contradiction from the assumption that all objects satisfy the negation of the property.
The principle may be formally expressed as the propositional formula ¬¬P ⇒ P, equivalently (¬P ⇒ ⊥) ⇒ P, which reads: "If assuming P to be false implies falsehood, then P is true."
In natural deduction the principle takes the form of the rule of inference which reads: "If
In classical logic the principle may be justified by the examination of the truth table of the proposition ¬¬P ⇒ P, which demonstrates it to be a tautology: Another way to justify the principle is to derive it from the law of the excluded middle, as follows.
We assume ¬¬P and seek to prove P. By the law of excluded middle P either holds or it does not: In either case, we established P. It turns out that, conversely, proof by contradiction can be used to derive the law of excluded middle.
Thus in mathematical practice, both principles are referred to as "proof by contradiction".
Proof by contradiction is equivalent to the law of the excluded middle, first formulated by Aristotle, which states that either an assertion or its negation is true, P ∨ ¬P.
The law of noncontradiction was first stated as a metaphysical principle by Aristotle.
Formally the law of non-contradiction is written as ¬(P ∧ ¬P) and read as "it is not the case that a proposition is both true and false".
The law of non-contradiction neither follows nor is implied by the principle of Proof by contradiction.
In intuitionistic logic proof by contradiction is not generally valid, although some particular instances can be derived.
In contrast, proof of negation and principle of noncontradiction are both intuitionistically valid.
Brouwer–Heyting–Kolmogorov interpretation of proof by contradiction gives the following intuitionistic validity condition: if there is no method for establishing that a proposition is false, then there is a method for establishing that the proposition is true.
[clarify] If we take "method" to mean algorithm, then the condition is not acceptable, as it would allow us to solve the Halting problem.
If proof by contradiction were intuitionistically valid, we would obtain an algorithm for deciding whether an arbitrary Turing machine M halts, thereby violating the (intuitionistically valid) proof of non-solvability of the Halting problem.
Thus in intuitionistic logic proof by contradiction is not universally valid, but can only be applied to the ¬¬-stable propositions.
A typical example of a decidable proposition is a statement that can be checked by direct computation, such as "
An early occurrence of proof by contradiction can be found in Euclid's Elements, Book 1, Proposition 6:[7] The proof proceeds by assuming that the opposite sides are not equal, and derives a contradiction.
His Nullstellensatz states: Hilbert proved the statement by assuming that there are no such polynomials
In Euclid's Elements the theorem is stated in Book IX, Proposition 20:[9] Depending on how we formally write the above statement, the usual proof takes either the form of a proof by contradiction or a refutation by contradiction.
If we formally express Euclid's theorem as saying that for every natural number
Suppose to the contrary that no such p exists (an application of proof by contradiction).
[10] Let us take a second look at Euclid's theorem – Book IX, Proposition 20:[9] We may read the statement as saying that for every finite list of primes, there is another prime not on that list, which is arguably closer to and in the same spirit as Euclid's original formulation.
In this case Euclid's proof applies refutation by contradiction at one step, as follows.
, it will be shown that at least one additional prime number not in this list exists.
The classic proof that the square root of 2 is irrational is a refutation by contradiction.
a/b = √2 by assuming that there exist natural numbers a and b whose ratio is the square root of two, and derive a contradiction.
[14][15] G. H. Hardy described proof by contradiction as "one of a mathematician's finest weapons", saying "It is a far finer gambit than any chess gambit: a chess player may offer the sacrifice of a pawn or even a piece, but a mathematician offers the game.
"[16] In automated theorem proving the method of resolution is based on proof by contradiction.