[FOM] about predicativity

[Harvey Friedman]

To reinvigorate interest in predicativity, I believe that it is necessary to
come up with something stunningly simple that is at least closely related to
the basic informal idea behind predicativity, which is of a level of
strength that is either Gamma0, or a bit higher or a bit lower.

I do not see how to do this.

So the natural focus of interest is on what predicativity means in practice,
for real mathematical statements.

Experience shows that standard mathematical statements *generally* have the
following properties.

1. Provable in ACA0, and so obviously predicative.
2. Provably equivalent to ATR0, and so definitely not predicatively provable
on anything like current views. This is because, such statements will fail
in the HYP sets.
3. Provably equivalent to Pi11-CA0. Even farther from being predicatively
provable. 

The case 2 is particularly interesting, since such statements have logical
strength measured by Gamma_0 by a theorem of mine relating ATR0 and Gamma0.
Hence they are interpretable in predicativity according to the status of
Gamma_0 and predicativity.

Case 2 includes such statements as comparability of well orderings (due to
me) and various forms of comparability (due to me and Jeff Hirst), and the
more recent comparability statement

given any two countable sets of reals, one is pointwise continuously
embeddable into the other

due to me, in the recently appeared Reverse Mathematics volume edited by
Simpson.

An exception is Kruskal's theorem, which is intermediate in logical strength
between 2 and 3 (due to me).

Also extended Kruskal's theorem (Kruskal's theorem with gap condition)
corresponds to 3 in strength (due to me). And the graph minor theorem is
stronger than the strength of 3 (due to me), but its exact strength is
unclear - although I do recall seeing that it is far less than a recursively
inaccessible ordinal in strength.

Another exception is various statements provable in ACA but not in ACA0,
such as the infinite Ramsey theorem for arbitrary finite exponent (due to
me). Any Pi12 sentence provable in ACA is provable in the theory of
<epsilon_epsilon_0 Turing jumps with set parameters, if I recall - making it
clearly well within any "normal" account of predicativity.

I know how to adjust numerical parameters in Kruskal's theorem and hit just
about any reasonable ordinal < the Ackermann ordinal (Theta sub Omega to the
omega, at 0), so that unless one settles on an exact characterization of
predicativity, one cannot settle on a verdict as to whether or not these
adjustments of Kruskal's theorem are predicatively provable or not. E.g.,
Kruskal's theorem for binary trees with two labels (with or without
left/right or "structure") corresponds exactly to Gamma0.

Harvey Friedman