[FOM] Predicativity and CZF

[Daniel Méhkeri]

In personal email I have been referred to the
type-theoretic interpretation of CZF. 

Briefly, as I understand it, a set is inductively
defined as a "small type" T and a (not necessarily
injective) function taking each instance of T to other
sets, which are its "intensional members"; the base
case is when T is an empty type. 

The axioms of CZF are interpreted using the
propositions-as-types interpretations, with the
primitive propositions defined by mutual induction as
follows: one set is a member of another if the former
is (extensionally) equal to an intensional member of
the latter. Two sets are equal if every set which is a
member of the first is also a member of the other
second and vice-versa.

"Small types" include the empty type, a singleton
type, and the natural numbers, and are closed under
disjoint sum, dependent sums and products, and
"Kronecker delta" types (if U is a small type and x,y
are elements of U, then I(U,x,y) is a small type which
is inhabited precisely when x and y are intensionally
equal.) Small types do not include the "universe of
sets" (nor the "universe of small types").

I hope I have got the above right.

Nik Weaver has suggested that Strong Collection might
be justified on an intuitionistic reading of the
axiom, which would roughly imply that we had uniformly
constructed each element satisfying the predicate
prior to constructing the set which collects them; so
even if the predicate quantifies over the universe,
this still is not circular. This seems plausible, and
I expect that is basically what the axiom works out to
in the propositions-as-types reading. But it is good
to have the more direct answer, especially since the
question of why Separation is restricted invites a
direct answer.

I'm sure Subset Collection can be worked through the
interpretation as well, but I'm hoping this can be
translated into a more direct answer as well.

Dan Mehkeri




      Découvrez les photos les plus intéressantes du jour.
http://www.flickr.com/explore/interesting/7days/