Date: Mon, 22 Mar 1999 16:45:50 -0700
From: Randall Holmes <holmes@catseye.idbsu.edu>
Subject: FOM: sterility?

I hardly think that it is a sterile concern for the foundations of
mathematics whether we can actually refer to such familiar structures
as "the natural numbers".  Second-order logic allows us to do this,
because it allows a categorical axiomatization of N and other familiar
structures; first order logic, even formalization in a first-order
theory as strong as ZFC, does not.

I am not saying that ZFC does not allow us to prove many theorems
about the natural numbers; it certainly does.  But first-order ZFC, if
consistent, has models in which the purported "natural numbers" are
clearly not the actual natural numbers (by which I mean that they do
not have the correct structure).  I assume that this fact is not in
dispute between Simpson and myself (or between other proponents of our
respective viewpoints).  The fact that theorems provable in ZFC about
"the natural numbers" as conventionally represented in ZFC are true
theorems about the natural numbers follows from our understanding of
what the natural numbers are; but it cannot be fully justified in ZFC,
or in first-order terms at all.

"What we can say" is a philosophical concern necessarily prior to
"what we can prove".  If I asked a philosopher what branch of
philosophy this question belonged to, I think the answer might be
... logic.  (Are any philosophers out there willing to address this
question?).  Formal logics for the purpose of expression or definition
may annoy Simpson, but I think they make perfectly good sense (we will
not be able to get a complete formal logic of expression: truth in a
language L will not in general be definable in L, as is well-known,
and will certainly not be definable if L extends second-order logic).
A formal logic of expression/definition which is capable of describing
the natural numbers precisely will be able to describe the notion of
provability in a formal system precisely, and so will not support a
complete notion of proof (but will support partial formalizations
usable for proof).


There are mathematicians on this list who believe that we cannot
successfully refer to the standard model of the natural numbers (or
other familiar mathematical structures).  If their belief is true, it
is a fact of general intellectual interest, and a fact within the
purview of the foundations of mathematics.  I don't think it is true.
I don't think that we can formalize notions that we cannot even
express.  If we can (partially) formalize talk of the natural numbers,
then we can talk informally about the natural numbers.  If we can talk
informally about the natural numbers, then the question arises as to
how this is possible (how can we refer to this structure?).  (One
possible answer is that we have partially formalized an informal
notion which is actually incoherent; but I see no reason to believe
that this is the case, and if it were the case I see no reason to
expect that the formalization would be useful or interesting).

A formalization in ZFC does not achieve this aim; it allows us to
prove many theorems about the natural numbers, and perhaps all the
theorems that we will ever want to prove in practice, but its model
theory makes it clear that it cannot be taken as explaining what we
_mean_ by "the natural numbers".  

The standard formalization in second-order logic captures precisely
what many of us think we mean by the natural numbers and is the form
in which the theory of the natural numbers was originally formalized
in the last century; one may note correctly that it does not allow one
to prove any theorems about the natural numbers that cannot be proved
about the natural numbers as conventionally represented in ZFC, but
that is beside the point.

A formalization in second-order ZFC does capture precisely what we
mean by the natural numbers (up to isomorphism as usual), and the
proof techniques of first-order ZFC are valid (but partial) techniques
for reasoning about the objects of second-order ZFC. So one may carry
out reasoning which looks like formal reasoning in first-order ZFC
from a stance in which one can claim to have a correct formalization
of what the natural numbers and other familiar structures "are" (with
incomplete techniques of proof).

I reiterate the point that second-order logic does not have any more
set-theoretical prerequisites than first-order logic.  Second-order
quantifiers may be understood to range over _properties_.  "Property"
is not a specifically mathematical notion (it is inarguably
topic-neutral and arguably "logical").  So objections to second-order
logic thus presented cannot be based on claims that second-order logic
is set theory in disguise.  I am given to understand (from
conversation on this list as well as earlier reading) that Zermelo
proposed the axiom of separation in terms of properties and objected
to the later formalization in terms of formulas of first-order logic.

These are not "sterile" considerations.  No one is going to prove new
theorems about the natural numbers based on these considerations (or
at least, I would just as surprised as Simpson if this happened!), but
there are important issues here which bear on the foundations of the
subject.

An aside: a place where the issue of what it is that we are talking
about cannot be honestly avoided is in the teaching of mathematics.  I
think that my students in mathematics classes have some right to
expect that we are talking about some definite subject matter.  The
ones who think we are playing a formalized game which is not really
about anything in particular are generally not the best students.

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@math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes