← @EscardoMartin Twitter archive

Martin Escardo

@EscardoMartin

Proofs by contradiction are allowed in constructive mathematics:

31/10/2022, 20:44:44

Favs: 5

Retweets: 1

Martin Escardo

@EscardoMartin

The answer is that it depends what you mean by "proof by contradiction". Apparently, there isn't a consensus. I always thought that proof by contradiction meant "to prove A, assume not A and derive a contradiction". In which case the answer is "False".
1/

01/11/2022, 20:31:54

Favs: 9

Retweets: 0

Martin Escardo

@EscardoMartin

But other people insist that "proof by contradiction" includes any kind of proof that mentions a contradiction. Such as "to prove not A, assume A and derived a contradiction". This method of reasoning is allowed in constructive mathematics (as opposed to /1 above).
2/

01/11/2022, 20:34:13

Favs: 7

Retweets: 0

Martin Escardo

@EscardoMartin

For example, the thousand's year old proof of the irrationality of the diagonal of a unit square does work by assuming its rationality and reaching a contradiction. And it is constructively valid (this is an instance of 2/).
3/

01/11/2022, 20:36:08

Favs: 8

Retweets: 0

Martin Escardo

@EscardoMartin

Regardless of terminology, (1) and (2) are different methods of proof. Both in classical and constructive mathematics. Only (2) is valid in constructive mathematics.
4/

01/11/2022, 20:37:06

Favs: 8

Retweets: 0