[FOM] What is a proof?
John T. Baldwin
jbaldwin at uic.edu
Mon Oct 27 08:49:36 EST 2003
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
More information about the FOM
mailing list