Making Sense of Proof by Contradiction [pdf] • Hacker News Board

Re: Making Sense of Proof by Contradiction [pdf]

#11

Post by adrian_b » Sat, Jun 27, 2026, 7:34 AM UTC

butokai wrote: post #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…

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

Re: Making Sense of Proof by Contradiction [pdf]

#12

Post by calf » Sat, Jun 27, 2026, 7:43 AM UTC

laichzeit0 wrote: post #8

calf wrote: 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…

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.

Re: Making Sense of Proof by Contradiction [pdf]

#13

Post by SkiFire13 » Sat, Jun 27, 2026, 7:48 AM UTC

sunday_serif wrote: post #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 form…

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.

Re: Making Sense of Proof by Contradiction [pdf]

#14

Post by dwenzek » Sat, Jun 27, 2026, 7:52 AM UTC

butokai wrote: post #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…

Exactly! A very nice explanation of what is and what is not a proof by contradiction is given by R. Harper in "Proofs by contradiction, versus contradiction proofs" [1]

- [1] "https://existentialtype.wordpress.com/2017/03/04/a-proof-by-...

Re: Making Sense of Proof by Contradiction [pdf]

#15

Post by butokai » Sat, Jun 27, 2026, 7:57 AM UTC

adrian_b wrote: post #11

butokai wrote: post #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…

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

Neither of the two. A proof by contradiction, as other comments have stated, is: assuming not P1, we reach a contradiction; thus P1 must be true. This is equivalent to tertium non datur in classical logic. I’m not sure it’s a valid deduction in your trivalent logic.

Re: Making Sense of Proof by Contradiction [pdf]

#16

Post by sxzygz » Sat, Jun 27, 2026, 7:57 AM UTC

butokai wrote: post #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…

To be a little more concrete, what it means to prove a negation ¬P (not P) is to assume P and construct an impossibility from it, like 0=1 (assuming those symbols exist in the theory you are working with) or more generally A∧¬A (A and not A) for some A (0=1 being a absurdity, hopefully, because your ambient theory already proves 0≠1).

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.

Re: Making Sense of Proof by Contradiction [pdf]

#17

Post by adrian_b » Sat, Jun 27, 2026, 8:14 AM UTC

butokai wrote: post #15

adrian_b wrote: post #11

Earlier quoted context omitted.

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

Neither of the two. A proof by contradiction, as other comments have stated, is: assuming not P1, we reach a contradiction; thus P1 must be true. This is equivalent to tertium non datur in classical logic. I’m not sure it’s a valid deduction in your trivalent logic.

Another poster has provided a link to a definition of "proof by contradiction", which I assume that it is the one that you mean ("A proof by contradiction is a proof of a positive by refutation of the negative.").

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.

Re: Making Sense of Proof by Contradiction [pdf]

#18

Post by adrian_b » Sat, Jun 27, 2026, 8:34 AM UTC

laichzeit0 wrote: post #8

calf wrote: 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…

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.

Re: Making Sense of Proof by Contradiction [pdf]

#19

Post by futune » Sat, Jun 27, 2026, 9:31 AM UTC

butokai wrote: post #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…

I think this is a good comment. Could you also provide an example of a true (essential?) proof of contradiction of an elementary mathematical statement, to illustrate?

Re: Making Sense of Proof by Contradiction [pdf]

#20

Post by arunix » Sat, Jun 27, 2026, 11:29 AM UTC

butokai wrote: post #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…

I agree that the prime list example is really a constructive proof. But what about the sqrt(2) and log(2) examples?