[FOM] What is a proof?

[Stephen G Simpson]

John T. Baldwin 26 Oct 2003 writes:

 > Position A.  A proof is a means of establishing the truth of a
 > proposition.
 > 
 > Position B.  A proof is an explanation of why a proposition is
 > true.
 > 
 > [...]
 > 
 > To raise some hackles: Principia Mathematica was an existence proof
 > for being able to prove all mathematical truths in Sense A;
 > however, its method of establishing A, completely defeated any
 > chance of B.

Dear John,

I assume you are aiming to be provocative, in the best tradition of
FOM, which means: to provoke a good discussion of some issue or
program related to f.o.m.  However, in this case, with this evidently
gratuitous swipe at Principia Mathematica, I don't know what you are
hoping to accomplish.  In what sense, or by what stretch of the
imagination, did Principia Mathematica impede explanation?

 > But my goal today is to point out that there are technical tools - 
 > provided by ordinary logic to address Position B.

Now I will try to raise your hackles.  I imagine I will raise your
hackles to the extent that you belong to the applied model theory
camp, led by Macintyre, who is known to be upset about reverse
mathematics.

It seems to me that reverse mathematics provides a series of
excellent, highly articulated answers to your question (though
probably not the kind of answers that you were seeking).

According to Aristotle, the best kind of knowledge is knowledge of the
cause.  Thus, to fully understand and explain X, we must find the root
cause of X.  Elaborating, Aristotle said:

  Reciprocation of premisses and conclusion is more frequent in
  mathematics, because mathematics takes definitions, but never an
  accident, for its premisses -- a second characteristic
  distinguishing mathematical reasoning from dialectical disputations.
  (Posterior Analytics 78a10)
  
Thus, to fully explain a mathematical theorem, we need to prove it
from premisses which are reciprocal with it, i.e., logically
equivalent to it.

For example, let X be the existence theorem for solutions of systems
of ordinary differential equations.  The original proof merely
established X, in the sense of your Position A.  Later, by working
harder, one proved X from weaker premisses, and then reversed it,
showing that Weak K"onig's Lemma (or Sigma^0_1 Separation) is not only
sufficient but also necessary for X.  This is the main result of one
of my early papers in reverse mathematics.  Do you agree that this
result goes some distance toward *explaining* X, in the sense of your
Position B?

Of course, when you speak of *explanation*, it may be that you are
yearning for something other than "reciprocation of premisses and
conclusions".  If so, can you be more specific?

-- Steve

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