Explosion and Cut Required

[Harvey Friedman]

This continues the discussion from FOM postings

https://cs.nyu.edu/pipermail/fom/2022-May/023297.html
https://cs.nyu.edu/pipermail/fom/2022-May/023306.html
https://cs.nyu.edu/pipermail/fom/2022-May/023309.html
https://cs.nyu.edu/pipermail/fom/2022-May/023312.html
https://cs.nyu.edu/pipermail/fom/2022-May/023315.html
https://cs.nyu.edu/pipermail/fom/2022-May/023317.html
https://cs.nyu.edu/pipermail/fom/2022-May/023318.html
https://cs.nyu.edu/pipermail/fom/2022-May/023322.html
https://cs.nyu.edu/pipermail/fom/2022-May/023326.html
https://cs.nyu.edu/pipermail/fom/2022-May/023327.html
https://cs.nyu.edu/pipermail/fom/2022-May/023328.html
https://cs.nyu.edu/pipermail/fom/2022-May/023332.html
https://cs.nyu.edu/pipermail/fom/2022-May/023334.html
https://cs.nyu.edu/pipermail/fom/2022-May/023334.html
https://cs.nyu.edu/pipermail/fom/2022-May/023336.html
https://cs.nyu.edu/pipermail/fom/2022-May/023337.html
https://cs.nyu.edu/pipermail/fom/2022-May/023340.html
https://cs.nyu.edu/pipermail/fom/2022-May/023341.html
https://cs.nyu.edu/pipermail/fom/2022-May/023342.html

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/20220525/aa4533e0/attachment-0001.html>