# Does proof by contradiction assume that math is consistent?

The standard proof by contradiction goes like

1. It is known that $P$ is true.
2. Assume that $Q$ is true.
3. Using the laws of logic, deduce that $P$ is false.
4. Rejecting this contradiction, we are forced to accept the falsity of $Q$.

In rejecting the contradiction we implicitly assume that mathematics is consistent. However, doesn't Godel's (Second) Incompleteness Theorem tell us that the consistency of mathematics cannot be proven? Does this pose a problem?

• If mathetmatics is inconsistent, we don't care what we can prove in it, since it is useless. So worrying about the case where an axiom system is not consistent is hardly of much value. We hope our axiom systems are consistent, and we work with that assumption every day, because inconsistency is a catastrophe. Sep 5, 2013 at 13:33
• @ThomasAndrews Not really. Jan 20, 2017 at 4:09

Godel's Incompleteness Theorem does not apply to every mathematical system. However, let us suppose we are working in a system to which it applies. If our system is consistent, your proof of $\neg Q$ is meaningful. If our system is inconsistent, then everything can be proven from it. So your proof tell us that a theorem is a consequence of the axioms of our system.

• Well... you also have to assume that the law of excluded middle holds (which is probably more to the point when considering proof by contradiction). Sep 5, 2013 at 12:58
• @ArthurFischer Strictly speaking LEM is not needed for the outlined proof: if you want to prove $\lnot Q$, then it is constructively legitimate to show that assuming $Q$ leads to a contradiction. The trouble is if you want to prove $Q$ but only show that assuming $\lnot Q$ leads to a contradiction... Sep 5, 2013 at 13:06
• No, to deduce $Q$ from $\lnot \lnot Q$ requires LEM. The axiom scheme $\lnot \lnot Q \to Q$ is equivalent to LEM. Sep 5, 2013 at 13:10
• @ZhenLin: I should really bone up on my intuitionistic logic. You are absolutely correct. Sep 5, 2013 at 13:18
• A proof by contradiction is a perfectly legitimate proof, if you accept LEM. But I reiterate: the proof strategy outlined in the OP is not proof by contradiction; rather, it is a constructively valid "direct" proof of a negative statement. In particular, if you prove that $Q$ leads to a contradiction, then $Q$ is false. You may have confused this with the constructivist stance that $Q$ being true is stronger than $\lnot Q$ being false. Sep 5, 2013 at 13:25

If logic is consistent, we have proven Q false.

If logic is inconsistent, then all statements are false (and true, simultaneously).

Either way, Q is false.

• I think this is just fantastic. Sep 29, 2016 at 18:21

The utility of formal proofs implicitly assume that the formal system is consistent (except those weird paraconsistent logics). Proof by contradiction, and more generally resolution proofs, are explicitly propositional logic, which is consistent and complete. Incompleteness is introduced by rules of inference for manipulating quantifiers powerful enough to represent arithmetic, which is beyond mere proof by contradiction.

The incompleteness theorems tells us that formal systems that are powerful enough to represent Robinson arithmetic (or its stronger, more orthodox cousin Peano arithmetic) have undecidable statements, but propositional calculus isn't that powerful and is entirely decidable. Even Presburger arithmetic and extensions of it that involve multiplication by constants are SMT decidable, and are provably complete. So in short, resolution proofs themselves aren't handicapped by incompleteness.

Incompleteness means that its possible there's some new Russel's paradox out there that forces everyone to rebuild the foundations of systems strong enough to represent Robinson arithmetic. The consequences of such a hidden inconsistency is catastrophic, because then all statements can be proven (by contradiction, as you demonstrated) and the system becomes useless; But not necessarily irreparable, as we did recover from Russel's paradox. However, we can take comfort that for many useful weaker systems, they are on perfectly stable, decidable, complete ground.

• What do you mean by "proofs assume the formal system is consistent"? If, in a context where the base theory is supposed to be $\mathsf{ZFC}$, one assumes $\text{Con}(\mathsf{ZFC})$ in the course of proving a theorem, then one had better state it in the hypothesis because the notion of "theorem of $\mathsf{ZFC} + \text{Con}(\mathsf{ZFC})$" is different than the notion of "theorem of $\mathsf{ZFC}$." Sep 6, 2013 at 16:30
• If in the context where the base theory is supposed to be ZFC, one assumes Con(ZFC) if we assume a theorem of ZFC has any useful meaning at all, because if a system isn't consistent, you can prove anything from it and its useless. You have to note Con(ZFC) in certain meta-logical proof systems to formally declare what you're proving, like independence proofs by forcing. While its correct to say that the logical consequences of a proof don't assume consistency, a proof being useful does depend on it in most of the logics people are familiar with. Sep 6, 2013 at 19:28
• However the statement is a bit overreaching, so I've edited it to be more clear: The utility of proofs implicitly assume consistency. Sep 6, 2013 at 19:36

I think item $4$ in the question introduces an irrelevancy, namely "Rejecting this contradiction". Before you get to item 4, the available information is that $P$ is true and that $Q$ implies not $P$. So $Q$ implies the contradiction "$P$ and not $P$". In both classical and constructive logic, the negation of a statement is equivalent to "that statement implies a contradiction". So we have the negation of $Q$.

The role of the contradiction here is not to frighten us so that we reject it because of our belief in the consistency of mathematics. Rather it is to serve as the (standard) criterion for negation.