6 ms·

Making Sense of Proof by Contradiction [pdf]

46 points by surprisetalk 4mo ago

luisgvv 4mo ago
This reminds me of the first time I was shown this in college. I loved this method so much that in my first formal logic test I tried to solve all of the problems via this method. It was a fun experience lol
dhosek 4mo ago
Worth noting, a lot of times, what people think is proof by contradiction is in fact proving the contrapositive (i.e., if you want to prove, “if p then q”, proving “if not q then not p” will also suffice).
- MaxRegret 4mo ago
  Also, proving ¬P by assuming P and deriving a contradiction is not "proof by contradiction"! That is just how you prove negations — ¬P is often taken to be syntax sugar for P ⇒ False. It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't. So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.
  - markovblanket 4mo ago
    woah truee
  - saithound 4mo ago
    "It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction" was a neologism introduced by Andrej Bauer in a 2010 discussion with Timothy Gowers. Most mathematicians have never heard of it. Those who have tend to scoff, even in CS and constructive mathematics, and call any proof that "supposes for a contradiction that X" a proof by contradiction. Take a look at Douglas Bridges calling the sqrt 2 proof a standard proof by contradiction [1], or Lars Birkedal in the proof of Lemma 6.6 here [2]. Bauer is a very productive mathematician who maintains a well-read blog, and it was through that blog that the phrase began to circulate, eventually becoming something of a shibboleth, signaling, perhaps a rather superficial acquaintance with the subtleties of intuitionistic logic. [1] https://www.dsbridges.com/myths-about-constructive-mathematics https://www.dsbridges.com/myths-about-constructive-mathemati... [2] https://cs.au.dk/~birke/papers/locrcg.pdf https://cs.au.dk/~birke/papers/locrcg.pdf
    - MaxRegret 4mo ago
      Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth, rather than a reasonable view of what a proof by contradiction is? I agree with what you say about mathematicians, being in an adjacent field myself. However, most mathematicians are not logicians, and we are seldom careful about making distinctions that only matter in non-classical logics. I do think that this particular distinction (between proving negation vs. proving the negation of a negation) is worth making, though. Even if we are, as a matter of practice, used to invoking the law of the excluded middle without a second thought, I think it's good to keep in mind in which proofs it is actually required and where it is not. So, for example, and to the GP's point, proving ¬Q ⇒ ¬P by proving P ⇒ Q doesn't require LEM, but the converse does. The trouble is that when translating mathematics to logic, it's often not clear what is a negation and what isn't. Is "x is irrational" the sentence ¬P for P being "x is rational" or is it simply an atomic sentence on its own? One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.
      - saithound 4mo ago
        For the working logician or the constructive mathematician, the distinction that matters is whether an argument uses a constructively invalid instance of the law of excluded middle (or double-negation elimination) or not. Indeed, long before 2010, they already had perfectly serviceable language for this sort of thing: they said "this proof uses DNE". They do not need a separate, additional term for "this proof of this particular form uses DNE at a very specific place". > One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians. Bridges, cited above, coauthored with Bishop the main monograph on constructive analysis. Birkedal, for his part, might fairly be said to have done as much as anyone to shape what we now call modern realizability. They don't scoff at these questions, they take them rather seriously. Yet like almost all mathematicians AND most other logicians, they chose not to use Bauer's terminology. > Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth? It's something of a shibboleth because it reveals the speaker first encountered the field through pop literature like blog posts (there is nothing wrong with that), and has not then spent sufficient time with the primary literature to realize that this is not, in fact, customary terminology used by most of those who work in the discipline proper. So it marks the speaker as somebody likely to have somewhat superficial knowledge of the field.
sunday_serif 4mo ago
For me, proof by contradiction only clicked (recently!) once I understood that logical consequence and unsatisfiability are equivalent. Once I understood that and reframed the contradiction as a statement about unsatisfiability… I could then see directly how the positive result you get is the equivalent logical consequence. Unfortunately, I feel like this intuition only really helps if you are pretty immersed in formal logic… otherwise it just sounds like jibberish.
- SkiFire13 4mo ago
  If you are into constructive logic then this will only work for proving negative statements (where indeed the definition is the same as what a proof by contradiction would give you). For positive statements you won't get back a direct proof term of your initial statement, but rather a proof of a double negation of it.
