[FOM] what is predicativity?

[Harvey Friedman]

Reply to Avron

http://www.cs.nyu.edu/pipermail/fom/2006-April/010466.html

Avron wrote:

"I have recently refrained from writing to FOM, because I am not
sure anymore whether the people who write to FOM are really interested
in what have always taken to be the real problems concerning the
foundations of mathematics."

Since I am interested in the real problems concerning f.o.m., you probably
have a different idea of what these real problems are. What are they?

Avron wrote:

"In principle, a true predicativist will never be able to
accept any given formal system as an adequate representation
of well-founded/absolute/predicativist mathematics. Because
if s/he accepts such a system s/he will be able to go beyond it
(e.g. by accepting as  absolutely proved any  arithmetical
sentence whose truth can be recognized as  equivalent to the
consistency of that system)."

That still allows for a system S with infinitely many axioms, written down
by someone who is acting at least a bit beyond predicatively, with a claim
that the predicativist can come to accept any finite number of the axioms,
but cannot come to accept all at once - e.g., because the predicativist
cannot formulate a suitably meaningful predicate to which to apply
induction. This appears to be the approach of Feferman/Schutte.

Do you regard Feferman/Schutte as being wrong in some real sense? And in
what sense? Has it been "refuted"?

Avron wrote:

"It is common nowadays to claim that no foundational
program works. Well, the predicativist program *does* work and is
successful in providing secure foundations to the major and
most important (and interesting) parts of mathematics - and it does
so for a very low cost. As far as I can tell, no such claim
can be made about any other foundational program."

There is a cost trade-off. You might prefer the one that corresponds to
predicativity. It is of course difficult to assess this cost if one is too
vague about what is predicative in practice.

The cost tradeoff is represented in great detail by the usual canonical
hierarchy of logical strengths ranging from, say, EFA (exponential function
arithmetic) to, say, ZF + j:V into V.

At lower levels, more people tend to have more confidence, because they view
things to be closer to directly observable reality. On the other hand, they
lose certain mathematical methods and theorems.

At higher levels, one gains mathematical methods and theorems, but one loses
many people's confidence, as things are farther away from directly
observable reality.

Obviously, there is a lot more to the story than these above two paragraphs.

We are only beginning to understand well just what theorems one loses as one
goes lower. 

Of course, mathematics is a quickly growing enterprise, and has been around
as a major professional activity with major numbers, for only a very short
period of time. 

As I have said many times before, I do not think that what has transpired in
mathematics, in light of the above paragraph, is even remotely
representative of the future.

So I fully expect a huge increase not only in the number of interesting
theorems that will be proved, but also a huge increase in the number of
interesting theorems that will be proved that require ever increasing levels
of the canonical hierarchy.

One has already seen a glimpse of what is yet to come. I have made much much
stronger conjectures along these lines.

Now for some specific questions for Avron.

Is Kruskal's theorem provable predicatively? We have exactly one person on
the FOM, and probably exactly one person worldwide, who has asserted this.
What is your view? Or is this an open ended mystery?

The labeled Kruskal theorem (due to Kruskal in his original paper), implies
ATR0. Do we agree that that makes it impredicatively provable? Or is this an
open ended mystery?

I once wrote on the FOM things like this:

Kruskal's theorem is predicatively unprovable on the Feferman/Schutte
analysis.

This continually prompted objections from exactly one FOM subscriber. Do you
object to this statement?

Also I wrote in http://www.cs.nyu.edu/pipermail/fom/2006-April/010411.html

"CHALLENGE. Present an entirely transparent nontechnical informal/semiformal
explanation of "predicativity" that is really powerful enough to determine
the status of basic assertions.

TEST CASE. Consider

'the truth predicate for arithmetic exists'

Can your presentation of predicativity clearly establish this? Let us go
thru, SLOWLY, why the above is true, predicatively, on the basis of your
presentation."

So far, no one has taken up the challenge. Will you?

Finally, you assert the open ended nature of predicativity. Do you also
assert the open ended nature of "effectively computable"? (I am talking
about the context of finite strings from a finite alphabet).

Harvey Friedman