Explosion and Cut required

[Curtis Franks]

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/20220526/b300f244/attachment-0001.html>