[FOM] FOM Digest, Vol 66, Issue 11, Predicativity in CZF (Nik Weaver)

[rathjen@maths.leeds.ac.uk]

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

Let's not squabble about this. "Generalized predicative" it has been called.

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

I completely agree. This is well-known to proof-theorists, but as you say
probably not widely known elsewhere. In the absence of full separation,
the proof-theoretic strength of a theory more often than not hinges
crucially upon the complexity of the predicates for which
 induction and transfinite induction is available. To illustrate this in
the case of CZF let's go back to the question of whether the subset
collection axiom is impredicative.
It turns out that the proof-theoretic strength of CZF is the same as that
of CZF* := CZF without Subset Collection. So here the situation is rather
different than in the case of ZF, where dropping the power set axiom gives
you a much weaker theory.
 On the other hand if one drops Set Induction from the axioms of CZF the
resulting theory CZF^- is much weaker. Indeed it is of the same strength
as Peano arithmetic. If one restricts set induction in CZF to Sigma
formulas one stills ends up with a theory of strentgh below Gamma_0. Thus
fragments of CZF can be predicatively justified via reduction
to predicative justified theories.
Whether CZF has a predicative justification in a stricter sense (stricter
than "generalized predicative") would depend on the particular form of
predicativity one endorses, i.e. whether the Bachmann-Howard ordinal
is reachable via "predicative" means.

Michael Rathjen