Explosion and Cut Necessary

[Harvey Friedman]

Both Explosion and Cut are necessary for an adequate formalization of
mathematics. By adequate I mean

*conforming to the way mathematics think and write mathematics*

Neil tennant wrote in response to this point:

"The answer is: Very easily in Core Logic, as explained in my book *Core
Logic*, Chapter 12, 'Replies to Critics of Core Logic', Section 5: 'Reply
to Friedman and Avron'; pp.327-337.

It is a very nice rebuttal of you and Avron, but too long to fit into the
margins of this note to fom."

and makes my point very nicely. The phrase "too long to fit" is indicative.

THEOREM. emptyset is contained in A.

Proof: Let x lie in emptyset. Then x lies in A by explosion. QED

In order to be an adequate formalization of mathematics, you need to make
it roughly that short.

The idea that cut can be eliminated is even more seriously wrong in the
following sense. Removing cuts generally blows up the length of proofs
iterated exponentially. So a proof that might fit on a page could when cuts
are eliminated, result in a proof that cannot fit in the solar system.

I suggest that we leave mathematicians alone to write their proofs in the
normal way that occurs to them.

There remains the question of what do we learn from Neil's Core Logic? Well
it doesn't appear to be an appropriate way of formalizing mathematics.

So what do we learn from Core Logic?

Harvey
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220519/dda4da79/attachment-0001.html>