Semantics of Constructions(Ⅰ) — The Traditional Approach

It is well known that impredicative type systems do not haveset theoretical semantics. This paper takes a look at semanticsof inductive types in impredicative type systems. A generalizedinductive type is interpreted as an omega set generated byeffectivizing a certain rule set. The result provides a semanticjustification of inductive types in the calculus of constructions.