Explosion and Cut Required
aa at tauex.tau.ac.il
Wed Jun 8 01:06:01 EDT 2022
In my opinion there is an essential difference between the use of cuts and the use of SOL:
Cut allows you only to speed up proofs of theorems you can prove without it.
SOL allows you also to prove new, sometimes less certain, theorems.
Speed-up is very important, but reliability is more.
From: FOM <fom-bounces at cs.nyu.edu> on behalf of Richard Kimberly Heck <richard_heck at brown.edu>
Sent: Sunday, June 5, 2022 8:24 PM
To: Foundations of Mathematics <fom at cs.nyu.edu>
Subject: Re: Explosion and Cut Required
I won't question or even comment on Harvey's reasoning here. I will note, however, that the *form* of reasoning he employs was also used by George Boolos to argue for a stronger conclusion: that a proper formalization of ordinary mathematical reasoning must be second-order.
Boolos's argument is in "A Curious Inference", here:
Boolos focuses on this inference:
∀n(f(n,1) = s1)
∀x(f(1,sx) = ssf(1,x))
∀n∀x(f(sn,sx) = f(n,f(sn,x))
∀x(Dx → Dsx)
Boolos shows that a first-order derivation of the conclusion from the premises in any standard natural deduction system---he focuses on the one in Mates---will contain more than 2 superexp 64 symbols, but that a second-order derivation, though long, can easily be written down. In fact, Jeff Ketland formalized the inference in Isabelle/HOL, as described here:
for a different formalization.
I actually don't know if anyone has looked at what kind of comprehension is needed for this argument. Because of the way induction is used, my guess would be that the natural formalization would use Pi-1-1 comprehension.
Harvey: Do you accept Boolos's extension of your argument? Or do you think there are important differences?
Let me close by saying that, since Boolos himself gives a version of Harvey's argument in an earlier paper, "Don't Eliminate Cut":
The most significant feature possessed by natural deduction but not the method of trees, a feature that can easily seem like a virtue, is not so much that natural deduction replicates ordinary reasoning rather more faithfully than [other systems], but that it permits the development and utilization within derivations of subsidiary conclusions, or, as they would be called in a more informal setting, lemmas. In criticizing a certain pair of systems, Feferman once wrote,“ . . nothing like sustained ordinary reasoning can be carried on in either logic”. Sustained ordinary reasoning cannot be carried on in [cut-free systems], where we are unable to appeal to previously established conclusions.
I think Boolos himself may well have meant himself to pose the kind of question I just have: If you think speed-up is a good argument for a logic, then there's a good argument for second-order logic.
PS Of course, that higher-order logic provides speed-up was first proved by Gödel.
On 5/30/22 20:39, Harvey Friedman wrote:
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.
Richard Kimberly (Riki) Heck
Professor of Philosophy
Office Hours: Monday 2-3, Wednesday 3-4
Personal link: https://brown.zoom.us/my/rikiheck
Email: rikiheck at brown.edu<mailto:rikiheck at brown.edu>
Google Scholar: https://scholar.google.com/citations?user=QUKBG6EAAAAJ
Research Gate: https://www.researchgate.net/profile/Richard_Heck
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM