[FOM] Predicativity in CZF

[Nik Weaver]

Daniel Mehkeri asked about the predicativity of CZF.  In
general I tend to be suspicious of offhand claims that this
or that formal system is predicatively justified, as it is
easy for impredicativity to creep in in subtle ways and
people are not always as careful about this as they should be.

Specifically, he questions whether strong collection and
subset collection are predicative.  Strong collection says
(roughly): if for every x in u there exists y such that phi(x,y),
then there exists a set v that contains such a y for every x in a.
The complaint is that v has been constructed with reference to a
condition phi that may involve quantification over the entire
universe.

Actually, I think this is okay.  The traditional predicativist
concern is directed at constructions that require us, in the
course of constructing a set v, to consult a class of sets that
contains v (e.g., the entire universe).  That isn't really the
case here because strong collection takes as a premise that we
know (forall x in u)(exists y)phi(x,y).  In other words, we are
not being required to evaluate phi whilst constructing v, but
rather are permitted to construct v only under the assumption
that we have already (somehow) been able to evaluate phi.  Is
that clear?

(Incidentally, it was noted by Kreisel in a different setting
that this kind of justification does not work if classical logic
is being used.  The premise of strong collection must not only be
classically true; it needs to have been predicatively established.
So the predicative justification of strong collection requires an
intuitionistic interpretation of the logical connective "implies".)

Subset collection, on the other hand, seems to me clearly
impredicative.  This axiom scheme is of the form

(forall a,b)(exists u)(forall z)( P implies (exists v in u) Q)

where I am not writing out P and Q.  Here every one of an
unbounded class of sets z potentially dictates the appearance
of an element v in u, so we clearly do have to consult the
entire universe in the course of constructing u.  I can't
imagine why anyone would think the axiom in this form is
predicatively legitimate.

It is possible to reformulate subset collection so that one
is only consulting all subsets of a x b rather than the entire
universe.  However, it is well known that power sets are
generally not predicatively acceptable, so this doesn't really
help.

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