FOM: Second order logic
J.P.Mayberry at bristol.ac.uk
Thu Mar 18 11:36:19 EST 1999
Steve Simpson says that the "sophisticated modern understanding [i.e.
of the continuum] can be summarised (somewhat over dramatically) by
saying that the absolute categoricity of the real number system is an
illusion: the real number system is categorical only within or relative
to a particular model of set theory." Now this will simply not do.
Where do these "models" of set theory reside? Inside another "model" of
set theory? If these models really are *models* then our sophisticated
moderns really ought to come clean about what these model are, what
properties they have, what constructions we can perform on them, etc.
Or is it that we can treat of them formally inside 1st order ZFC or
some alternative formal 1st order system of set theory? If, as I
suspect, the latter is what Simpson has in mind, then I'm afraid that
what he calls modern sophistication contains a large and undigested
lump of old fashioned formalism.
It seems to me that he has got the wrong idea of what
formalisation is *for*. We don't formalise our theories in order to
find out what we can prove: we formalise them in order to find out what
we *can't* prove. Only the most utterly trivial mathematical proofs can
be fully formalised in any practical sense. We don't believe our
ordinary proofs to be valid *because* they can be fully formalised in
ZFC: we believe our ordinary proofs to be fully formalisable in ZFC
because they are valid. To think otherwise is to indulge in a
completely unreal fantasy: it is to set the obvious facts of
intellectual life squarely on their heads.
I don't want to be misunderstood here. I am convinced that all
our ordinary proofs in arithmetic, analysis, geometry and set theory
*can* be formalised in 1st order ZFC. Moreover, I think that this fact
is of the utmost importance for the foundations of mathematics. If you
don't grasp this fact you can't grasp the *significance* of Godel's and
Cohen's independence results, or of the beautiful series of results
that Harvey Friedman has been producing over the last few months.
Still, although it is *true* that all our valid ordinary proofs can be
formalised in ZFC, that doesn't constitute a *definition* of what their
validity consists in. I'm not convinced that such a definition can be
This is why Steve Simpson's argument that the facts about 2nd
order definability are really first order facts after all is utterly
unconvincing. It perfectly true that because we use set theory to prove
them, we can, in principle, formalise those proof's in 1st order ZFC.
But that is quite beside the point. For we believe that we can formalise
the proof that all complete ordered fields are isomorphic because we
believe that it is valid, we don't believe that it is valid because it
can be formalised. I conjecture that it has never been formalised, and
never will be. Whatever would be the point of doing so?
School of Mathematics
University of Bristol
J.P.Mayberry at bristol.ac.uk
More information about the FOM