Proof by Contradiction

[Tennant, Neil]

Harvey,

To avoid any confusion, let's take your clarification of what you mean by "proof by contradiction" and just call it "proof by  appeal to EFQ". EFQ is the inference from absurdity to any statement you like. Intuitionistic Logic (hence also Classical Logic) has EFQ.

EFQ is not needed for a logic adequate unto the needs of science and mathematics. Nor (in the sequent setting) are the structural rules of Thinning or Cut. These two rules generate irrelevancies. Indeed, they allow one to derive EFQ. So they have to go.

Classical Core Logic (call it C+) does not have EFQ. It does not have Thinning. And it does not have Cut.

But C+ proves all classical logical truths; proves the inconsistency of any unsatisfiable set of sentences; and proves from any satisfiable set of sentences all its classical logical consequences.

Nothing more is needed of a logic for it to be adequate for science and mathematics.

You might  have a hazy recollection of the relevant metatheorems supporting these claims from some earlier exchanges on fom.

Let me know if there are any further details you might need to know about the Core systems.

Best regards,
Neil





Get Outlook for iOS<https://aka.ms/o0ukef>
________________________________
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Harvey Friedman <hmflogic at gmail.com>
Sent: Wednesday, May 18, 2022 4:50:04 PM
To: Ingo Blechschmidt <ingo.blechschmidt at math.uni-augsburg.de>
Cc: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: Proof by Contradiction

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

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<mailto: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<https://urldefense.com/v3/__https://arxiv.org/abs/2012.13850__;!!KGKeukY!y5LMIK9n5jNqg0P-fyh1cVpNu03SKitdrMWEGUF3j_YdhXaTa_8KE_Stfu6cSvtxXpSFDFymlR5nIntJtw$>

> 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/20220519/35f30e34/attachment-0001.html>