[FOM] Impredicativity needed?

[Harvey Friedman]

On 4/6/06 2:10 AM, "Bill Taylor" <W.Taylor at math.canterbury.ac.nz> wrote:

> Somehow it came across me, on first seeing a sketch of them,
> that the standard proofs of basic Ramsey theory results
> made use of impredicativity in an essential way.
> (There may be longer proofs that do not, OC.)
> 
> Can anyone confirm please?  Do basic Ramsey theory proofs require it?
> 

I assume that the basic Ramsey theory you are talking about is the original
infinite Ramsey theorem. It says that if you color the unordered k-tuples of
nonnegative integers with p colors then there is an infinite set of natural
numbers such that all of the unordered k-tuples drawn from that set have the
same color. 

For each fixed k, this is provable in ACA_0, which makes it predicative
under any proposed interpretation of predicativity.

Now the full statement is not provable, but is provable in ACA, which
differs from ACA_0 in that it allows for induction for all formulas.

There are two positions that I have seen regarding ACA.

1. Anything provable in ACA is "obviously predicative" since ACA_0 is
obviously predicative, and induction on the natural numbers, without
restriction, is predicative.

2. Induction on the natural numbers is not automatically predicative,
because the formula to which one is applying induction is not predicatively
meaningful. 

Those adhering to view 2 will want a different proof of RT = Ramsey's
theorem. 

There is one, that uses the principle:

*) for all n and subsets x of N, the n-th Turing jump of x exists.

In fact, I proved a very long time ago that

RCA_0 proves that RT is equivalent to *).

Then most people involved with predicativity assert that *) is obviously
predicative. However, they seem to split on just how to respond to anyone
that says "why is *) predicative?"

I was planning to write a sequel to my
http://www.cs.nyu.edu/pipermail/fom/2006-April/010343.html

when I saw your posting.

In strict predicativity, as treated in
http://www.cs.nyu.edu/pipermail/fom/2006-April/010343.html

 *) is clearly provable. It is also clearly provable in Feferman/Schutte.

HOWEVER, there is something that I call

ultra predicativity

which is more limited that strict predicativity, which I was planning to
discuss in my sequel.

In ultra predicativity, one absolutely forbids comprehension where there is
any set quantifier present, and adheres to induction strictly in the form:
every nonempty set has a least element.

One is then led to ACA_0 as the analysis of ultra predicativity.

Under this analysis, RT is NOT ultra predicative.

Harvey Friedman