FOM: denunciation of formalized mathematics?

[Randall Holmes]

Simpson said:

Randall Holmes 18 Mar 1999 16:00:03 disputes the well known fact 

  (*): mathematics can be formalized in formal systems based on
  first-order logic such as ZFC.

I find this position remarkable.  The well known fact (*), which
Holmes disputes, is of course well known to be crucial for current
f.o.m. research.  I know of no scientific reason why Holmes would want
to undercut (*), especially since Holmes himself has credentials as an
f.o.m. researcher.

Holmes replies:

I find the whole tenor of your response(s) remarkable.  When you find
your interpretation of what your respondent in a debate is saying
_too_ remarkable, it might be profitable to check your premises (as to
what your "opponent" means); some of them may be wrong.

What I'm saying is that mathematics is not _completely_ formalized by
ZFC.  You admit this yourself later.  I am certainly not an opponent
of formalized mathematics.  A large part of my work is in computer
assisted theorem proving, which would be a really remarkable pursuit
if I did not value formalized mathematics!!!

The context is:

(earlier message from Holmes)
In this note, I discuss Simpson's claim that

"mathematics can be formalized in ZFC"

This is a very common claim; I often make it myself (more often I
claim that mathematics can be formalized in strong extensions of NFU,
a claim to which the same strictures apply that I apply below to the
commoner claim about ZFC).  It is true in a certain practical sense.
But I think that there are also good grounds (which most of us know
about, though I will tiresomely summarize them below) for the contrary
claim that

"arithmetic (and so most of mathematics) cannot be formalized at all".
(end of earlier message from Holmes)

A complete reading of the message would make it clear that I am not
issuing a blanket denunciation of formalized mathematics.  Even a
reading of the excerpt should suggest this.  The specific, and
well-known point which I make in the rest of the excerpted post is
that first-order ZFC (or any first-order theory) (in a sense which I
discuss further below) is not adequate for the definition of the
natural numbers (in a precise sense which I make clear below, and made
clear in that post).  This is an uncontroversial mathematical fact.  I
also make the philosophical point, with which one may agree or
disagree, that the informal standpoint from which one starts to
understand mathematics is never completely captured or replaced by any
formal system; this is not a denial that formalizations of mathematics
are important and useful.  A serious discussion of such philosophical
issues in f.o.m. is what I would really like to hear.

Simpson said:

In his subsequent posting of 18 Mar 1999 16:25:52, Holmes backs down a
little bit:

 > I must hasten to add that ... first-order logic does capture a
 > (nearly) universal standard of formalized proof.

Holmes replies: I wasn't "backing down" at all.  This is an essential
part of my position.  You seem to think that because I recognize the
importance of second-order logic for definition I do not recognize the
crucial importance of first-order logic for inference and cannot avail
myself of first-order tools.

I exhibit this remark of Simpson:

However, he doesn't back down from his denunciation of formalized
mathematics.

I respond, for the record:

I did not issue a denunciation of formalized mathematics.  If anyone
other than Simpson thinks that I was denouncing formalized mathematics,
please tell me; such was far from my intention.

Simpson asserted:

When well known facts are in dispute, somebody needs to stand up and
be counted.  I want to put on record that I disagree with Holmes and
reject his rejection of the idea of formalized mathematics.

Holmes comments:

I want to put it on the record (as I have already) that I do not
reject the idea of formalized mathematics.  I do reject the idea that
first-order ZFC, all by itself, constitutes a complete formalization
of the fundamentals we need for f.o.m.  It is seriously flawed, _if
considered as a foundation all by itself_ (in my opinion).  Arguments
could be given against the position that these flaws are flaws at all,
or against the position that these flaws, if they are flaws, are
avoidable or worth avoiding.  Simpson has not attempted this; he
simply continues to misunderstand me.  The reasons why Simpson
steadfastly refuses to understand my argument, in which I use
well-known facts, just as he does, are a complete mystery to me,
especially as this argument is not especially novel.

For the record: if one's entire aim is to prove theorems whose usual
interpretation captures (almost all of) classical mathematics, then
first order ZFC is completely adequate as a foundation of mathematics.
This is not disputed by me, and I think that Simpson wants to defend
(without ever quite saying it) the position that this is all that
matters.  It is not, in my opinion, all that matters for
philosophically adequate foundations of mathematics.  I can imagine
philosophical viewpoints from which my additional concerns would not
be significant; such positions have been clearly stated by others on
this list.  Simpson has not clearly stated such a position.

Simpson said:

The truth is that there is an extremely important sense in which ZFC
*does* allow us to refer to the natural numbers and other familiar
structures and *does* contain a categorical axiomatization of those
structures.  Namely, the isomorphism types of these structures are
straightforwardly definable in ZFC.

Holmes says:

This is the crux of the matter.  I claim that there is a perfectly
precise (and well-known) sense in which the isomorphism type of the
natural numbers (to take the simplest case) is NOT definable in ZFC
(or any first-order theory).  If ZFC is consistent, it has models in
which the isomorphism type of the "natural numbers" (as usually
defined in ZFC) in the model is not the same as the order type of the
standard model of the natural numbers.  You know that as well as I do.
I find it very hard to interpret this quote as anything but a
_deliberate_ misunderstanding of what I am saying.

I also understand perfectly well that if I agree to understand the
usual definition of N in ZFC as referring to the natural numbers, and
the elements of P(N) as usually defined in ZFC as referring to the
natural numbers, I will be able to use the machinery of ZFC to prove
many correct theorems of second-order arithmetic; in fact, a lot more
theorems of second-order arithmetic than I can prove in the
first-order two-sorted theory usually called "second-order
arithmetic".  If you have read what I have written, I think that you
once again know perfectly well that I understand this.

