Explosion and Cut required

[WILLIAM TAIT]

Hi Curtis-

You are right that eliminability of cut has two meanings: ‘the cut rule can be eliminated from the rules of proof,’  and the stronger  (but vaguer) ‘cuts can be eliminated from any pt\roof’. Proofs of Takeuti’s conjecture are proofs only of the former sense.

You are also right that Herbrand stated cut elimination; but his proof of it (in particular Lemmon 3.3) is defective. This was discovered by Peter Andrews in 1961-2—I can’t remember.  It was published in a paper by Andrews, Drebin and Anderaa in 1963.

Bill Tait

Sent from my iPad

> On May 28, 2022, at 12:00 AM, Curtis Franks <Curtis.D.Franks.7 at nd.edu> wrote:
> 
> 
> Just regarding Cut, there cannot be any controversy about whether such an inference is required in mathematical reasoning.
> 
> The Cut elimination theorem shows that the operational rules associated with logical connectives and quantifiers suffice to prove any sentence in pure logic that can be proven with them together with Cut. It is not a claim about the eliminability of Cut inferences from proofs in formalized mathematical theories. Jacques Herbrand pointed this out several years before Gentzen in his thesis: "the result shows [. . . ] that the 'rule of implication' [i.e., Cut], whose origin, after all, is in the classical syllogism, is not necessary in building logic. The rule remains necessary, however, in mathematical theories, which contain hypotheses."
> 
> What can be done with a modification of the technique of Cut elimination is to transform a proof in a formal theory like PA into a proof in which every Cut is "anchored" in the sense that (at least one occurence of) its Cut formula is a direct descendent of a formula from the non-logical axioms of the theory. What is sometimes more insightful is to embellish this procedure with conversion steps that replace instances of induction inferences with finite sequences of Cut inferences -- this is what is done, for example, in the familiar consistency proofs for PA.
> 
> In any event, none of this amounts to an argument that Cut is not required in mathematical reasoning. Instead, it can be used to show exactly where it is required (i.e., strictly speaking, not practically speaking). But that is not ordinarily thought of as a recommendation for how to go about conducting mathematics, nor even for how to go about formalizing mathematics. So the "proof theory of mathematical practice" as described seems to me to pull in two conflicting directions: Formalizing lucid pedagogical demonstrations or written transcriptions that are supposed to capture relevant reasoning involved in actual mathematical discovery will presumably have very high-level Cuts (high-complexity Cut formulas), and running the Cut elimination procedure on them will return proofs with typically lower-level Cuts. They can even be further modified to discover exactly "how much induction" is needed: For example, I believe that Sheperdson showed decades ago that there are models of arithmetic with "open induction" in which the square root of 2 is rational, so any fully reduced proof of its irrationality will have to involve induction over formulas with some quantifier complexity. But I don't see how this enterprise is going to shed any light on mathematical practice itself. It will take as input proofs that are arguably faithful representations of the reasoning found in that practice and return as output proofs that, quite apart from their size, provide insight of a very different sort than insight into that practice.
> 
> Curtis
> 
> 
>> On Wed, May 25, 2022 at 8:18 PM Harvey Friedman wrote:
>> 
>> 
>> Explosion is the rule of proof: from a contradiction derive A. Here A is
>> arbitrary, and various ways of expressing a contradiction are used in
>> mathematics.
>> 
>> Explosion is obviously necessary for any appropriate formalization of
>> mathematical practice since any appropriate formalization of mathematical
>> practice must at least readily and without change, accommodate what is
>> often taught in the mathematics curriculum. Only one person on the FOM
>> discussion above questions the necessity of explosion for any appropriate
>> formalization of mathematical practice. Are there any other subscribers or
>> readers who wish to question the necessity of Explosion in this sense?
>> 
>> Now with regards to cut. Here the situation is even stronger. Not only is
>> cut used incessantly in mathematical practice, it is rather doubtful that
>> it can be eliminated without ludicrously impractical blowup in the size of
>> the proof.
>> 
>> However, I haven't seen much with regard to the issue of cuts in actual
>> mathematical practice. In fact, we need a real subject called
>> 
>> PROOF THEORY OF MATHEMATICAL PRACTICE
>> 
>> At this point, which is near square zero, I would prefer to use a different
>> system than ZFC. I would prefer to use PA with primitive recursion. Let's
>> write this as PA(prim).
>> 
>> Let's see the use of CUTS in simple in, say, the proof of the irrationality
>> of the square root of two. Let's make the usual move by stating this as
>> "2(n^2) = m^2 has no solution in the positive integers".
>> 
>> A common way to teach this result is to first give an intuitive proof that
>> is very clear, but needs to be formalized in PA(prim). Namely, define F(n)
>> to be the number of times 2 goes into n. Then state obviously that F(nm) =
>> F(n)+F(m).
>> 
>> Now fix 2(n^2) = m^2, n,m >= 1. Then F(2(n^2)) = F(m^2), Hence 1+2F(n) =
>> 2F(m), which is a contradiction.
>> 
>> The students are asked to give a natural primitive recursion for F, and
>> then prove the LEMMA that F(nm) = F(n)+F(m), all within PA(prim).
>> 
>> This LEMMA is then plugged into the proof of a contradiction from 2(n^2) =
>> m^2, n,m >= 1.
>> 
>> So this COMPLETELY NATURAL OBSERVED PROOF in math classes has an
>> interesting web of CUT and proof by contradiction. So this shows that CUT
>> is required of any adequate formalization of mathematical practice.
>> 
>> How do we give a logical analysis of this commonly taught proof as a
>> theorem of PA(prim)? What happens when we apply cut elimination and
>> constructiviation procedures to this proof?
>> 
>> AND: do this sort of analysis of mathematical practice with elementary
>> number theory in PA(prim).
>> 
>> Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220528/ef7840fc/attachment.html>