FOM: ZFC orthodoxy/wider story

[Harvey Friedman]

Simpson writes 6:58PM 12/21/99:

>On the one hand, I speculate that the currently dominant, ZFC-style,
>set-theoretic-foundational orthodoxy may well fall into disrepute
>fairly soon.

I do not believe that it will fall into any kind of disrepute. What is more
likely to happen is that when the story of f.o.m. is told, it is told in a
way that makes it clear that there is much more going on than just the
formalization of mathematics in ZFC. Disrepute - no.

In fact, I believe that ZFC captures all information about sets that is
"simple", and this can be properly formalized and proved. In this sense,
ZFC is complete, and certainly not going to go away or fall into disrepute.

Of course, this leaves open the possibility that certain kinds of orthodoxy
might, however, fall into disrepute.

>This speculation is based on observation of recent
>directions in f.o.m. research.  On the one hand, recent
>set-theoretical research points to a need for large cardinal axioms
>going far beyond ZFC, in a somewhat unpcontrollable way.

I would put it differently. There is the expectation that large cardinal
axioms can be productively used in order to get new kinds of information
about standard objects of mathematics that cannot be obtained without them
- and this is just starting to happen to some extent.

Even if this happens, people will rightfully be interested in just when
large cardinals are needed, and just when ZFC is sufficient - partly
because of the preferred status of ZFC as capturing all of the "simple"
facts about sets.

 >On the other
>hand, recent research on subsystems of second-order arithmetic
>indicates that the bulk of current mathematical practice is
>formalizable in systems much weaker than ZFC.

That's part of

*the story of f.o.m.*

 that includes more than just the formalization of mathematics in ZFC.

>My feeling is that both
>of these research directions tend to put the ZFC orthodoxy into
>question, and this could result in widespread rejection of the ZFC
>orthodoxy within the next 100 years.

I wouldn't put it this way. The positive way to say this is that ZFC tells
only part of the story.

>On the other hand, I predict that our current 20th century idea of
>mathematical rigor, explicated in terms of formalization in
>first-order logic, a.k.a. the predicate calculus, will surely remain
>vital and of the essence in pure mathematics, for at least the next
>500 to 1000 years.  To me these ideas seem so compelling that I can
>see no viable alternative.

>In sum, my feeling is that mathematical rigor and the predicate
>calculus will endure much, much longer than ZFC set theory as an
>f.o.m. orthodoxy.

Well, I can already see that "predicate calculus" is also only part of the
story, too. It is only part of the f.o.m. model for reasoning story.

First of all, predicate calculus cannot even be used at all in the
formalization of reasoning without practical modifications. E.g.,
abbreviation power. And then it cannot really be used yet, because of it
being virtually impossible to support actual reading and writing. As you
know, I have continually said that this can be remedied - with hard work -
and I made some starts. And the ongoing Mizar project is relevant.

So both predicate calculus and ZFC are only part of the f.o.m. story. You,
like Buss, wish to draw some sharp distinctions between the two of these.

Well, I think that is hard to do this in a really convincing way.

But I would like to have the luxury of not trying to make such sharp
distinctions, and instead say that both of them are only part of a more
sophisticated story - the story of f.o.m.