[FOM] FOM Digest, Vol 66, Issue 5, Predicativity in CZF (Daniel M?hkeri)

[rathjen@maths.leeds.ac.uk]

Predicativity of CZF is usually not argued for directly.
There is a constructive notion of set which can be formalized in
Martin-Loef type theory (MLTT). Peter Aczel has given an interpretation of
CZF based on this notion in MLTT. The argument for CZF's constructivity
can thus be based on that of MLTT. 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.
Constructive set theory originated with John Myhill. In his 1975 JSL paper
he presented a formal theory CST (Constructive Set Theory). One of the
axioms of CST is exponentiation, that is the statement that given two sets
A and B, the set of all functions from A to B,  A->B, forms a set. The
subset collection axiom of CZF is a generalization of exponentiation.
Myhill rejects the power set axiom but accepts exponentiation:
``Power set seems especially nonconstructive and impredicative compared
with the other axioms ....
One could make the admittedly vague, objection to the existence of the set
A->B of mappings of A into B but I do not think the situation is parallel
- a mapping or function is a rule, a finite object which can
actually be given .."

Michael Rathjen