[FOM] Predicativity in CZF

[Daniel Méhkeri]

Speaking about restricted comprehension: Constructive
Zermelo-Fraenkel (CZF) is supposed to be predicative.
And it does in fact restrict comprehension even
further than ZFC, allowing only subsets defined by
Delta_0 formulas (only bounded quantification).
However CZF has no such restriction on the formula
used in its strong collection axiom scheme (which
replaces the axiom of replacement). On the face of it,
this seems to allow defining a new set with reference
to the entire universe of all sets. 

The same could be said for CZF's subset collection
axiom scheme (which replaces the axiom of power set). 
One way out is that the entire schema is equivalent to
one "axiom of fullness" which doesn't refer to the
entire universe this way.

By contrast, Kripke-Platek set theory with Infinity
(KPI) only has Delta_0 collection. KPI is supposed to
be equiconsistent with CZF. 

Is there a way to predicatively justify strong
collection in CZF?  

Cheers, -DM


      Découvrez les styles qui font sensation sur Yahoo! Québec Avatars.
http://cf.avatars.yahoo.com/