[FOM] Friedman on predicativity

[Nik Weaver]

Harvey Friedman, in a message that may or may not have been
a response to my recent posts on predicativism, wrote:

> 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.

I disagree with this conclusion.  In my paper "Predicativity beyond
Gamma_0" I have presented predicatively valid formal systems which
prove the well-ordering of notations for all ordinals up to and
beyond theta_{Omega^omega}(0).  So all such adjustments of Kruskal's
theorem are predicatively provable.

I don't know about the graph minor theorem, but I believe that my
well-ordering proof techniques can be substantially extended and
this may very well lead to a predicative proof of results even of
this degree of strength.  There is something for experts in proof
theory to work on here.

The rest of the message was basically a review of some of Friedman's
impressive contributions to reverse mathematics, work which I hold
in the highest regard.  However, I do have a point to make about
the following sequence of assertions:

> Experience shows that standard mathematical statements *generally*
> have the following properties.
[snip]
> 2. Provably equivalent to ATR0, and so definitely not predicatively
> provable on anything like current views.
[snip]
> Case 2 includes such statements as comparability of well orderings ...

First of all, I should mention that since Gamma_0 is predicatively
provable and this implies the consistency of ATR_0, statements of this
degree of strength can be predicatively proven consistent.  But more
important here is the fact that "comparability of well orderings" in
the sense used here is not a standard mathematical statement.  I would
characterize it as a specialized proof-theoretical statement.

We must remember that the well-ordering concept has classically
equivalent versions which are not predicatively equivalent.  For
example, classically we can define a linear ordering < on omega to
be a well-ordering if

(*) for every subset X of omega, if X is progressive with respect
to < then X = omega

holds.  ("Progressive" means: for all a, if every element less than
a belongs to X then a belongs to X.)  And then using a comprehension
axiom we can prove for any predicate P that if P(.) is progressive
then P(a) holds for all a in omega.  Predicatively we cannot do this
in general, so "well-ordered for sets" does not provably imply
"well-ordered for predicates".

But it is the latter version of well-ordering which is significant in
ordinary mathematics, not the former.  The value of well-ordering to
the working mathematician is that one can use it to prove a statement
is true for all values of some parameter when that parameter ranges
over a well-ordered set.  And when we use the term "well-ordered" in
this sense there is no problem in predicatively proving comparability.

It is only when "well-ordering" is used in the weaker, specialized
sense (*), the sense that is not central to mainstream mathematics,
that comparability becomes a problem.

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu

http://www.math.wustl.edu/~nweaver/conceptualism.html