In second-order ZFC, the definitions you refer to are correct.  I
suspect that your claim that first-order ZFC is an adequate foundation
is based on an equivocation between first-order and second-order ZFC.

My formulation is _not_ misleading (though it may require careful
reading of the context to understand it), and I have worked very hard
to make it clear exactly what I am talking about.

Simpson says:

 > "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.

So what?  Regardless of what a hypothetical philosopher might say,
logic is still the science of correct inference.  Second-order logic
is not logic in this sense, because it lacks rules of inference.  Why
deny this obvious point?

Holmes replies:

We have already looked at dictionary definitions.  Logic (as a branch
of philosophy) is not invariably defined as being _only_ the science
of correct inference, though it is always defined so as to include
that.  A traditional part of the science of logic is the principles of
correct (and adequate) _definition_.  The advantages of second-order
logic in defining well-known, basic mathematical structures are
well-known; the inadequacy of first-order logic for this purpose is
also well-known. The absence of complete (though _not_ of sound)
systems of inference for second-order logic is also well-known, and
have been granted by myself and others.  The adequacy of ZFC as a
foundation for mathematics if one's only concern is inference has been
explicitly granted by me.

Simpson said:

(replying to Holmes:)
 > Formal logics for the purpose of expression or definition may annoy
 > Simpson

Not at all.  Where did you get that idea?

Holmes replies:

You repeatedly assert that logic is exhaustively defined as the
science of correct inference.  My position that second-order logic is
an indispensible part of logic has to do with its function as a
(formal!!!)  language for formulating adequate definitions of basic
mathematical concepts.

Thus Simpson (replying to Holmes):

 > one may note correctly that [second-order logic] does not allow one
 > to prove any theorems about the natural numbers that cannot be
 > proved ... in ZFC,

Actually, second-order logic does not allow one to prove anything at
all, because it has no rules of inference.

Holmes replies:

The deductive principles of first-order logic are sound, though not
complete, for second-order logic.  I've made this point repeatedly,
and so have you (though not with the same intention).  They are
certainly available for anyone taking a second-order approach.

Simpson said:

No, it's not beside the point.  It goes directly to my point that any
proposed approach to f.o.m. via second-order logic is useless and
sterile.  

All of the most important f.o.m. advances (G"odel's incompleteness
theorem, the work of G"odel and Cohen on the continuum hypothesis, etc
etc, not to mention reverse mathematics, etc) are concerned with
inference and therefore require a first-order approach and could not
have happened under a second-order approach.

Holmes says:

We are perfectly free to use all the first-order machinery we want
(including the rules for second-order quantifiers analogous to those
for first-order quantifiers) while taking a second-order approach.  We
can also talk about models of first-order ZFC, including nonstandard
ones, to our hearts' content.  I can't imagine that you don't
understand that.

Simpson said:

A comment for Holmes: I am beginning to think that your remarks may
indicate some fundamental misunderstanding or off-beat assumption
about current research in f.o.m.  But I am having a hard time placing
my finger on exactly where you are going wrong.  Tell me, is your
advocacy of second-order logic somehow bound up with your advocacy of
NF?  NF strikes most people as a rather off-beat and unintuitive kind
of set theory ....

Holmes replies:

This has nothing to do with NF.  NF is a first-order theory.  I
sometimes put in a good word for strong extensions of NFU (not NF
itself) as alternative foundations for mathematics, but such
extensions are readily intertranslatable with strong extensions of
ZFC.  Suitable extensions of NFU have some formal advantages and some
formal disadvantages compared with ZFC; I think that ZFC has a better
intuitive justification overall, but I think that the fact that there
are alternative approaches is worth keeping in mind.  NFU has a less
satisfactory second-order metatheory (or at least a more complicated
one) than ZFC, because there are small (countable!)  proper classes in
any model of NFU.

I think that you either have or (I am really beginning to fear) feign
a fundamental misunderstanding of what I have been saying in this
entire thread.  It is very discouraging to be treated in this way.  I
would like to see evidence that this is not what is actually
happening.  

Some of the disagreement between us _may_ hinge on my using
terminology in odd ways; however, I have repeatedly explained myself,
with references to well-known results, to the point where it ought to
be perfectly clear what I actually mean.  In particular, I have not
denounced formalized mathematics.

I quote from a posting of Mayberry's with which I agree:

Strictly speaking - and we ought to speak 
strictly here - a formal 1st order theory is the theory of the class of 
structures that satisfy it. Formal first order group theory is about 
all groups, i.e., all those structures that satisfy the familiar axioms 
of group theory; formal first order Zermelo-Fraenkel set theory is 
about all those structures that satisfy the axioms of ZFC.
 	Simpson is muddled here. ZFC does not provide the foundation 
for mathematics. *Set theory* provides the foundation for mathematics, 
and ZFC is a first order formalisation of set theory. Since it is a 
formal, first order theory it has all sorts of interpretations that are 
radically different from its intended interpretation. That means that 
we cannot simply *identify* set theory with ZFC as a formal 1st order 
theory. But, as everybody knows, some of those non-intended 
interpretations have important uses.
 	What makes the formal theory ZFC so important for foundations 
is the fact that any proof in ordinary mathematics has a formal 
counterpart in ZFC. (Naturally, this is not a mathematically exact 
claim, since "ordinary mathematics" is not an exact concept.). It is 
this fact that gives significance to theorems to the effect that such 
and such a formal proposition (e.g., the formal sentence corresponding 
to CH) is not among the formal theorems of ZFC. The point of setting up 
that formal theory is NOT to provide a foundation for mathematics - set 
theory performs that task. The point is rather to provide us with the 
means for applying rigorous mathematical reasoning to questions about 
what we can prove.

(end Mayberry quote)

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