FOM: Question grown from Friedman talks

[Harvey Friedman]

McLarty Thu, 01 Feb 2001 21:19:53 writes:

>	I have heard two talks by Harvey Friedman lately, and talked with
>him at
>both, and they got me thinking of various things. Rather than say what I
>think Harvey might think, though, let me throw out a question people could
>discuss. I'm especially interested to know what you think of it, Harvey.
>
>
>	Is it likely that, in the foreseeable future, it will become
>routine for
>mainstream mathematicians to exceed any fixed axiomatic foundation--in the
>sense that, given any specific extension of ZFC, they will soon prove
>theorems that go beyond that?

I am not asserting such a thing, and the situation, as I see it, is quite
subtle.

The present situation is that normal mathematicians working on normal
mathematics use only a tiny fragment of the fixed axiomatic foundation ZFC,
and this has been going on for a "long" time.

I believe that no conjectures in the existing literature within normal
mathematics are independent of ZFC.

However, normal mathematics of the future is different. Boolean relation
theory is obviously normal mathematics of the future, uncovered before its
time in the present, for f.o.m. purposes.

In the foreseeable future, we see BRT and offshoots accepted as normal
mathematics, with small large cardinals routinely used to obtain the best
results.

Several people have challenged me about whether this will go beyond small
large cardinals into cardinals like measurables. If you look at the most
recent issue of the Bulletin of Symbolic Logic, there is an article by
Feferman, Maddy, Steel, and me. You will find this issue addressed.

I suspect that there will be another suitable subject of the future
unearthed to show the necessary use of measurable cardinals. It is probably
first appear as an elaboration of BRT. This will again be done by people in
f.o.m., who will lead the way. But it will be by no means routine, and
certainly NOT be a matter of diagonalization.

The fact that this is not a matter of diagonalization leads me to believe
that there may still be a fixed formal system for mathematics that suffices
for at least extremely long periods of time - say thousands of years. E.g.,
the large cardinal idea may prove to more or less run out of steam, and no
essentially different idea for generating axiom candidates may emerge.

The opposite possibility should at least be clearly mentioned. That is,

**given any reasonable formal system T for mathematics, there is a sentence
in normal mathematics that is neither provable nor refutable in T.**

This would be a very surprising and profound development. Note that in my
work, I use special properties of T.