FOM: second order logic, reference of mathematical language

[Randall Holmes]

I suggest that one of the difficulties in the second-order logic
thread is that the participants are talking past each other.  It would
be nice to get out of this state and figure out what the real concerns
underlying this dispute are.

Thesis 1: I think that the issues here have nothing to do with the
actual practice of mathematics.  I agree with Simpson and Friedman
that the way to do our business is to work in a formalization which
looks like first-order ZFC, using definitions which can be phrased in
the language of first-order ZFC, and prove theorems from that as a
starting point (I don't see any reason to think that any others who
might agree with me would think differently).  Under some
circumstances, it is necessary to move to a stronger formal theory;
there is a natural (though not formalizable) way of getting stronger
and stronger extensions of ZFC in which we have confidence.

The questions are in the area of f.o.m., not of mathematics.

Thesis 2: The questions have to do with the motivation of definitions
of mathematical concepts.  One side of the debate sees a problem with
them which the other does not.  The problem is perhaps philosophical
rather than genuinely mathematical (but nonetheless falls within the
scope of f.o.m.)

Mayberry and I both hold the view that the first-order theory ZFC is
the theory of the class of models of ZFC (just as group theory is the
theory of structures which satisfy the group axioms).  On this basis,
first-order ZFC cannot express the notion "the set of natural
numbers", because there is no term in the language of ZFC which will
always define the set of natural numbers.

On the other hand, in any model of second-order ZFC (this is a far
stronger theory than is needed!) the usual definition of "the set of
natural numbers" will refer to an implementation of the set of natural
numbers.

Thus I would say that second-order ZFC allows us to express the notion
"the set of natural numbers" and first-order ZFC does not.  This usage
of the word "express" may be eccentric, but I should now have made it
clear what I mean by it.

The effect of this on mathematical practice is nil, for the following
reasons (already belaboured in this thread): we can't do anything in
second-order ZFC without adopting a partial formalization (a complete
formalization is impossible).  The formalized theory will include
first-order ZFC (actually, the natural formalization will give the
slightly stronger Kelley-Morse set theory).  I don't think Simpson or
Friedman would regard an insistence on working in Kelley-Morse set
theory as more than a mild eccentricity!  In any event, the
formalization will be a first-order theory fitting in the hierarchy of
natural extensions of ZFC.

In this framework, it is natural to study models of first-order ZFC
(or of Kelley-Morse set theory) both for their own intrinsic interest
and because this study allows one to look at alternative possible
situations which might hold in the ambient second-order ZFC.  So the
practice of studying consistency and independence results makes
perfect sense from the "second-order ZFC" standpoint; the only
difference is one of philosophical perspective.  No change in the
actual mathematics being pursued is to be expected!  I suppose that it
is possible that the mathematician with the second-order standpoint
might become convinced through his study of consistency and
independence results that he ought to adopt some additional axioms in
his second-order theory -- but a mathematician taking a different
approach might adopt additional axioms for reasons which would look
much the same on the surface!

The advantages of such an approach (if any) cannot lie in the actual
mathematics being done, because the mathematics being done (even re
consistency and independence results) will be the same.

The point for me is that the approach via second-order logic (be it
logic or not -- that's another terminological argument) allows the
exact definition of basic mathematical concepts in topic-neutral terms
(something like the logicist program).  This is a philosophical issue
(but one proper to f.o.m.); it may be disputed whether it is possible
or desirable, and I would be interested in discussing its value or
lack thereof.  There is no claim (on my part at least) that there
should be any fundamental change in mathematical practice.

Note that the argument about the mathematical or topic-neutral
character of second-order logic is relevant here.  I have already said
something about this: second-order quantifiers can be taken to range
over predicates or properties rather than the specifically
mathematical "sets".  Of course, the legitimacy of this proceeding is
open to debate.

The question of what the natural numbers (for example) are, or what we
mean when we talk about the natural numbers (or other mathematical
structures) is certainly a legitimate topic for f.o.m. (though not
necessarily of great interest to a working mathematician).
Incidentally, questions like this should also be important in
mathematical pedagogy.

(An interesting incidental side effect of an approach using
second-order logic is that it makes the claim of ZFC to be the proper
foundation (as opposed to alternatives like Ackermann set theory or
NFU) much stronger.  The comprehension axioms of ZFC have elegant
second-order analogues, while the comprehension axioms of Ackermann
set theory or NFU are much harder to motivate in second-order terms;
there is a nice second-order version of NFU which I have studied, but
it is extremely strong!  This isn't directly relevant, but there have
been side comments on my fondness for NFU.  As a first-order
formalism, NFU is really not bad at all; I'm doing theorem proving
work using stratified lambda-calculus (theory of functions rather than
sets) and it appears to be quite convenient to use this as a
"higher-order logic" (it is not a true higher-order logic)).

So I would like to hear from other parties.  How do we define "the set
of natural numbers" in ZFC (this is not a request for the text of the
definition!), and what is the relation of this definition to our
pre-formal notions?  I do not understand the legitimacy of a
definition in a formal language prior to the adoption of axioms or
rules of inference -- or at least for the sake of this argument I
don't.  The only way I can understand this proceeding involves the
implicit interpretation of the primitives of first-order ZFC as having
the meanings which they have in second-order ZFC.  But I'm not going
to presuppose that this is what is happening in the heads of other
mathematicians.

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