Explosion and Cut Required

[Richard Kimberly Heck]

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:
https://www.jstor.org/stable/30226368
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))
     D1
     ∀x(Dx → Dsx)
     ∴ Df(ssss1,ssss1)
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:
https://criticathink.wordpress.com/2021/02/09/booloss-curious-inference-in-isabelle-hol/
See also:
http://mizar.org/trybulec65/20.pdf
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":
https://www.jstor.org/stable/30226313
concluding:

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.

Riki

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 Tennanthttps://cs.nyu.edu/pipermail/fom/2022-May/023369.htmlwrites:
> "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 myhttps://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

-- 
----------------------------
Richard Kimberly (Riki) Heck
Professor of Philosophy
Brown University

Office Hours: Monday 2-3, Wednesday 3-4
Monday:https://brown.zoom.us/j/92705928838
Wednesday:https://brown.zoom.us/j/99591098476
Personal link:https://brown.zoom.us/my/rikiheck

Pronouns: they/them/their

Email:rikiheck at brown.edu
Website:http://rkheck.frege.org/
Blog:http://rikiheck.blogspot.com/
Amazon:http://amazon.com/author/richardgheckjr
Google Scholar:https://scholar.google.com/citations?user=QUKBG6EAAAAJ
ORCID:http://orcid.org/0000-0002-2961-2663
Research Gate:https://www.researchgate.net/profile/Richard_Heck
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220605/bbbb4a3f/attachment-0001.html>