Explosion and Cut required

[Harvey Friedman]

Arnon Avron writes

On Fri, May 20, 2022 at 1:24 AM Arnon Avron <aa at tauex.tau.ac.il> wrote:

> This is the example  I have always given to students of a simple case in
> which
> it is clear that the mathematician's implication is indeed based on the
> truth-function
> for -> that I teach them.
>
> It is also true that the two theorems cannot be proved without using some
> form of EFQ
> (like the disjunctive syllogism).
>
> Having said that,  I should add that one can give  proofs of e.g.  Theorem
> in which the use of EFQ is rather hidden. ...
>

My main point with regard to explosion (EFQ) is that the natural
transcription of what mathematicians actually do and actually think is
using explosion. So any formalization of mathematicians without explosion
is to be rejected out of hand as a formalization of mathematics in the
normal sense of the word.

The same is true of not having cut. One conceptual way of saying that a
mathematician is using cuts is that in the course of proving a theorem,
they are using generally clever formulas that are far and even very far
from being a subformula of the theorem being proved. This occurs all the
time in real mathematics. I know of no kind of cut elimination that would
necessarily yield proofs of even simple cases of cut, that can reside
inside the solar system.

So that is a clear indication that adhering to anything like a cut free
formalization of mathematical reasoning is doomed. Of course there are some
very interesting research projects here that I would be very interested in
seeing pursued. Like a study of actual cut or cut like moves in real
mathematical contexts, what happens actually if cut elimination processes
are applied, and so forth. Also there is the question of what fragment of
mathematics can really be done without cut so that the proofs are still
under reasonable control in size and complexity.

Hence the subject title of this post.

Harvey Friedman

>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220520/63042a7a/attachment-0001.html>