21
$\begingroup$

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?

$\endgroup$
  • 15
    $\begingroup$ 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. $\endgroup$ – Thomas Andrews Sep 5 '13 at 13:33
  • $\begingroup$ @ThomasAndrews Not really. $\endgroup$ – Billy Rubina Jan 20 '17 at 4:09
5
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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}$." $\endgroup$ – Trevor Wilson Sep 6 '13 at 16:30
  • $\begingroup$ 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. $\endgroup$ – dezakin Sep 6 '13 at 19:28
  • 1
    $\begingroup$ However the statement is a bit overreaching, so I've edited it to be more clear: The utility of proofs implicitly assume consistency. $\endgroup$ – dezakin Sep 6 '13 at 19:36
16
$\begingroup$

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.

$\endgroup$
  • 6
    $\begingroup$ 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). $\endgroup$ – user642796 Sep 5 '13 at 12:58
  • 2
    $\begingroup$ @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... $\endgroup$ – Zhen Lin Sep 5 '13 at 13:06
  • 1
    $\begingroup$ No, to deduce $Q$ from $\lnot \lnot Q$ requires LEM. The axiom scheme $\lnot \lnot Q \to Q$ is equivalent to LEM. $\endgroup$ – Zhen Lin Sep 5 '13 at 13:10
  • 1
    $\begingroup$ @ZhenLin: I should really bone up on my intuitionistic logic. You are absolutely correct. $\endgroup$ – user642796 Sep 5 '13 at 13:18
  • 2
    $\begingroup$ 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. $\endgroup$ – Zhen Lin Sep 5 '13 at 13:25
6
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I think this is just fantastic. $\endgroup$ – Benjamin Lindqvist Sep 29 '16 at 18:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.