Explosion and Cut Required

[Harvey Friedman]

Neil Tennant https://cs.nyu.edu/pipermail/fom/2022-May/023369.html writes:

"Once again, I wish to emphasize: Classical Core Logic is adequate for the
fully rigorous formalization of the classical mathematical reasoning that
you actually find in the mathematical literature."

My reading of this is that it is false and I would like to hear from
any FOM reader who will defend Tennant's position. The resolution
might be that Classical Core Logic really does have explosion and cut
both as explicit ready to use for immediate use, rules. However
Tennant seems to deny this. So based on that, his claim must be false.

Formalization of mathematics demands that the usual proof of things
like the empty set is contained in every set and a set is contained in
every set if and only if it is equalied to the empty set, must be
formalized as conceived and expressed normally by mathematicians
throughout the world. Core Logic is not sufficient for that as
literally presented.

With regard to other aspects of mathematics that Core Logic does not
adequately formalize in any sense, there is the matter of cut.

I made a point of stating a largely formalism free notion of using
cut. That is, the subformula property.

Mathematicians will routinely work in some sugared form of ZFC and use
certain axioms A1,...,Ak from there, and then prove by pure logic a
theorem T. And in the course of proving T they will routinely involve
formulas way way way far from being subformulas of the theorem T and
A1,...,Ak.

So there are two aspects of formalization of mathematics that are
essential and many more of course.

1. There must be the derivation of anything from a contradiction,
which is used quite a bit by mathematicians.

2. There must be proofs of theorems T which use formulas that are way
way beyond being any kind of subformula of T and the axioms used to
logically derive T.

In the normal way of looking at what cut means, one definitely is
proving T from mathematical axioms A1,...,An using the cut rule. Of
course one can make up artificially idiosyncratic systems of logic for
which the subformula property may not apply to "cut free". That
doesn't count, as it is the subformula property that is so badly false
in the formalization of real mathematics.

The standard example of where one knows that one has a blowup in any
sense of the word if you want "cut free" or "subformula property".

THEOREM. Induction for P holds up through 2^2^2^2^2^2^2^2.

This is proved using the usual axioms for successor, recursion
equations for addition, and recursion equations for base 2
exponentiation, using a blatantly non subformula of the theorem
statement and the few axioms I stated. The proof is maybe, if written
out completely, something like 10 pages of normal mathematical text.
But we know that if we have cut free or for that matter any reasonable
version of the subformula property, the size of the proof will not fit
into the solar system.

The really interesting open issue here is to find real world exciting
mathematically familiar instances of this. In my
https://cs.nyu.edu/pipermail/fom/2022-May/023357.html I talked about a
real world mathematically important example, but unlike the situation
above here, I don't know of any results about blowup in the following
sense.

1. Where as above, we can show that if we want cut free or subformula
property in the usual  sense, then we can't fit the proof into the
solar system.

2. Where if we use any known natural cut elimination or reduction to
subformula property, then we actually get a proof that can't fit in
the solar system.

Here 2 is weaker than 1, and in the case discussed in
https://cs.nyu.edu/pipermail/fom/2022-May/023357.html, one may well
have NO BLOWUP in those cases, where one is giving a different proof.

NOTE: This is the very first time since I founded FOM from my initial
low tech mailing-list-by-hand (with scholars like Dave Marker, Lou van
den Dries, Anand Pillay from applied model theory arguing about f.o.m.
to others ), to Simpson's setting up the list server facility and
moderation, to Martin Davis taking over as moderator with an Editorial
Board, that I have been in extended direct contradiction with an
author on some matters that at least have the appearance of being
technically precise. (There have been unresolved matters of course but
the issues did not even have the appearance of being technically
precise). It would be useful for the FOM readers to have others
comment on the origins of this dispute, and/or possibly to resolve it
by showing that the two parties are using terminologies in quite
different ways. In particular, I am seeking any FOM readers who can
elucidate just what Tennant is claiming.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220530/4e1400a0/attachment-0001.html>