[FOM] What is a proof?

[Stephen G Simpson]

John T. Baldwin 27 Oct 2003 writes:

 > Does anyone actually understand why a result several hundred pages
 > into PM holds other than by a belief that the previous lines are
 > correct?

John,

Of course we understand this kind of thing.  For instance, when 1 < 2
shows up as a theorem in Principia Mathematica, we understand that it
is a formal consequence of the axioms of PM, even if we haven't read
all the lines of the formal proof.

More broadly, and contrary to what you said, PM not only didn't impede
scientific progress, but it was actually a huge advance, in that it
showed for the first time that completely formal proofs of
mathematical theorems from appropriately basic, general, formal axioms
can actually be carried out and written down.  This insight was of
crucial importance for subsequent f.o.m. research.

Concerning Angus Macintyre's recent paper in the BSL:

 > I, for instance, found the recent BSL piece by Angus largely
 > off-base.  It proposes an interesting new project and solely for
 > propaganda purposes labels it as model theory.

This is news to me.  When I read the paper, I didn't see any specific
proposal for a new project, other than a devaluation of set theory,
and some interesting applications of model theory to algebra, of the
kind we have already seen.

An aspect of the paper that I particularly relished was Macintyre's
evident frustration and perplexity vis a vis the continued success of
set-theoretic foundations.  By the way, you never replied to my
earlier query (FOM, 9 Jul 2003):

  Does anyone know of an alternative way to set up model theory using
  some approach other than the familiar one, which is overtly
  set-theoretical?

Now, returning to the point in your recent posting, you evidently
understand that Macintyre was indeed proposing a specific new positive
project or interesting new way of looking at things.  Could you please
explain it here on FOM?

Unfortunately, Macintyre has been reluctant to discuss his ideas here
on the FOM list.  Since you are partly in the applied model theory
camp, I am asking you these questions, as a surrogate for Macintyre.

By the way, why did you find Macintyre's paper "largely off-base"?
Just because he labels his new project as model theory?  What's wrong
with calling it model theory?

-- Steve

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