3 ms·

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”, prov

by 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.

by dhosek 4mo ago

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.