FOM: Second order logic

[John Mayberry]

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

John Mayberry
School of Mathematics
University of Bristol

-----------------------------
John Mayberry
J.P.Mayberry at bristol.ac.uk
-----------------------------