FOM: Second order logic
John Mayberry
J.P.Mayberry at bristol.ac.uk
Fri Mar 5 06:24:39 EST 1999
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
-----------------------------
More information about the FOM
mailing list