FOM: serious disagreement?

[Harvey Friedman]

Despite a lengthy interchange with Holmes, I still cannot tell whether or
not there are any substantive issues worthy of continued discussion! I
believe that Holmes thinks that certain facts and definitions are important
that I don't. And Holmes may think that NFU plays a significant role in
f.o.m. I don't. It might in the future, but so might a large number of
things.

Perhaps a more interesting disagreement might be that he does not
acknowledge the very important sense in which ZFC is currently accepted as
the complete formalization of mathematics. He keeps emphasizing various
pedestrian senses in which it is not. This seems counterproductive,
backward looking, and totally uninteresting.

Of course, I am engaged in a long term project which may ultimately change
the status of ZFC as the currently accepted complete formalization of
mathematics. This in a much deeper sense than Holmes remark that "we
believe in Con(ZFC), which is not provable in ZFC". But we are not there
yet.

Holmes 8:31PM 3/24/99 writes:

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

Many formal languages are created after there is a developed subject
matter. In the case of set theory, the first order language of set theory
evolved after considerable development of the subject matter of set theory.
It is understood that the semantics of the first order language of set
theory is immediately derivative of the subject matter of set theory.
Namely, for all x means for all sets x, and there exists x means there
exists a set x. Consequently, there is an obvious definition in the
language of set theory of "being a natural number system" with,
demonstrably within set theory, the requisite properties required, as in
ordinary mathematics. Don't confuse this with second order logic.

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

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

No. The Annals of Math would accept any well exposited proof of a Theorem
using Replacement. The fact that mathematicians sometimes make a point of
alluding to uses of Choice is irrelevant to this discussion. Certainly the
Annals of Math does not require that uses of the Axiom of Choice be
explicitly mentioned.