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