calf 4mo ago
It's interesting that even a child can do it, but actually explaining it clearly gets confusing. One problem is that as soon as you use "Suppose A then following steps S we get not A", but a hidden, implied premise is the stipulation that the world you are reasoning about already has certain consistency properties. This premise is what trips people (students like me) up because it is not part of the rules of algebra, geometry, etc.
- laichzeit0 4mo ago
  What’s assumed and not explicitly stated is the law of the excluded middle. That A is true or A is false and those are the only 2 possibilities. If you assume the law of the excluded middle then it’s impossible that “A or not-A” is false. So it’s true. But “A or not-A” is true is equivalent to “A and not-A” is false (just apply DeMorgan). So proof by contradiction is you assuming something B is true and it leading to a “A and not-A” (contradiction) so clearly B must be false.
  - calf 4mo ago
    See, that's the thing. If you are saying Law of Excluded Middle matters for justification of using proof by contradiction, then we are suddenly really talking about the justification or not of classical versus non classical logics. That's kind of the author's point in the last paragraph of his article, that there's a metamathematical thing going on even if the student cannot quite articulate it. The real problem is not LEM's place in propositional logic but the cognitive move of hypothetical reasoning. Even the article leaves the question open ended. To make this less abstract, note that in your own example you used a proof by contradiction to justify the technique of proof by contradiction. That is inherently problematic.
  - adrian_b 4mo ago
    No, the law of the excluded middle is not relevant for a demonstration by "reductio ad absurdum", when it is performed correctly. If P is a proposition and it is demonstrated that "P implies not P", from this it can be concluded that P cannot be true and this conclusion is valid in any kind of logic, even if the law of the excluded middle is false. Only in bivalent logic, where the law of the excluded middle is true, from the fact that a proposition is not true it can be concluded that it is false. This is a separate thing, which has nothing to do with the technique of demonstration by a variant of reductio ad absurdum, where the goal is to prove the implication from P to not P.
butokai 4mo ago
This document misses the point in a way that very commonly arises when mathematicians (as opposed to logicians) discuss proof by contradiction. The examples in this document all revolve around assuming a fact, showing that it would lead to an absurd, and thus establishing that that fact can’t be the case: there is no rational equal to sqrt(2), there is no finite listing of all the primes. They are not using proof by contradiction at all, and on the contrary these proof are fully constructive: if one where to give us what they believe is a finite list of all the primes, the proofs gives us a method to construct a new prime. Proof by contradiction, on the other side, deems that we derive a contradiction from the assumption that a statement does not hold. Then, by contradiction, we may state that is true because it is impossible for it to be false. This is why it is rejected by the intuitionists and constructivists: there is no way to extract an explicit procedure from such a proof, since it only states that what can’t be false must me true.
- adrian_b 4mo ago
  "What can’t be false must me true" is what classic logic called "Tertium non datur", and which has absolutely nothing to do with a demonstration by "Reductio ad absurdum", i.e. with "assuming a fact, showing that it would lead to an absurd". A demonstration by "Reductio ad absurdum" can also be done in multivalent logic, for instance in trivalent logic, where a statement can be true or false or neither true nor false, therefore "Tertium non datur" is not applicable. In my opinion, trivalent logic is the simplest kind of logic that is applicable to mathematics or to the real world. Its subset that is bivalent logic is interesting as an object of study but not as a technique that can be useful for practical reasoning or for mathematical demonstrations. If I understood you correctly, you want to distinguish the following 2 kinds of demonstrations, where P1 and P2 are propositions: 1. One demonstrates that "P1 implies not P1". From this it can be concluded that P1 cannot be true. 2. One demonstrates that "P1 implies not P2". But it is known that P2 is true. From these 2 facts it can be concluded that P1 cannot be true. Which of these 2 you call "proof by contradiction"? Probably a better name is needed, because both kinds of demonstrations end in a contradiction, the first contradicts the premise, while the second contradicts an independently known fact. EDIT: Another poster has provided a link to someone who uses the following definition: "A proof by contradiction is a proof of a positive by refutation of the negative." I believe that such a definition refers to a thing so trivial that it does not deserve a special name. Obviously if P is a proposition and it is shown that "not P cannot be true" (refutation of the negative), only in bivalent logic it can be concluded that P must be true. In trivalent logic, that only proves that P is either true or neither true nor false. In real life, bivalent logic is never applicable, as the statements that are neither true nor false are much more frequently encountered than those that are known to be either true or false. So in real life, any "demonstration" by refutation of the negative is almost certainly a logical fallacy.
leephillips 4mo ago
All difficult conjectures should be proved by reductio ad absurdum arguments. For if the proof is long and complicated enough you are bound to make a mistake somewhere and hence a contradiction will inevitably appear, and so the truth of the original conjecture is established QED. -- John Barrow

