FOM: second-order logic is a myth

[Randall Holmes]

Black and Simpson had the following exchange:

 > second-order logic is an essential tool for the *expression* of
 > mathematical theories.  It can do this, and first-order logic
 > can't, ...

That statement is indeed very odd, if not absurd, because it overlooks
the fact that mathematics is formalizable in ZFC.

I comment:

I find it hard to believe that Simpson doesn't understand what Black
means here.  It is possible to formalize mathematics in ZFC in one
sense, and not possible in another sense.  It is possible to prove
many facts that we believe about the mathematical world by using
familiar representations of this world in ZFC.  But it is not possible
to prove certain other facts that we do believe in this language: for
example, it is not possible to prove Con(ZFC), which can be understood
as a fact about the natural numbers.

The axioms of ZFC describe a class of structures (models of ZFC) which
include the intended interpretation(s) (whatever precisely it (they)
may be) but also include structures which are clearly not the intended
interpretation: a model of ZFC whose natural numbers do not satisfy
Con(ZFC) is certainly not what we are after!  Thus ZFC does not
completely formalize mathematics (in fact, no formal system can) in
one sense.

Since we do recognize that some interpretations capture the intended
interpretation and some do not, there is an informal understanding of
what is wanted which is prior to the formalization in ZFC.
Second-order logic is a useful working language for this informal
level (which we cannot really completely replace by a completely
formalized system!)

Another exchange between Simpson and Black (Black is indented by
Simpson, elisions are represented by [...] and my inserted remarks are
labelled).:

Black:
 > [I] see Steve as conceding my point, but insisting on replacing the
 > word 'second-order' by 'naive (i.e. informal)'.

Simpson:
That is not what I intended.  I said and meant `naive
(i.e. informal)', not `second-order'.  There is a big difference
between `naive (i.e. informal)' and `second-order'.

I comment:  I see this the same way Black does.

Black:
 > I read [Steve's] 'any set' and 'any class' as the intended range of
 > the second-order variables.

Simpson:
That is not what I intended.  Informal reasoning about sets and
classes is a very different thing from second-order logic.  In the
first place, second-order logic is formal, not informal.  In the
second place, when we reason informally about sets and classes in a
mathematical context, we are viewing them as just another kind of
mathematical object.  They are topic-specific and not part of any
underlying logic.

I comment: second order logic _is_ informal; I grant (and I understand
Black as granting) that it is not a formal system.

Simpson (continued):

Let me try again to give you my view of how PA and ZF are motivated.

In the case of PA, the induction scheme is motivated by an informal
picture involving sets: the least element principle for arbitrary
subsets of N.  Despite this, the axioms of PA don't mention sets.
They can't, because sets aren't in the language of PA.  However, the
axioms of PA capture the idea of the least element principle for all
sets describable in the language of PA.  Thus sets play a role in
motivating PA but they are absent from the final formulation.
Similarly, in the case of ZF, the separation and replacement schemes
are motivated by an informal picture involving classes.  The axioms of
ZF don't mention classes.  They can't, because classes aren't in the
language of ZF.  However, the axioms of ZF capture the idea of
separation and replacement for all classes describable in the language
of ZF.  Thus classes play a role in motivating ZF but they are absent
from the final formulation.

Note that second-order logic (neither formal nor informal) plays no
role in the above description of how PA and ZF are motivated.

I comment: I agree with everything Simpson says about motivation here,
except that one can be even less "mathematical" and replace set or
class by "property" throughout.  Second order logic is clearly present
if one quantifies over predicates/properties -- that is what
second-order logic is about.

Black continues:

 > Frege had created second-order logic precisely for the purpose!

Simpson:
Wait a minute.  You say that Frege's system includes second-order
logic.  I recently had occasion to reread the Begriffschrift, and I
agree with you in a sense.  But let's be precise here.  Following
Shapiro, we need to ask, is Frege's system a species of `second-order
logic with standard semantics', or is it a species of `second-order
logic with Henkin semantics'?  I think it's more like the latter,
because Frege presents axioms and rules of inference, and the axioms
and rules that Frege presents are somewhat similar to the Henkin
axioms and rules.  In other words, according to the modern
understanding of this, Frege's system is really a first-order system!

Also, it's worth mentioning that Frege's system turned out to be
inconsistent.

I comment: The inconsistency in Frege's system is irrelevant.  It was
caused by the actual "set theory" in Frege (the correlations provided
between "second-order objects" and "first-order objects").

Frege's system would only be a species of `second-order logic with
Henkin semantics' if Frege claimed that the given rules of inference
were complete.  Did he?  Even if he did, this claim could be abandoned.

The fact that second-order logic is not completely formalizable does
not mean that partial formalizations cannot be presented and used
without abandoning the second-order viewpoint.

Black continues:
 > 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.

Simpson:
That is not so obvious to me.  There are difficulties of
interpretation, and the early history can be read so as to support
varying points of view.

I think it's fair to say that 1890's ideas about sets and classes are
very different from our current ones.  Then, people tended to view
sets and classes as logical notions.  Now, as a result of progress and
clarification in axiomatic set theory, we have a more sophisticated
view.  We now treat sets and classes as simply another kind of
mathematical object.  This is reflected in the distinction that we
make between the logical axioms and rules of ZF and the set-theoretic
(`non-logical') axioms of ZF.

I comment: I think that it is correct to say that many do take this
view that "sets and classes as simply another kind of mathematical
object" in practice.  It may turn out that they are wrong to abandon
the previous attitude.  

I think the correct view is that there is a specifically mathematical
notion of "set", which only comes into view when sets are considered
as elements of other sets, something which does not happen in
second-order logic (and does happen in third and higher-order logics,
which I regard as eliminable in favor of second order logic).  The
notion of "proper class" (set or class which cannot be considered in
its turn as an element) corresponds to the notion of "property" which
I think is really at issue in second-order logic, and which is not
a specifically mathematical notion at all.
 
[...]

Simpson:

The minute you write down rules for second-order logic, you are in the
realm of first-order logic (`Henkin semantics').  That's why I say
that second-order logic is a myth -- it isn't really logic, or to put
the point another way, to the extent that it *is* logic, it's
first-order logic.

Holmes concludes:  if logic means "formal system of inference" then this
statement is correct.  But I have elsewhere discussed reasons why I believe
that this definition is too limited.

Again, writing down formal rules does not mean that one abandons
second order logic unless one claims further that the formal rules
completely define one's logic.

By the way, the definition of "logic" in the OED is too vague to be useful
to either myself or Simpson.

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes