[FOM] Predicativity in CZF

[Nik Weaver]

Michael Rathjen wrote:

> The brand of predicativity adhered to in MLTT is
> often called "generalized predicative" as is allows
> for the formation of inductively defined sets other
> than the natural numbers.

I have to disagree with this.  I don't think there is a
brand of predicativism that can admit general inductive
definitions.

It's an appealing idea on its face: inductively defined
classes can be built up in a series of well-ordered stages
and hence without circularity; therefore they are
predicative, in some sense.  (Michael, please correct
me if this is not a fair characterization.)

But look what happens.  Let's say we want to inductively
define a class A satisfying some closure conditions.  We
tell the predicativist to build A up in a series of
well-ordered stages.  Then he has to prove that A is
minimal, i.e., it is contained in any other class B that
satisfies the same closure conditions.

Well, since A is built up in well-ordered stages we'll
prove this by induction.  Let S be the set of stages at
which elements of A appear that do not belong to B.  If
S is nonempty then it has a least element and we can now
get a contradiction from the fact that B satisfies the
closure conditions which define A.  But wait a minute.
Was S a predicatively legitimate set?

No, it wasn't.  S cannot be defined using only bounded
quantifiers.  Predicativists do not have strong enough
comprehension axioms to prove the minimality of inductively
defined sets!

That's the difficulty in a nutshell.  Another way to say
this is that predicative well-ordering is subtle.  Merely
knowing that every nonempty subset has a least element does
not imply that we can establish induction for arbitrary
predicates, because we lack the necessary comprehension
axioms.  Actually in predicativism we have a hierarchy of
well-ordering notions characterized by their supporting
induction for different classes of predicates.  This seems
not to be widely understood.

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