46 points by surprisetalk 4mo ago

This reminds me of the first time I was shown this in college. I loved this method so much that in my first formal logic test I tried to solve all of the problems via this method. It was a fun experience lol

dhosek 4mo ago

Worth noting, a lot of times, what people think is proof by contradiction is in fact proving the contrapositive (i.e., if you want to prove, “if p then q”, proving “if not q then not p” will also suffice).

MaxRegret 4mo ago
Also, proving ¬P by assuming P and deriving a contradiction is not "proof by contradiction"! That is just how you prove negations — ¬P is often taken to be syntax sugar for P ⇒ False. It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't. So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.
- markovblanket 4mo ago
  woah truee
- saithound 4mo ago
  "It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction" was a neologism introduced by Andrej Bauer in a 2010 discussion with Timothy Gowers. Most mathematicians have never heard of it. Those who have tend to scoff, even in CS and constructive mathematics, and call any proof that "supposes for a contradiction that X" a proof by contradiction. Take a look at Douglas Bridges calling the sqrt 2 proof a standard proof by contradiction [1], or Lars Birkedal in the proof of Lemma 6.6 here [2]. Bauer is a very productive mathematician who maintains a well-read blog, and it was through that blog that the phrase began to circulate, eventually becoming something of a shibboleth, signaling, perhaps a rather superficial acquaintance with the subtleties of intuitionistic logic. [1] https://www.dsbridges.com/myths-about-constructive-mathematics https://www.dsbridges.com/myths-about-constructive-mathemati... [2] https://cs.au.dk/~birke/papers/locrcg.pdf https://cs.au.dk/~birke/papers/locrcg.pdf
  - MaxRegret 4mo ago
    Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth, rather than a reasonable view of what a proof by contradiction is? I agree with what you say about mathematicians, being in an adjacent field myself. However, most mathematicians are not logicians, and we are seldom careful about making distinctions that only matter in non-classical logics. I do think that this particular distinction (between proving negation vs. proving the negation of a negation) is worth making, though. Even if we are, as a matter of practice, used to invoking the law of the excluded middle without a second thought, I think it's good to keep in mind in which proofs it is actually required and where it is not. So, for example, and to the GP's point, proving ¬Q ⇒ ¬P by proving P ⇒ Q doesn't require LEM, but the converse does. The trouble is that when translating mathematics to logic, it's often not clear what is a negation and what isn't. Is "x is irrational" the sentence ¬P for P being "x is rational" or is it simply an atomic sentence on its own? One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.
    - saithound 4mo ago
      For the working logician or the constructive mathematician, the distinction that matters is whether an argument uses a constructively invalid instance of the law of excluded middle (or double-negation elimination) or not. Indeed, long before 2010, they already had perfectly serviceable language for this sort of thing: they said "this proof uses DNE". They do not need a separate, additional term for "this proof of this particular form uses DNE at a very specific place". > One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians. Bridges, cited above, coauthored with Bishop the main monograph on constructive analysis. Birkedal, for his part, might fairly be said to have done as much as anyone to shape what we now call modern realizability. They don't scoff at these questions, they take them rather seriously. Yet like almost all mathematicians AND most other logicians, they chose not to use Bauer's terminology. > Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth? It's something of a shibboleth because it reveals the speaker first encountered the field through pop literature like blog posts (there is nothing wrong with that), and has not then spent sufficient time with the primary literature to realize that this is not, in fact, customary terminology used by most of those who work in the discipline proper. So it marks the speaker as somebody likely to have somewhat superficial knowledge of the field.

sunday_serif 4mo ago

For me, proof by contradiction only clicked (recently!) once I understood that logical consequence and unsatisfiability are equivalent. Once I understood that and reframed the contradiction as a statement about unsatisfiability… I could then see directly how the positive result you get is the equivalent logical consequence. Unfortunately, I feel like this intuition only really helps if you are pretty immersed in formal logic… otherwise it just sounds like jibberish.

SkiFire13 4mo ago
If you are into constructive logic then this will only work for proving negative statements (where indeed the definition is the same as what a proof by contradiction would give you). For positive statements you won't get back a direct proof term of your initial statement, but rather a proof of a double negation of it.

calf 4mo ago

It's interesting that even a child can do it, but actually explaining it clearly gets confusing. One problem is that as soon as you use "Suppose A then following steps S we get not A", but a hidden, implied premise is the stipulation that the world you are reasoning about already has certain consistency properties. This premise is what trips people (students like me) up because it is not part of the rules of algebra, geometry, etc.

