[FOM] Kruskal's theorem and predicativism

[Nik Weaver]

In a recent post, Harvey Friedman repeats his claim that
Kruskal's theorem is predicatively unprovable.  He is careful
to say "on the Feferman-Schutte analysis of predicativity",
so that his statement is factually correct --- on the F-S
analysis, Kruskal's theorem is indeed not predicatively
provable.  However, this is only interesting if the F-S
characterization is valid, or valid on some interpretation
of predicativism, or, minimally, valid as an analysis of
*some* coherent philosophical stance.  I don't think it is,
and I can explain the difficulty fairly simply.

The attempt to precisely capture predicative reasoning goes
back to Godel's introduction of the constructible hierarchy.
This hierarchy is built up in such a way that each stage of the
construction introduces new sets that are explicitly definable
in terms of previously identified sets.  Godel expressed the
view that his hierarchy L_\alpha codified the predicatively
acceptable means of set construction, and that the only
impredicative aspect of the constructible universe L arises
from the fact that \alpha ranges over all ordinals.  This
view has been generally accepted.

Hao Wang considered the question of which ordinals are
predicatively acceptable, and tentatively proposed an answer:
the predicative ordinals are precisely the recursive ordinals.
Wang's idea was that (1) there is no predicative difficulty
in defining all recursive well-orderings of omega and (2) by a
result of Spector, no non-recursive well-ordering of omega
will appear in L_\alpha for any recursive \alpha.  Thus, the
predicativist can access all recursive ordinals but will never
be able to reach any non-recursive ordinal.

Wang's proposal was criticized by Kreisel, who drew an important
distinction between "definable" well-orderings and "provable"
well-orderings.  A predicativist can certainly accept as
well-defined all recursive orderings of omega.  However, it may
not be clear to him which of these orderings are well-founded
because the statement "there are no infinite decreasing sequences"
involves a quantification over all subsets of omega.  So, in order
to accept L_\alpha a predicativist would have to not only *define*
some ordering of omega which is isomorphic to \alpha, he would also
have to *prove* that it is a well-ordering.

Proof theorists should immediately see a problem: we have to prove
not just well-ordering but arithmetical transfinite recursion.  This
was not understood by Kreisel when he went on to suggest a model for
capturing the predicatively provable well-orderings of omega.  There
are a number of variations on the proposal but the basic idea is this.
Start with some base system that is predicatively acceptable and
consider infinite proof trees for this system.  We initially accept
all proof trees whose well-foundedness is provable in, say, Peano
arithmetic.  Call this set of proof trees T_1.  We then accept all
proof trees whose well-foundedness is established by a proof tree in
T_1; call this new set of proof trees T_2.  Proceed inductively.
Kreisel proposed that the ordinal \alpha is predicatively provable
precisely if an ordering of omega of order-type \alpha is proven
to be a well ordering by a proof in T_n for some n in omega.  The
Feferman-Schutte characterization of predicativity makes this
proposal rigorous.

There are two fatal problems in Kreisel's proposal, one slightly
subtle and the other not subtle at all.  The not subtle problem
is, why can the predicativist not see that he would accept all
proof trees in every T_n and then go further?  Glib responses
are unpersuasive because we have to ask why, if *we* can see
that a predicativist would eventually come to accept every proof
tree in every T_n, he cannot also see this?  I have been able
to find three separate places in the literature where Kreisel
attempts to deal with this objection, all of which fail, in my
opinion.  I discuss these in detail in Section 1.4 of my paper
"Predicativity beyond Gamma_0".

The more subtle problem has to do with going from T_n to T_{n+1}.
We already see this problem in Wang's consideration of the L_\alpha.
Suppose we have an ordering of omega which is isomorphic to \alpha
and we know that every nonempty subset has a least element.  How
do we go from this to actually constructing L_\alpha?

This is the problem of passing from well-ordering to transfinite
recursion. The difficulty arises from conflating classically
equivalent versions of the well-ordering concept which are not
predicatively equivalent.  Classically, if I have a total ordering
< of omega which is well-ordered in the sense that for any subset
S of omega,

(forall a)[(forall b < a)(b in S) --> a in S]

implies S = \omega, then it is also well-ordered in the sense
that for any statement P,

(forall a)[(forall b < a)(P(b)) --> P(a)]

implies P(a) for all a.  That is because I can form the set
S = {a: P(a)} and reduce to the first condition.  However,
predicatively acceptable comprehension axioms are fairly
limited and in general we cannot form the set S and draw the
desired inference from "well-ordered for sets" to "well-ordered
for statements".  But this is precisely what we have to do to
go from "\alpha is well-ordered" to "L_\alpha exists" --- or
to go from T_n to T_{n+1}.  Once we accept that a proof tree is
well-founded, why should we believe that it proves a true
statement?  We would have to infer well-foundedness for truth
from well-foundedness for sets.

Feferman later proposed a variety of formal systems for modelling
predicative reasoning.  All suffer from the same two difficulties
(why can't we go further and induction versus recursion).  Again,
a fairly comprehensive discussion can be found in my Gamma_0 paper.

The first half of that paper is an extended critique of the
Feferman-Schutte analysis of predicativity, and the second half
is devoted to formulating systems in which one can reason using
a hierarchy of Tarskian truth predicates, with the aim of proving
relatively strong well-ordering statements.  I produce systems
there which do prove the well-foundedness of a notation for the
ordinal \phi_{\Omega^\omega}(0), which is enough to prove Kruskal's
theorem (over a weak base system).  I also defend the predicative
legitimacy of these systems at length.

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