Making Sense of Proof by Contradiction [pdf]
foster77.co.uk
foster77.co.uk
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.
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.
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.
Unlike in that unambiguous definition, the words used by you are confusing, because "we reach a contradiction" is also applicable to the 2 variants of "Reductio ad absurdum" that I have described.
A demonstration like "a proof of a positive by refutation of the negative" is valid only in strictly bivalent logic and invalid in any multivalent logic.
The 2 variants of "Reductio ad absurdum" that I have mentioned are also valid in any multivalent logic or modal logic.
- [1] "https://existentialtype.wordpress.com/2017/03/04/a-proof-by-...
Now to prove P by contradiction, is to assume, the contrary, ¬P and construct an impossibility. But what you have really done here is prove ¬¬P. Now if you are a normal mathematician, you are classical, and hence you believe every statement A is either true or false, i.e. A∨¬A (A or not A, from any statement A, i.e. the law of the excluded middle). It just so happens that if you accept the law of the excluded middle then from ¬¬P you can deduce P.
An interesting question is why is the meaning of a proof of negation the construction of an absurdity? I guess this is philosophical, but if you accept the point of logic is to only conclude true things, then concluding an absurdity must be impossible, and hence if you assume something that leads to an absurdity, it follows that there must be no proof of the assumption because otherwise you'd have a proof of absurdity, and hence the meaning of a negation is showing that there is no proof of the pre-negated statement. In logic, ⊥ is used as the symbol for absurdity. Hence ¬P is really shorthand for P⇒⊥ (P implies absurdity), which is why earlier I identified A∧¬A with absurdity since when you have A and A implies absurdity, you immediately deduce absurdity.
You give me a rational candidate p/q for log 2 and by the argument of the article I “construct” that p = q = 0.
In both instances I create a contradiction thus showing that you could not have provided me such a rational to begin with.
Now let me show you non-constructively that there are irrationals a and b with a^b rational.
To prove this I consider c = √2^√2. I don’t know whether this is rational or irrational so I invoke the law of the excluded middle.
Suppose c is rational. Then take a = b = √2 and we have a^b = c where a and b are irrational and c is rational.
Otherwise suppose c is irrational. Then take a = c and b = √2 and we have a^b = (√2^√2)^√2 = √2^2 = 2 and again we have our result.
What is the difference here? I have no idea whether c is rational or irrational. Either way I can make it work but I can’t tell you which possibility is the genuine one.
You can actually make better choices of a and b and show this result constructively.
This leads to a deeper question. Are there statements with no constructive proof and how do you prove that. This is beyond my expertise, but there are indeed high-powered logical tools that allow you prove such results for certain statements.
The stuff that human beings have done by simply looking at the stars and dreaming really hard is pretty awe-inspiringly incredible.
The article enters this territory at the last paragraph and simply concludes "This can be difficult questions to resolve to student's satisfaction", without even trying to answer it.
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.
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.
So proving P=>~P does not imply P is false. It means our context is inconsistent. It could be inconsistent because of P or because of Q?
-- John Barrow
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.
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-mathemati...
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.
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.
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.
Fwiw, I am in full agreement, and it's commendable when people do have at least a basic understanding of intuitionistic logic.
My remark was simply that the majority in the field don't make this (barely 16 years old) distinction between "proof of negation" and "proof by contradiction", and it has come to be associated with a more introductory or superficial understanding. This is not to suggest that everyone who uses Bauer's terms has a superficial understanding, e.g. Bauer and Escardo are top tier and certainly use it a lot.
I also don't say that this distinction is unique to Bauer. I'm saying he invented and popularized it (I was in fact there in the 2010 thread where it was invented).
With that out of the way:
> It's simply a way to square two widely-held beliefs, even amongst professional mathematicians [...] > > 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.
Well, yes, one should correct the first widely held belief, because it is a baseless misconception (or rather, was a baseless misconception under the reading of everyone before 2010).
There is no necessity to divide it into “two kinds,” or to speak of positive and negative statements though. If one assumes not-X and thereby arrives at a contradiction, then one has indeed established that not-X is not the case. This works the same way in both classical and intuitionistic logic, in both classical and constructive mathematics.
If you have some way of going from not-not-X to X, then you also proved X. The difference between classical logic and intuitionistic logic is that the latter does not admit any general way of going from not-not-X to X.
This is what's actually going on, and it's entirely orthogonal to proofs by contradictions. Redefining "proof by contradiction" to make a common misconception come out right does not help communicate this in any way, since the end of a proof by contradiction is not the only place where double negations are eliminated in classical mathematics.
If anything, it obscures what is going on: mathematicians usually come away with more misconceptions, like "in constructive mathematics you are not allowed to assume a negative". And it makes it a fair bit harder for constructive mathematicians to converse clearly with the rest of the mathematical world.
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