[FOM] Theory of Actual Proofs

[Mark Steiner]

    I think the Theory of Actual Proofs might be quite interesting
philosophically.  It can also be regarded as answering various
Wittgensteinian challenges, to the effect that formal techniques can never
capture mathematical practice--but I won't go into details here.  (I'll just
mention that W was always complaining that the "logicists'" approach that
definition is nothing but abbreviation seriously falsifies the nature of
mathematics.  This new approach puts definition back into the heart of
things.

    Here is an example of a question that I would expect our fom experts to
be able to answer--it's a question I have had for many years but could never
formalize as a mathematical question:

The Goedel formula G(n) for PA cannot be proved (if PA is consistent) yet
for every n, one can prove G(n) and I would imagine that the proofs would be
classified as "trivial."

Now consider a formula with more variables PHI(n,x,y,z)  Fermat's last
theorem has such a form.  Before the  proof of the formula PHI(n,x,y,z) one
could have imagined that the theorem is true, yet unprovable in PA (or even
ZFC), yet for each n separately, we could have a "different" proof (one
using different ideas, inequivalent in some sense) of the FORMULA
PHI(n,x,y,z) for each n.  Or at least that we could have a proof idea that
works up to n = a, another one that works for n=b>a, so that we get a
succession of "inequivalent" proofs getting higher and higher in n, as in
fact started to happen.

Fermat's theorem turned out not to fit this bill, but is there a way to
define an appropriate idea of "inequivalent" so that the question could be
asked for other such formulas of PA?