FOM: formalization, first order, ZFC

[Harvey Friedman]

Holmes 1:24PM 3/23/99 writes:

>What I'm saying is that mathematics is not _completely_ formalized by
>ZFC.  You admit this yourself later.

A number of postings by Holmes and others makes this point, but I think it
is somewhat misleading.

There is no question that no mathematics Journal would intentionally accept
an article with a purported proof of a Theorem which was not
straightforwardly formalizable in ZFC just from an understanding of the
proof as written.

So in that sense, ZFC serves as a complete formalization of mathematics.

However, Con(ZFC) is not provable in ZFC, but the same people who are very
comfortable with ZFC as a foundation of mathematics are also very
comfortable with Con(ZFC). So it would seem that ZFC does not serve as a
complete formalization of mathematics.

The error is to regard Con(ZFC) as part of mathematics. It is part of
mathematical thought, but not mathematics itself. It is perhaps part of
reflective mathematics. But this is not the same as real mathematics.

The Journals implicitly agree. Con(ZFC) has to be mentioned as an explicit
hypothesis if it is used in a proof. But no axiom of ZFC has to be
mentioned as an explicit hypothesis if it is used in a proof.

Of course, Journal editors, referees, authors, etcetera all act on this at
a semiformal level. But they know that there is a theory behind this that
they don't want to study; they don't need to study in order to act
appropriately.

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

Bad idea.

>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)

I was going to mention the Mizar project - which I mentioned much earlier
on the FOM, but Simpson beat me to the punch. There are such important
issues raised by
(projects like) Mizar that I want to make this the subject of a separate
posting.

Basically, the Mizar project **suggests** (not proves!) that formalization
can actually be carried out by human beings with the help of computers for
all of published mathematics, and gives us some idea of how long this would
take.

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

As I said before, you are wrong under the normal use of the terms
"adequate" and "definition." You particularly sense of this is wholly
inappropriate.

>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 false in the sense that ZFC serves as the accepted complete
formalization for mathematics. As I said above, one must distinguish
between other mathematical activities such as reflective mathematics, or
mathematical thought, or various metamathematical activities.

Of course, one day there might be such striking developments on various
fronts that some extensions of ZFC may be the accepted complete
formalization for mathematics. But that is another story for another day.

> A serious discussion of such philosophical
>issues in f.o.m. is what I would really like to hear.

What philosophical issues do you want discussed on the FOM?

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

ZFC is the accepted complete formalization of mathematics. But not the
accepted complete formalization of all mathematical activities.

>It is seriously flawed, _if
>considered as a foundation all by itself_ (in my opinion).

I don't see why.
>
>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.

And that is what is to be emphasized. Not the irrelevant side issue that
you keep raising.

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

True. But it is irrelevant to the discussion of ZFC as a formalization of
mathematics.

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

Even I know this as well as most people. But it is a technical side issue
in this thread about f.o.m.

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

Informal set theory does this just fine. The first order language of set
theory does this just fine.

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

The first order language of set theory is preferable for this purpose.


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

The first sentence does not make any sense to me. This is because the
language of first order and second order logic are different.

>I [Holmes] 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.

I disagree. A formal first order theory - set up for the purposes of f.o.m.
- is a model (in the sense of, e.g., "modelling physical phenomena") of
mathematical practice. The models (in the sense of model theory) that it
has is a comparatively technical side issue that often needs to be
considered in order to obtain important information about what can be
proved in the system and related issues.

>Formal first order group theory is about
>all groups, i.e., all those structures that satisfy the familiar axioms
>of group theory;

OK.

>formal first order Zermelo-Fraenkel set theory is
>about all those structures that satisfy the axioms of ZFC.

Absolutely not!!

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

Defensible pedantic point that is hard to argue or agree with.

>Since it is a
>formal, first order theory it has all sorts of interpretations that are
>radically different from its intended interpretation.

This is a technical side issue that must be constantly kept in mind by all
workers in f.o.m. in order to avoid all kinds of false proofs and technical
pitfalls.

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

Fine. Of course you can't identify set theory with ZFC since set theory is
an area of mathematics and ZFC is a formal system.

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

A pedantic point that may cross the line into indefensibility. Imagine
doing set theory without any clear idea as to what principles of set
construction are being allowed. You just make it up as you go. You may want
to call this a "foundation for mathematics" but it is grossly unsatisfying
and is solved by writing down ZFC - well before you get to issues as to
what you can prove in ZFC.