FOM: "cannot be formalized at all"

[Randall Holmes]

At some point I said that a case could be made for a proposition of
the form

"arithmetic cannot be formalized at all"

By this I meant, as I have said repeatedly, that mathematics
(even arithmetic) cannot be completely captured by any formal
system.  This is a well-known fact.  What I actually meant can
readily be determined from the context in which it was written.

There was some perhaps ill-advised attempt on my part to be
deliberately provocative in the way it was phrased.  This is a
rhetorical maneuver of which Simpson himself is far from innocent.

Comments of the kind Simpson just made are especially annoying since I
have already said this _at length_.

Give it a rest.

Re recent posting by Friedman:

Friedman said:

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.

Holmes replies:

I may perfectly well believe that Con(ZFC) is true as a mathematical
assertion (in fact, I do).  For example, I may use Kelley-Morse set
theory as my background set theory (as some still do, I think), in
which case Con(ZFC) is a theorem.  The case for Kelley-Morse is quite
good; it is very similar to the informal case for ZFC.  If I do
believe Con(ZFC) as a mathematical statement, and use it, then I do
owe my readers the courtesy of telling them that I am using this
hypothesis, since it is not a universally accepted assumption.  But
this does not put it outside of mathematics.

Friedman said:

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.

Holmes comments: This is not always true, surely.  I think there may
very well be contexts in which implicit use of an axiom of ZFC (I have
Replacement in mind) would be illicit because ZFC is itself of very
high consistency strength.  And many mathematicians do make a point of
alluding to uses of Choice.

Friedman said:

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.

Holmes comments:

I have alluded to this.  I think the evidence that formalization can
actually be carried out is quite strong.

Friedman said:

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

Holmes comments:

The sense of the terms which I am using is  appropriate to the 
topic which I am actually discussing, which falls under the
category of "reflection on mathematics" which you allude to below.

Friedman said:

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

Holmes comments:

and of course I am engaged in reflection on mathematics, as is
fairly obvious from the context.

[...]

Friedman said:

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

The ones I have been discussing!

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