[FOM] predicative foundations

[Harvey Friedman]

The claims that predicativity has some special place in the robust hierarchy
of logical strengths ranging from EFA through j:V into V are unjustified.

On can stop a lot earlier than "predicativity", say, stop at ACA0 or RCA0,
or one can stop somewhat higher than "predicativity", say at one inductive
definition, or Pi11-CA0. Or one can stop even higher at, say, the theory of
a recursively inaccessible, or what have you.

All of these stopping places, and many more, have very "nice" stories. All
of these stories have advantages and disadvantages. These advantages and
disadvantages make sense and have their proponents, both mathematically and
philosophically. 

One can, for many such stopping places, create models of mathematical
practice with stories about how one can code "almost all" or "nearly all",
or whatever. Or "almost all" blue mathematics, or "almost all" green
mathematics, or whatever.

At the extreme ends, the stories, of course, have to be strained in one way
or another. 

At the low end, EFA, the story fits very well into finite mathematics
(arithmetical theorems).

At the very high levels, we don't know enough to give many stories,
particularly as relates to mathematical practice. The stories are limited,
and even extremely limited at j:V into V. But some of this is changing,
hopefully, through what I am doing now.

For example, Weaver did not answer the following questions that I raised in
my last posting responding to him. I will raise them again.

1. Give me one example of a theorem in what you call "normal" or "core"
mathematics (I make a distinction between the two, and I don't know if you
do), that is handled in "predicativity" but not in ACA0. I asked if there
was a significant range of such. It would also be nice to examine your
viewpoint on this question if we replace ACA0 by RCA0. Both ACA0 and RCA0
are substantially lower than predicativity - both mathematically and
philosophically.

2. Give me one example of a theorem aobut finite objects, in what you call
"normal" or "core" mathematics (I make a distinction between the two), that
is not handled in PA, or even EFA. Both PA and EFA are far less than
predicativity - both mathematically and philosophically.

3. Clearly 1,2 relate to the issue of how special the stopping place of
predicativity really is. E.g., why not stop earlier?

Weaver writes:

> It [predicativity] is a stopping place based on accepting the natural numbers,
> which have been considered obviously absolutely objective for
> thousands of years,

Predicativity does accept a unique objective full system of natural numbers
on face value. However, it has MUCH MUCH MORE than that in it.

I do not think that a unique objective full system of natural numbers is
obviously appropriate or obviously inappropriate. I am sure that we do not
know nearly enough about f.o.m. to make such a decision.

Furthermore, I do not think that most intellectuals accept such a thing. Of
course, there are some on the f.o.m. here who categorically reject such a
thing (I am not among them).

In particular, many scientists and engineers are dubious about such a
notion, and are incomparably more comfortable with substantial initial
segments of it. 

>while not accepting the infrastructure of
> Cantorian set theory which (1) is based on highly dubious
> metaphysical beliefs about a fictional world of sets,

I don't agree that the world of sets is fictional, and I don't agree that
the word of sets is not fictional. We just don't know nearly enough about
f.o.m. to make such a determination.

There are obviously equally good arguments on both sides of this. Godel took
the non fictional view. Is there something that compels you to so
confidently disagree with Godel? On what basis?

For some, a very compelling picture would be the obvious way in which ZFC
extrapolates from finite set theory. I.e., one goes from the finite levels
of the cumulative hierarchy of sets - which I assume you accept without
reservation - to the cumulative hierarchy of sets, and makes essentially the
same assertions, seeing essentially the same phenomena.

I don't uncritically endorse this picture, but I certainly don't know how to
argue strongly against it.

>(2) is
> inconsistent in its naive form,

So is the natural number picture, in its naïve form. It is naively clear
that there is a notion of small or physically realizable natural number, and
that it is closed under successor. This is roughly analogous to the naïve
idea that a set can be formed out of sets in any way with no restrictions.

>and (3) is essentially irrelevant
> to core mathematics.

This is of course false historically. Set theory arose out of the (at least
then) core mathematical activity of working with closed sets of real
numbers, in connection with trigonometric series. Do you wish to repudiate
the notion of closed sets of real numbers, or trigonometric series in some
way?

Also "essentially" has to be used. This merely reflects the fact that
rigorous mathematics is an extremely YOUNG subject, probably having been
developed as little as 10^-9 or less of its naturally mature state.

There is no doubt that the exceptions - or exceptions you wish to
marginalize - will grow as time proceeds.

In particular, what I am doing now strongly suggests that the situation may
be COMPLETELY different within a few years.

> You may not find this view compelling, but you should at least
> recognize that it is of basic philosophical significance, and
> not merely one out of countlessly many possible stopping places.

As I have said before, after many different versions and analyses of
predicativity, it does not appear that predicativity has a clear enough
meaning to clearly justify any particular stopping place to be identified
with it. One particular stopping place has been accepted as the standard
stopping place for whatever "predicativity" means, and this is not going to
change in the near future.
> 
> I have never advocated
> banning impredicative mathematics nor have I ever said it is
> bad mathematics.

I'm glad to hear that. Have you any comments about Pollard's recent
hhttp://www.cs.nyu.edu/pipermail/fom/2006-February/009698.html and my reply
to him http://www.cs.nyu.edu/pipermail/fom/2006-February/009726.html?
> 
> What I have said is that core mathematics is 99% predicative,

If that is the case, then probably under your measure it is also 99% ACA0.
Why not use ACA0?

