[FOM] What is a proof?

[Stephen G Simpson]

John T. Baldwin 27 Oct 2003 writes:

 > (Of course it would only be terminological if you wanted to reserve
 > proof for the weak notiion ;-) used by fom and `good' proof for the
 > stronger notions that I am suggesting.)

Dear John,

I imagine your ;-) is intended as an indication that we are not to
take your statement too seriously.  And, you have ackowledged the
usefulness of reverse mathematics.

Nevertheless, you still seem to be overlooking the fact that "mere"
formal provability in first order logic is an extremely powerful
notion.  For example, it is powerful enough to explicate your own
vague distinction between non-explanatory proofs (Position A) versus
explanatory proofs (Position B), in a precise and illuminating way.

To spell it out, what I am proposing is that we make your vague
distinction precise, as follows:

  Definition.  Let T be a theorem of second order arithmetic, Z_2.
  Let P be a formal proof of T within the formal system Z_2.  We say
  that P is *explanatory* if the conjunction of the fintely many Z_2
  axioms used in P is logically equivalent to T, over RCA_0.

This rigorous notion of *explanatory proof* may not do everything you
want it to do, but it is good enough to make some useful distinctions.

In particular, there are many cases as above, where T is a standard
mathematical theorem, and where the obvious formalization of the
standard, textbook proof of T is *not* explanatory, because it uses
some axioms which are not logical consequences of T over RCA_0.
Furthermore, in many of these cases, it is possible to find an
alternative proof of T which *is* explanatory, in the above sense.

This is a thread that runs through the reverse mathematics literature.
I hope you appreciate this.

-- Steve

Stephen G. Simpson
Professor of Mathematics
Pennsylvania State University
http://www.math.psu.edu/simpson/