[FOM] Predicativity in CZF

[Nik Weaver]

I wrote:

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

And Michael Rathjen replied:

> I completely agree. This is well-known to proof-theorists,
> but as you say probably not widely known elsewhere.

I'm sure you are right, but proof theorists have not been
sensitive to this point in analyses of predicativism.  I
already mentioned that the purported predicative justification
of generalized inductive definitions hinges on a failure to
recognize just this distinction.  The classical Feferman-Schutte
analysis involves the same fallacy when we pass from "the
notation \gamma_n is well-ordered" to "the theory S_{\gamma_n}
is valid" (where (\gamma_n) is the canonical sequence of
notations increasing to \Gamma_0).  In order for this inference
to be legitimate we would have to have induction for the
predicate "S_a is valid", which can't even be expressed in
the language of second order arithmetic.

> On the other hand if one drops Set Induction from the axioms
> of CZF the resulting theory CZF^- is much weaker.

Right!  I wasn't thinking about this when I wrote my earlier
message about strong collection and subset collection.  But
now that you mention it, set induction is also impredicative
--- with, again, predicative well-ordering being the issue.

The justification for set induction (again, please correct me
if I'm wrong) is that sets are thought of as being built up in
well-ordered stages.  But that would only be enough to support
set induction for delta_0 predicates.

Nik