[FOM] Impredicativity of Kruskal's Theorem

[Nik Weaver]

Hendrik Boom wrote:

> Nik, perhaps it would further the discussion to have a presentation
> of Wang/Lorenzen predicativity.

This wasn't a distinct conception of predicativism, but merely a
naive belief that generalized inductive definitions are predicative.
As Bas Spitters mentioned in a recent message, modern type theorists
tend to feel the same way.  Generally speaking I think people who
believe this are not primarily interested in predicativism but have
a vague sense that generalized inductive definitions appear to be
predicatively okay.  However, there is a critical difficulty, which
I suspect the type theorists aren't aware of.

Intuitively, a "generalized inductive definition" is a definition
of a set of natural numbers as the smallest set which satisfies
some closure property.  For example (a classical example), we might
look for the smallest set such that (1) the set contains the number
0; (2) if x is in the set then so is 2^x; (3) if y is the Godel
number of a recursive function whose range is contained in the set,
then 3 times 5^y is in the set.

The slick classical way to identify the minimal set satisfying
such a closure property is by taking the intersection of all
sets that have the closure property.  (There's always at least
one, namely omega itself.)  Nobody thinks this construction
is predicative, since not all subsets of omega are initially
available to be intersected.

However, you can also try to build up the desired minimal set
"from below".  In the above example, let S_0 = {0}.  Then let
S_1 be S_0 together with all numbers mandated by conditions (2)
and (3) given that the set contains S_0, let S_2 be S_1 together
with all numbers mandated by (2) and (3) given that the set
contains S_1, etc.

This is slightly troublesome because the construction may have
to continue into the transfinite (to S_omega, S_{omega+1}, etc.).
Classically we can prove that it must terminate at some countable
ordinal, but again that's not predicative because not all countable
ordinals are initially available.

Still, one might hope to treat the inductively defined class in
some sort of loose way as a variable entity which can always be
further enlarged, the same way that predicativists treat the real
line or the power set of omega.  Such things used to be called
"potential totalities".  So, we say that a number z belongs to the
class if there exists a countable ordinal alpha and a sequence
of sets S_beta, 0 <= beta <= alpha, as above such that z is in
S_alpha.  But we recognize that predicatively the class of
countable ordinals is not fixed but can always be enlarged.

Here's the problem.  Exactly what does "countable ordinal" mean?
As I've stressed repeatedly, there are predicatively distinct ways
of interpreting this expression.  The simplest interpretation is
to say that a total ordering < of omega is well-ordered if for
any subset S of omega,

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

implies S = omega.  But we could also ask that for larger classes
of statements P the premise

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

should imply P(a) for all a.  Classically you can go from the former
to the latter using a comprehension axiom, but predicatively the
second form appears to be genuinely stronger.

So, we must fix some version of the well-ordering concept in order
to execute our proposed treatment of inductive definitions.  Can
this work?  No, it could never work because we need to be able to
verify the minimality property ("the *smallest* set that satisfies
the closure property").  In order to show this I need to perform a
transfinite induction on a statement of the form "if z belongs to
the inductively defined class then it also belongs to some other
class which satisfies the same closure property".  In order to
be able to do this I would have to have used a version of the
well-ordering concept which is strong enough to support
transfinite induction for statements of this form.  But these
statements refer to the inductively defined class so they would
not have been available before the class was defined.  This is
circular!!  In order words, in order to define the inductively
generated class I need a well-ordering concept that refers to
the class it is being used to define.

I wonder how type theorists who consider generalized inductive
definitions to be predicative would answer this objection.  Would
they agree with Harvey Friedman that I am only talking about
"Weaver predicativity", so they don't need to worry about it?

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