[FOM] What is a proof?

[John T. Baldwin]

Simpson wrote:

>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?
>
Does anyone actually understand why a result several hundred pages into 
 PM holds other than
by a belief that the previous lines are correct?

>
> > 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 is irrelevant, but this is libel.   :-)    While I have some 
interests in what you choose to call applied model theory
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.

Back to the point of the post.

>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).
>
I was of course aware of this connection.  And reverse mathematics joins 
the long tradition (e.g 1_01 axioms
equivalent to the axiom of choice )_ of investigations in this line. 
 This is certainly a valuable contribution
of reverse mathematics.

Steve again:

>
>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?
>
>  
>
I think I made several specific suggestions in my original note.  
First I am analyzing the notion of proof not equivalence of theorems. 
 (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.)

So I asked for `relevance'  and `significance' and suggested how these 
might be formalized.  In the second case a very ill-formed suggestion
which I have not yet refined.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20031027/da90fa26/attachment.html