query: models of CIC

[Thorsten Altenkirch]

Hi Milad,

 > Is there a realizability semantics or set theoretical model known for 
 > CIC (i.e. Calculus of Inductive Contrsuctions, the underlying type
 > theory of Coq proof assistant)? In CIC we have two impredicative
 > universes,Prop and Set and a cumulative hierarchy of Type_0, Type_1, ...
 > on top of them. Moreover we have (dependent) inductive types both on the
 > predicative and the impredicative level and we have dependent
 > elimination on Set (which is stronger than the one for Prop).

I am not sure what you mean by a "set theoretic model": there is an
old result by Reynolds which shows that there are no non-trivial
set-theoritic models of impredicativity (in classical set theory).

As far as realizability goes: omega-sets (and related models called
D-sets by Thomas Streicher) provide models for CIC and similar
calculi. Basically the idea is that a Type is modelled by an omega-set
(X,||-_X) where X is a set and ||-_X a relation between the natural
numbers (hence omega) and X s.t. forall x in X there is a number i
s.t. i ||-_X x. i is called the realizer of x. Given omega-sets
(X,||-_X) and (Y,||-_Y) the omega-set of functions is given by those
set-theoretic functions which are tracked by a recursive function
(which again can be encoded as a number) giving rise to a new relation
||-_X->Y. To be precise

     ({f : X-> Y | Ex m. m ||-X->Y f,
      m ||-_X->Y f iff Forall i,x.i||- x -> {m}i ||- f(x))

This can be extended to dependent function spaces (Pi-type), Sigma
types and it is easy to see that omega-sets support inductive types
such as Natural Numbers and W-types. To construct an impredicative
universe one observes that the subcategory of modest omega-sets 
(where the ||- relation is injective) provide a good interpretation
fro Prop. 

To model the hierarchy of Type-universes one seems to need
inaccessible cardinals.

There are a lot of (old) references to this, w-sets (or D-sets) are
the main topic of Thomas Streichers PhD and book (Semantics of Type
Theory, Birkhaeuser, 1991). Zhaohui Luo extended this in his PhD to
ECC. I used a variant - lambda sets - in my own PhD to show strong
normalisation also covering inductive types. There is much more...

Provaktive question: why does one need an impredicative universe? 

Cheers,
Thorsten