4 ms·

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 synt

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 3mo ago
woah truee
saithound 3mo 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 3mo 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 3mo 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.
    - MaxRegret 3mo ago
      Is your position that the term "proof by contradiction" should not be limited to proofs of ¬¬P followed by double negation elimination, and should instead also encompass proofs of ¬P that start with "suppose P, for contradiction"? I agree that this is in keeping with traditional usage. But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience): 1. Intuitionistic logic does not admit proof by contradiction. 2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid. I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link. The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time. I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry. To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.

markovblanket 3mo ago

woah truee

saithound 3mo 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 3mo 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 3mo 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.
  - MaxRegret 3mo ago
    Is your position that the term "proof by contradiction" should not be limited to proofs of ¬¬P followed by double negation elimination, and should instead also encompass proofs of ¬P that start with "suppose P, for contradiction"? I agree that this is in keeping with traditional usage. But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience): 1. Intuitionistic logic does not admit proof by contradiction. 2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid. I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link. The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time. I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry. To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.