FOM: Second order logic

[Robert Black]

I say that second-order logic is an essential tool for the expression of
mathematical theories, because only in second-order logic can you have
categorical theories with infinite models.  Steve says this is 'very odd,
if not absurd'.  I take it he's not denying that only with second-order
logic can you get categorical theories with infinite models (which would be
very odd, if not absurd, on Steve's part) but rather that ability to give
categorical descriptions of mathematical structures matters in any way.
Well, I think I have an intuitive understanding of 'true sentence of
first-order arithmetic', and also of the distinction between standard and
non-standard models of first-order arithmetic.  Further, I know of no way
of giving explications of these concepts without using second-order logic
(or something which from Steve's point of view will be just as dubious).
Now maybe I'm wrong:  maybe this is illusory, and we don't really
understand the concept of arithmetical truth or 'standard' model.  But
since we seem to understand these notions, and since it seems that we can
only explicate them in terms of second-order notions, there's at least a
prima facie case that these notions are meaningful and essential for the
expression of certain things we want to express. Exactly what is Steve's
argument against this prima facie case?

> > ... for the realist, it's not just that you can prove in
> > first-order ZF that, say, second-order arithmetic is categorical,
> > but that it really *is* categorical ...
>
>This is a very odd remark, because for the realist, the fact that a
>statement X is provable in ZF *implies* (i.e., is stronger than) the
>fact that X is true, but not the other way around.

Dear Steve, try reading the second half of the sentence before replying to
the first half.  Of course for the realist provability in ZF brings truth,
because one of the models of ZF is the model the realist 'intends'.  The
point is that the *non*-realist can give a much weaker meaning to the claim
that second-order arithmetic is categorical, namely that each model of ZF
determines a unique model of arithmetic (though different models of ZF may
determine different models of arithmetic).

>It seems to me that the induction scheme in PA and the separation
>scheme of ZF are justified not by second-order logic but rather by
>naive (i.e., informal) considerations about sets and classes, followed
>by straightforward formalization of these naive considerations within
>the predicate calculus.
>
>One naively believes that any set of nonnegative integers has a least
>element, so one asserts this for all sets describable in the language
>{+,x,0,1,<,=} and this is the induction scheme of PA....  One naively
>believes that the intersection of any class with a set is a set, so one
>asserts this for all classes describable in the language {epsilon,=} and
>this is the separation scheme of ZF.

The most natural way to read this (perhaps not the only way) is to see
Steve as conceding my point, but insisting on replacing the word
'second-order' by 'naive (i.e. informal)'.  I read 'any set' and 'any
class' as the intended range of the second-order variables. Is Steve saying
that although we do use informal second-order logic to arrive at
first-order schemata, it's somehow naughty to formalize the second-order
logic we're using, in case someone might think that we're going to use it
as a model of inference rather than a source of axioms?

I agree with Steve that history doesn't matter: the question is not one of
how people originally thought about these things, but rather of how we
should think about them today.  But since Steve raises history, and claims
that in the original conception of PA and ZF 'second-order logic didn't
play a role.  Did it?', it's worth pointing out that history is all on my
side here.

The basic idea behind the induction axiom/schema first appears in part III
of Frege's 'Begriffschrift', and not only is it unambiguously expressed in
second-order logic - in parts I and II Frege had created second-order logic
precisely for the purpose!  The first statement of something like 'Peano's
axioms' is (independently of Frege) in Dedekind's 'Was sind und was sollen
die Zahlen?', in which the whole aim is to show that arithmetic is part of
'logic' (and where there is no hint of a division between first and
second-order logic, or logic and set theory, but rather the contrast is
between 'logic' and anything depending on Kantian intuition).  In the
letter to Keferstein Dedekind points out that Frege's construction 'agrees
in essence' with his own.  Peano's axiomatization in 'Arithmetices
principia' gives the induction axiom (Axiom 9) in terms of classes, where
'class' is assumed to be a logical notion.  Of course this is all at a time
when no-one made any distinction between first-order and second-order
logic, but it's obvious that it is what we now think of as the second-order
notions that were being used.

So far as set theory is concerned, Zermelo openly rejected Skolem's
interpretation of his axiom of separation (an interpretation which amounts
to the modern first-order schema).  In a footnote to 'Ueber Grenzzahlen und
Mengenbereiche' he insists that 'the propositional function f(x) [i.e. the
condition used to separate out a subset] can here be completely *arbitrary*
[Zermelo's emphasis]Š and from the point of view adopted here any
conclusions drawn from a restriction of it to a particular class of
functions do not apply'.  In other words, Zermelo said quite clearly that
separation was to be understood as a second-order axiom and not as a
first-order schema.

I am a bit astonished at the following passage from Steve's reply to John
Mayberry:

>I don't think non-r.e.ness of validities *on its own* precludes
>so-called `second-order logic' from being a logic.  For instance, the
>validities of `omega-logic' and `weak-second-order logic' are also
>non-r.e., but unlike so-called `second-order logic' these `logics'
>have at least some claim to being called logics, because they are
>defined by certain logical axioms and rules of inference (albeit
>infinitary ones).

I thought Steve's criterion for being logic was being 'a model of
reasoning' (his words). Now I may have a swollen head, but I don't have an
infinite mind.  So I can't use infinitary rules of inference - though I can
use finite first-order surrogates, just as I can use first-order schemata
in place of second-order axioms.  I really can't see the difference here.
Incidentally, I wonder what Steve thinks of first order logic enriched with
the quantifier 'there are uncountably many ...'.  Astonishingly, we still
have a completeness theorem.  (See the Barwise _Handbook_ pp. 44-5.)  Is
this still logic?

PS I'm signing off from this debate for a month, because for the next ten
days I'm too busy, and then for three weeks I'm out of e-mail contact.  But
whatever Boniface VIII may have said, silence doesn't mean agreement.

Robert

Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845
home tel. 0115-947 5468