FOM: ZFC, NF(U), foundations

[Harvey Friedman]

Holmes writes 3:27PM 3/25/99:

>A subtle point is that I think there is a fairly good argument that
>the comprehension criterion for NF(U) is a better resolution of the set
>theoretical paradoxes than the comprehension criterion of ZFC --

Absurd.

>but I
>don't think that the foundations of mathematics really depend in any
>essential way on a confrontation with the set theoretical paradoxes
>(the paradoxes were avoidable mistakes).

Bizarre.

If the set theoretical paradoxes are not confronted appropriately then we
do not have legitimate foundations of mathematics. There may be various
ways to confront them. E.g., one can propose V(omega+omega) as a picture of
the mathematical universe.
>
>Friedman writes:
>
>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.
>
>Holmes writes:
>
>I do not deny that ZFC is the favorite formalization of mathematics.
>Fellow NF-istes chide me for referring to it as "the usual set
>theory".  But I think that Friedman is making a stronger claim than is
>warranted.
>
>A predicate like "backward-looking" is generally applied to evil
>reactionary forces opposed to the right-thinking "progressive"
>elements; in what direction does Friedman think we should be making
>progress (he might find that I agree with him :-))?

Implicit in what I said is that it is more progressive to consider in what
sense ZFC and various of its fragments are formalizations for all and parts
of mathematics as conceived of and practiced by mathematicians when they do
what they normally do when they say they are doing mathematics. This is
more productive than the hackneyed answer that no formal system will do,
they are all artificial fragments, etc., with the usual Con(T) argument.
This hackneyed answer is best put in perspective by making distinctions
such as the one I was making between, say, mathematics and mathematical
thought. A careful consideration of such issues leads to a mapping out of
significant fragments of ZFC, and the creation of reverse mathematics. But
only the surface has been scratched.

>Friedman writes:
>
>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 writes:
>
>I considered citing this against you.  Results of the kind you are
>aiming for are much better examples than Con(ZFC).  The mere
>possibility of such a project militates against your apparent views.

Note the word ****currently****. I am consistent, although maybe I can't
prove that (smile).

>Harvey Friedman writes:
>>...
>>But I am confident that you will join me and many others on the FOM list in
>>enthusiastically celebrating this recognition of Turing and Godel!!
>
>Holme writes:
>
>I will applaud, even if the recognition is for the wrong reasons :-)

Good.