Live data from Hacker News

Making Sense of Proof by Contradiction [pdf]

foster77.co.uk

1–10 of 29 posts

Re: Making Sense of Proof by Contradiction [pdf]

#4
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.

Re: Making Sense of Proof by Contradiction [pdf]

#5
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.

Re: Making Sense of Proof by Contradiction [pdf]

#6
post #3

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

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.

Re: Making Sense of Proof by Contradiction [pdf]

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

Re: Making Sense of Proof by Contradiction [pdf]

#8
post #5

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,…

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.

Re: Making Sense of Proof by Contradiction [pdf]

#9
post #3

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

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…

woah truee

Re: Making Sense of Proof by Contradiction [pdf]

#10
post #3

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

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…

"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-mathemati...

[2] https://cs.au.dk/~birke/papers/locrcg.pdf

Post reply on HN