FOM: Second order logic

[John Mayberry]

	Pat Hayes points out that Tarski's definition of satisfaction 
in a structure "does seem to involve sets centrally in the very 
business of logic". He could have gone on to observe that the natural 
definitions of the basic logical notions - universal validity, logical 
consequence, and logical consistency (satisfiability) - all involve set 
theory in an even more essential way. (When I speak of "set theory" 
here I am speaking "naively" of the theory of the domains of discourse 
of the structures to which Tarski's definition applies.)
 	It has, of course, been argued, that these basic notions of 
global semantics can, in the case of conventional 1st order logic, be 
characterised in a purely syntactic, proof-theoretical manner using any 
one of the many proof systems for that logic, and, strictly speaking, 
this is perfectly correct. But I don't think this pre-Tarskian way of 
looking at 1st order logic is intellectually coherent. It doesn't 
really make sense, for example, to take provability in a particular 
formal system as the fundamental *definition* of 1st order logical 
validity. Of course we have clear intuitions of the *soundness* of such 
systems: that requires us to consider the axioms and rules of the 
system only individually and singly. But we have no intuitions that 
would guarantee their *completeness*, for that requires us to confront 
those axioms and rules as a whole. And knowledge of completeness is 
essential, since without it we would be haunted by the possibility that 
we had failed to incorporate some essential principle of logic in our 
formal system.
 	Once we see that the *semantic* definitions of validity, 
logical consequence, and logical consistency are primary, then we have 
a prima facie case for regarding 2nd order logic as a bona fide logic. 
After all, Tarski's satisfaction definition for 2nd order languages is, 
on the face of it, of a piece with the corresponding definition for 1st 
order languages. And the basic *semantic* definitions of logical 
validity, logical consequence, and logical consistency (satisfiability) 
in the 2nd order case are exactly analogous to the corresponding 1st 
order definitions. Of course this depends on our assuming that our 
"sets" - the domains of our structures - have power sets. But we do 
assume this, at least in ordinary mathematics. (Are their groups which 
cannot support a topology, for example?) Indeed, most of the axiomatic 
theories studied informally by mathematicians can be formalised only in 
second order logic. By this I just mean that if you want your formal 
axioms to define exactly the same class of structures defined by the 
informal axioms then you have to use second order logic.
 	Many of the first order theories that mathematical logicians 
study are the first order reducts of second order theories, and they 
are natural only insofar as they *are* reducts of this sort. Perhaps we 
wouldn't be so surprised at the incompleteness of 1st order PA if we 
did not know that 2nd order PA is categorical, and therefore complete. 
Of course this completeness is of no practical help in discovering 
arithmetical truths since 2nd order logic has no complete systems of 
proof procedures. As Steve Simpson has pointed out, if you want to 
study 2nd order logical consequence you ought to embed your discussion 
in some appropriate first order theory so you can bring the powerful 
proof theoretic and model theoretic techniques of modern logic to bear 
on it.
	 A	A natural 1st order theory in which to study 2nd order 
logic is ZF. But ZF is itself the 1st order reduct of a 
(semi-)categorical theory, and that raises interesting issues 
concerning the status of the 2nd order version of ZF. There's a good 
discussion of these matters in Stuart Shapiro's book. (Like Steve 
Simpson I was put off by Shapiro's animadversions against 
"foundationalism" in his early chapters; but you don't have to agree 
with him about that to find his later discussion about the connections 
between ZF and 2nd order logic interesting.)
 	What is the "set theory" that underlies Tarskian semantics? I 
think it is the Zermelo-Fraenkel system. But you can't simply identify 
that system with the first order theory ZF. You have to take the notion 
of set *seriously*. Otherwise you can't make sense of the notion of an 
axiomatic theory, 1st or 2nd order. But I've now come full circle, so 
I'll stop.

John Mayberry
School of Mathematics
University of Bristol
-----------------------------
John Mayberry
J.P.Mayberry at bristol.ac.uk
-----------------------------