Proof by Contradiction

[Harvey Friedman]

Regarding recent posting of Ingo Blechschmidt.

There is a terminology problem here. I am talking about proof by
contradiction NOT in the sense of the law of excluded middle but in the
sense, as I thought i described it, of deriving anything from a
contradiction. I was not talking about any intuitionistic systems as you
are. I was only talking about classical systems.

The Pi01 conservative extension between classical and intuitionistic
arithmetic is due to Goedel, and is rightly credited to him if I
recall also for Pi02 sentences using if I recall his Dialetica
interpretation.. I came up with a very simple and very applicably new proof
using what is called A-translation that proves Pi02 conservation for a wide
variety of systems.

Harvey Friedman

On Wed, May 18, 2022 at 7:42 PM Ingo Blechschmidt <
ingo.blechschmidt at math.uni-augsburg.de> wrote:

> Dear Harvey,
>
> On Tue 17 May 2022 09:03:56 AM GMT, Harvey Friedman wrote:
> > 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
>
> right, this is not only a basic rule of classical logic, but also of
> intuitionistic logic (though not minimal logic).
>
> > 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.
>
> Right. Sometimes this is called "Barr's theorem". There are several
> versions of it. It states something like:
>
>     If a Π⁰₂-statement has a proof using the law of excluded middle,
>     then it also has a proof without.
>
> There are roughly two strategies for proving this metatheorem. One is
> via cut elimination (with the issues you mention). The other is using a
> combination of the double negation translation and the trick of
> employing a nontrivial exit continuation. This latter strategy ensures
> that the resulting intuitionistic proof is only polynomially larger than
> the given classical proof.
>
> A stronger version of Barr's theorem states:
>
>     If a Π⁰₂-statement has a proof using the law of excluded middle and
>     the axiom of choice, then it also has a proof not using any of these
>     axioms.
>
> The textbook proof of this metatheorem requires the axiom of choice and
> is hence not effective at all, giving no bound on the size of the
> resulting constructive proof.
>
> Some more details are in this survey paper of mine:
> https://arxiv.org/abs/2012.13850
>
> > 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).
>
> No, firstly there are several effective metatheorems to this effect and
> also a huge corpus of work in constructive mathematics evidencing that,
> with enough work, theorems of classical mathematics tend to be able to
> be recasted as theorems of constructive mathematics.
>
> Cheers,
> Ingo
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220518/deef16c5/attachment-0001.html>