[FOM] Least class that ...

[Nik Weaver]

Giovanni Sambin wrote:

> What you are aiming at here is just an inductive (or
> generalized inductive) definition. So a set is defined by its
> introduction rules (the inductive clauses) and the eliminations rule,
> telling that you can prove things by induction on those clauses.
>
> This is the idea underlying Martin-Loef's type theory, which is both
> intuitionistic and predicative (in a reasonable sense).

Also somewhat earlier Charles Parsons posted a reference to a
paper of his ("The impredicativity of induction") in which he
argues that generalized inductive definitions are predicative
in some sense.  This was the post
http://www.cs.nyu.edu/pipermail/fom/2006-January/009512.html
Similar comments have been made to me by others off list.

A crucial point that has not been explicitly discussed in these
comments is the question whether classical or intuitionistic logic
is to be used.  On its face it is fairly hard to believe that
theories of generalized inductive definitions using classical logic
should be straightforwardly predicatively acceptable, and I don't
know of anyone who has advocated that claim.  On the contrary,
it's not so implausible on its face that using intuitionistic
logic one could predicatively conceive of inductively generated
classes as perpetually incomplete entities that can always be
enlarged by repeatedly applying the closure condition.

Kreisel suggested in at least two places that intuitionistic logic
might render generalized inductive definitions predicatively valid
("La predicativite", Bull. Soc. Math. France 88, 1960, 371-391;
"Foundations of intuitionistic logic", in Logic, Methodology and
Philos. Sci, pp. 198-210, 1962).  There is also the Martin-Lof
tradition which doesn't have a lot of detailed discussion of the
question but seems to assume generalized inductive definitions are
predicative.  I can even point to a paper of Feferman ("Predicatively
reducible systems of set theory", in Axiomatic Set Theory, pp. 11-32,
1974) where this claim isn't actually made but it seems like one can
infer it.  In that paper Feferman comments that Kripke-Platek set
theory is impredicative because of the Delta_0 collection scheme
and refers to a paper of Kreisel for explanation.  Yet the paper
referred to clearly makes the point that the kind of impredicativity
involved is removed when one switches to intuitionistic logic.  So
one could infer that KP with intuitionistic logic is thought to be
predicative.

I disagree, and I have given a fairly detailed explanation of why
generalized inductive definitions are impredicative *even if
intuitionistic logic is used* in Section 2.5 of my paper
"Predicativity beyond Gamma_0".  The reason is actually kind of
subtle.  Granting that we can conceive of inductively generated
classes as perpetually incomplete entities that can always be
enlarged by repeatedly applying the closure condition, there is
a problem in verifying the minimality condition required of
inductively defined classes.  This seems to require a transfinite
induction along a well-ordered set that corresponds to the stages
in the construction of the class, and the subtle problem that arises
here hinges on the predicative inequivalence of classically equivalent
versions of the well-ordering concept.  Namely, it is not predicatively
possible to meaningfully talk about well-ordering in the sense of
supporting transfinite induction for all properties, only with
respect to some restricted family of properties whose senses are
all understood in advance.  The problem for inductively generated
classes is that in order to prove minimality one has to carry out
a transfinite induction with respect to the property of belonging
to the class being defined.  This introduces a circularity which
I think is absolutely intractable.  I refer to my paper for the
details of the argument.

The failure to distinguish between predicatively inequivalent
versions of the well-ordering concept is a fundamental error
that pervades the literature on predicativism, and on my analysis
it is present here too.

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