>and
> I have made the observation that most core mathematicians generally
> regard genuinely impredicative mathematics as pathological.

What does "most" mean here?

 Within the last few months, I had some conversations with a Fields Medalist
(core mathematician) - a different one than I have ever previously alluded
to. 

I asked him if he ever used the axiom of choice in his main research.

He surprised me, and said yes, a lot of the time, and in fact, the example
he gave me surprised me on several counts.

1. He and his colleagues use it all the time, and things like it. It
involves only countable structures, and is very natural - for them and for
me.
2. He and his colleagues did not know (according to him) how to remove the
axiom of choice. 
3. In fact, they identify Zorn's Lemma as the method of proof.
4. The proof they have of it not only uses the axiom of choice, but is
blatantly highly impredicative in other ways. Even beyond iterated inductive
definitions.

In fact, it is clear that they are indiscriminately working in a system like
full second order arithmetic with lots of choice  - at least!

I got suspicious about the need for choice, and calculated that the
statement is Pi13, and hence can automatically be proved without the axiom
of choice - BY A WELL KNOWN METAMTHEOREM FROM SET THEORY!

Then I dug in, and saw that I had considered just this situation in a more
general context earlier, and published on it.

So how does that fit into your claim that predicativity matches mathematical
practice better than set theory?

I had already published an equivalence of the principle behind this
situation with Pi11-CA0 in Simpson's Reverse Mathematics conference volume
(ASL), which has appeared.

>That's
> an observation, not a value judgement.

>From what I said, you now see that your "observation" needs major
modification.

>I've also argued that one
> has a clear philosophical basis for believing in the correctness
> of predicative mathematics and one does not have such a basis for
> impredicative mathematics.

This is false. There is also a clear philosophical basis for the
impredicative comprehension axiom scheme. The philosophical basis is of
course NOT THE SAME as that for "predicativity" or for ACA0. Why is one
clear and not the other? There is, in reality, only levels. You are claiming
"clarity" for one of these levels and "not clarity" for another. This cannot
be justified - at least not with what we know now.

>That's not the same as saying it should
> be banned!

It is just a weaker form of banning. You seem to argue that it should be
banned if one says that one is doing mathematics with a clear philosophical
basis. Many people want to have a clear philosophical basis, or think they
have a clear philosophical basis, for the mathematics that they do. The
practical effect for them of what you say is: to BAN their work.

Do you want to BAN some of the work of that Fields Medalist and his
colleagues? I think I know him well enough to think that he feels that he
has a "clear philosophical basis" for his work.

> Yes, surely 95% of the theorems that appear in the Annals could be
> recovered in ACA_0.  I wonder what your point is here.
> 
> The relevance of your comment about RCA and RCA_0 is lost on me.

As I said earlier, then why not stop at ACA0 or RCA0?

> As I've pointed out to you before, I have shown that Kruskal's
> theorem is predicatively provable in my paper "Predicativity
> beyond Gamma_0". 

Not according to the usual commonly accepted interpretation of
"predicativity" due to Shutte and Feferman. This is not going to change in
the near future, for many reasons.

>Whether the graph minor theorem is predicatively
> provable is open.

It doesn't under the commonnly accepted interpretation of predicativity.

> I claim to have decisively refuted the Feferman-Schutte analysis
> of predicativism.  You continue to refer to it as if it were
> established fact.  Are you willing to directly assert that I
> am wrong?

I am asserting that the concept of "predicativity" is not sufficiently clear
to allow anything but a broad range of equally legitimate interpretations.
So the established convention given by Feferman and Schutte will stand for
the forseeable future.

Instead of trying to find hidden meaning in a word like "predicativity", one
is better off simply accepting the fact that there are a hierarchy of levels
ranging from EFA to j:V into V, and talk about those levels.

The graph minor theorem is above the level Pi11-CA0, and from some initial
discussions with Robertson, which will be continued, seems to be below
omega^omega hyperjumps.

That is how we should talk about GMT. Not mix it up with arguments about
hidden meaning in a word like "predicativity".

Having said that, I think that it IS worthwhile to look for hidden meaning
in "effectively computable". Here I don't mean bringing in physical ideas.
That's "physically computable", and I am extremely dubious about that
notion. I don't think that we know anything near enough about the physical
world to have any idea what "physically computable" means, let alone have a
good working model of it.

>> I have no doubt that the situation will look entirely different
>> by the end of the century. At some point, there will be a special
>> kind of breakthrough that shows how to use higher principles in a
>> huge variety of contexts to gain sharper information of a valued
>> kind.
> 
> I don't believe this, but it would be very important if it did
> happen and I sincerely wish you luck.

Things are working according to plan. It is slow, and I have been doing this
for over 40 years. Given that mathematics certainly has a life span of over
10^9 years, 40 man years is essentially nothing. So it is safe to expect
nothing, but you will not get nothing.

At least it is obvious that I am setting in motion a process which will lead
to this breakthrough. With some luck, I will find it myself.

> I do wonder whether that sharper information will be true information.
> I specifically wonder what grounds there are for believing that
> arithmetical consequences of large cardinal axioms are actually
> true, if one is not a platonist.
> 

The result will be that if you point to any remotely natural stopping point
from EFA to j:V into V, including yours or anybody else's favorite stopping
places, there is an example of a Pi01 sentence in normal and even core
mathematics, which is exactly at that level. Just go up to the places you
are interested in, and you will see the examples, and draw your own
philosophical conclusions - if you want to.

Harvey Friedman