Proof by Contradiction

[Harvey Friedman]

It's been a long time since I thought about issues regarding proof by
contradiction in the sense of the rule of inference that

from a contradiction derive anything

If my memory serves me right the situation is as follows as far as normal
mathematics is concerned.

1. This inference is obviously valid in the sense that any model of a
contradiction is also a model of any formula. This is by default.

2. Statements obviously true by default occur not only in mathematics but
also in ordinary discourse. For instance,

Harvey Friedman scored 100 points in every single basketball game I played
in the NBA. This is not true of Michael Jordan.

3. In some very common ways to formalize ordinary classical mathematical
reasoning, this is ordinary considered to commonly arise in the following
natural situation in the course of a fairly involved proof. One has a
division of cases, maybe 5 or so. It can be rather convenient to argue by
cases:

case 1.
case 2.
case 3.
case 4.
case 5.

and in some of these cases, one simply says "impossible". For other cases,
a hard argument ensues to get the desired conclusion.

Of course, in this situation one can avoid writing down cases that are
impossible. But I know from experience in writing complicated proofs that
it can be preferable at least for me, to carry out the argument with
"impossible cases".

4. The philosophy behind proof assistants is to support any kind of useful
obviously valid reasoning that an appreciable number of working
mathematicians find congenial and useful.

5. Now here is where my memory gets hazy. There are meta theorems to the
effect that any proof in pure logic with use of proof by contradiction in
this sense, can be effectively replaced by a proof without using proof by
contradiction. Such a result would not affect the stance taken by proof
assistants in allowing just about anything in wide use.

6. However, I don't remember some details. Firstly, this may be true in
pure logic but somehow doesn't lift properly to systems like ZFC.

7. Or even in pure logic, maybe some metatheorem about removal of proof by
contradiction depends on having cut elimination?

8. But using cut elimination here is problematic. While it is true that
every proof in pure logic has a cut free proof in pure logic, it is NOT
true that every proof in pure logic of reasonable size has a cut free proof
in pure logic of reasonable size.

So no general use of cut elimination seems possible for actual mathematical
practice. Might this mean that no general elimination of proof by
contradiction is possible for actual mathematical practice? (Haven't
thought about this for a long time).

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220517/8c4c511e/attachment-0001.html>