laichzeit0 4mo ago
What’s assumed and not explicitly stated is the law of the excluded middle. That A is true or A is false and those are the only 2 possibilities. If you assume the law of the excluded middle then it’s impossible that “A or not-A” is false. So it’s true. But “A or not-A” is true is equivalent to “A and not-A” is false (just apply DeMorgan). So proof by contradiction is you assuming something B is true and it leading to a “A and not-A” (contradiction) so clearly B must be false.
- calf 4mo ago
  See, that's the thing. If you are saying Law of Excluded Middle matters for justification of using proof by contradiction, then we are suddenly really talking about the justification or not of classical versus non classical logics. That's kind of the author's point in the last paragraph of his article, that there's a metamathematical thing going on even if the student cannot quite articulate it. The real problem is not LEM's place in propositional logic but the cognitive move of hypothetical reasoning. Even the article leaves the question open ended. To make this less abstract, note that in your own example you used a proof by contradiction to justify the technique of proof by contradiction. That is inherently problematic.
- adrian_b 4mo ago
  No, the law of the excluded middle is not relevant for a demonstration by "reductio ad absurdum", when it is performed correctly. If P is a proposition and it is demonstrated that "P implies not P", from this it can be concluded that P cannot be true and this conclusion is valid in any kind of logic, even if the law of the excluded middle is false. Only in bivalent logic, where the law of the excluded middle is true, from the fact that a proposition is not true it can be concluded that it is false. This is a separate thing, which has nothing to do with the technique of demonstration by a variant of reductio ad absurdum, where the goal is to prove the implication from P to not P.

butokai 4mo ago

This document misses the point in a way that very commonly arises when mathematicians (as opposed to logicians) discuss proof by contradiction. The examples in this document all revolve around assuming a fact, showing that it would lead to an absurd, and thus establishing that that fact can’t be the case: there is no rational equal to sqrt(2), there is no finite listing of all the primes. They are not using proof by contradiction at all, and on the contrary these proof are fully constructive: if one where to give us what they believe is a finite list of all the primes, the proofs gives us a method to construct a new prime. Proof by contradiction, on the other side, deems that we derive a contradiction from the assumption that a statement does not hold. Then, by contradiction, we may state that is true because it is impossible for it to be false. This is why it is rejected by the intuitionists and constructivists: there is no way to extract an explicit procedure from such a proof, since it only states that what can’t be false must me true.

adrian_b 4mo ago
"What can’t be false must me true" is what classic logic called "Tertium non datur", and which has absolutely nothing to do with a demonstration by "Reductio ad absurdum", i.e. with "assuming a fact, showing that it would lead to an absurd". A demonstration by "Reductio ad absurdum" can also be done in multivalent logic, for instance in trivalent logic, where a statement can be true or false or neither true nor false, therefore "Tertium non datur" is not applicable. In my opinion, trivalent logic is the simplest kind of logic that is applicable to mathematics or to the real world. Its subset that is bivalent logic is interesting as an object of study but not as a technique that can be useful for practical reasoning or for mathematical demonstrations. If I understood you correctly, you want to distinguish the following 2 kinds of demonstrations, where P1 and P2 are propositions: 1. One demonstrates that "P1 implies not P1". From this it can be concluded that P1 cannot be true. 2. One demonstrates that "P1 implies not P2". But it is known that P2 is true. From these 2 facts it can be concluded that P1 cannot be true. Which of these 2 you call "proof by contradiction"? Probably a better name is needed, because both kinds of demonstrations end in a contradiction, the first contradicts the premise, while the second contradicts an independently known fact. EDIT: Another poster has provided a link to someone who uses the following definition: "A proof by contradiction is a proof of a positive by refutation of the negative." I believe that such a definition refers to a thing so trivial that it does not deserve a special name. Obviously if P is a proposition and it is shown that "not P cannot be true" (refutation of the negative), only in bivalent logic it can be concluded that P must be true. In trivalent logic, that only proves that P is either true or neither true nor false. In real life, bivalent logic is never applicable, as the statements that are neither true nor false are much more frequently encountered than those that are known to be either true or false. So in real life, any "demonstration" by refutation of the negative is almost certainly a logical fallacy.

leephillips 4mo ago

All difficult conjectures should be proved by reductio ad absurdum arguments. For if the proof is long and complicated enough you are bound to make a mistake somewhere and hence a contradiction will inevitably appear, and so the truth of the original conjecture is established QED. -- John Barrow