# Justification of Proofs by Contradiction

Is there a validation for the technique of proof by contradiction? Or do those who use it take its validity as an axiom?

-

The use of proof by contradiction is closely tied to the law of the excluded middle. The motivation for including this sort of proof in ordinary mathematics is that we think of each statement as being either true or false, and we think that if a statement is not true then its negation is true. If we are talking about abstract truth about a particular structure, then these are arguably self-evident principles. For example, the structure might be the semiring of natural numbers, and the statement might say that there are infinitely many primes. In this structure, it seems clear that there are either infinitely many primes (meaning the set of primes is not bounded), or there are not, and that exactly one of these alternative holds. So when we take the structure as already given, and reason about which statements are true or false in the structure, classical logic is a good framework for this sort of reasoning.

However, there are mathematical frameworks that do not include the law of the excluded middle but still include forms of proof by contradiction. For example, the usual formalization of intuitionistic logic includes the ''ex falso quodlibet'' rule: if you can prove $P \land \lnot P$ then you can conclude $Q$, for any statements $P$ and $Q$. But this logic does not, in general, prove $P \lor \lnot P$. Intuitionistic logic is a good framework if we think of a structure as only partially given, so that our knowledge of its overall properties may change over time as we discover more. To affirm a sentence in this logic, we need to know that the sentence is true based only on the part of the structure that we have seen so far. In this setting, we may not be able to affirm $P$ on the basis of the part of the structure we have seen, and we may not be able to affirm $\lnot P$ until the entire structure is known; in this case we can't affirm $P \lor \lnot P$ based only on our partial information. This logic still proves $\lnot (P \land \lnot P)$: it is impossible for the part of the structure we have seen to satisfy both $P$ and $\lnot P$. One reason that ordinary mathematics is not done this way is that ordinary mathematicians don't think of structures such as the natural numbers as only partially specified; we think of the natural numbers as a completed object.

One logical framework that includes neither ''ex falso quodlibet'' nor the law of the excluded middle is known as "minimal logic". This framework is mostly of interest in proof theory, where it's used for the purpose of stating results in more generality.

-
I would add that ex falso quodlibet is equivalent (in the presence of the other rules of inference of intuitionistic logic) to the principle of modus tollendo ponens, that is, $\{ \lnot p, p \lor q \} \vdash q$, which seems to be entirely reasonable to me! – Zhen Lin Jul 5 '11 at 14:39
@Zhen Lin: That's interesting. Could you give a hint on how to prove $\bot \to q$ from modus tollens ponens? – Carl Mummert Jul 5 '11 at 15:04
Regarding "ex falso quodlibet" and the Principle of Explosion see the prior question Why in an inconsistent axiom system every statement is true? – Bill Dubuque Jul 5 '11 at 15:29
@Carl: Well, $\{ \bot \} \vdash \bot$, and by disjunction introduction, $\{ \bot \} \vdash \bot \lor q$, so... – Zhen Lin Jul 5 '11 at 17:02
@Doug Spoonwood: You can prove that each of them is a derivable rule (i.e. an admissible rule) in the system consisting of minimal logic plus the other one. – Carl Mummert Jul 6 '11 at 2:26

A proof by contradiction works as follows. We know something is true. Let's call this something $A$, just for clarity. We want to see if some proposition $P$ is true. We determine that if $P$ is false, then $A$ is false. But this is impossible, as we know $A$ is true. So therefore we know that $P$ is true.

Is there a validation? Yes. It looks like what I just wrote. I suppose that in a way, it depends on us admitting that we know something. Really, this is covered very well on wikipedia

-
I guess it depends on the law of excluded middle. – Jonas Meyer Jul 5 '11 at 6:04
I think you're right. Is it enough? – Ernest Jul 5 '11 at 6:07
mixedmath: Thanks for your answer. I actually read the wikipedia article and didn't find it satisfactory. I think you're validating proofs by contradiction using the fact that P->Q is equivalent to not Q -> not P. What's the justification for that (going down to axioms/self-evident propositions)? – Ernest Jul 5 '11 at 6:09
@Ernest: q and (not q) is false by the law of contradiction. The law of excluded middle means that q or (not q) is true. – Jonas Meyer Jul 5 '11 at 6:09
@Jonas: Thanks. I recalled that and edited my answer before I saw your correction. – Ernest Jul 5 '11 at 6:11

Let "C" denote the material conditional, "N" negation, 0 falsity, and read via the Polish notational scheme. Then proof-by-contradiction can get justified as follows:

1. We have the rule of inference of modus ponens.

2. We have CCNp0p as a true formula for our background logic.

3. We have a rule which goes "if we have derivation which starts with a proposition q and ends with a proposition r, we may infer Cqr".

Then, it follows that if we assume the negation of a proposition Np as true, and deduce a falsity, we may then infer that Np implies a falsity, or equivalently CNp0 as true. Then since CCNp0p holds, and we have modus ponens as a rule of inference, we may infer the proposition p as true.

Of course, oftentimes, with K denoting conjunction, one takes the formula KpNp as a falsity. But, there do exist non-classical logics where KpNp isn't a falsity, and there still exist falsities in those logics. So, proof-by-contradiction still can get used, say by deducing NCpp as the falsity, given that NCpp always has truth value of false, or if Cpp is a theorem, and the negation of a theorem qualifies as a contradiction.

-
Thanks for your answer. Unfortunately, I don't understand it. Where could I read the background of what you're talking about (CNNpop, etc.)? – Ernest Jul 6 '11 at 3:25