[FOM] What is a proof?

[John Baldwin]

At 01:31 PM 10/27/2003 -0500, Stephen G Simpson wrote:

Baldwin wrote

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

At 01:31 PM 10/27/2003 -0500, Stephen G Simpson wrote:

>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.

Dear Steve,

I didn't say that PM impeded foundations.  I said that it made great 
strides in one direction, showing that there was a way to
ground mathematics on a few basic principles.  I also said that when one 
breaks mathematics down to long strings of `meaningless'
statements that this does not provide an explanation but only a 
verification.  I think this is a commonplace; not some
exceptional statement that I am making.

We seem to be at cross purposes and I will not further comment on this part 
of our conversation.  I will
respond to several other of your comments that I find more fruitful.

John