In der traditionellen Martin-Löf-Typentheorie gibt es keinen Unterschied zwischen Typen und Sätzen. Dies steht unter dem Motto "Sätze als Typen". Aber es gibt manchmal Gründe, sie zu unterscheiden. CoC macht genau das.
Es gibt viele Varianten von CoC, aber die meisten hätten
aber nicht T y p e : P r o p . Ein weiterer Unterschied zeigt sich, wenn wir unendlich viele Typuniversen haben und P r o p improvisieren (dies ist, was Coq tut). Betrachten Sie konkret eine Variante von CoC, bei der wir P r o p und unendlich viele Typuniversen T y p e 1 , T y p e haben
Prop:Type
Type:PropPropPropType1 ,
T y p e 3 mit
P r o pType2Type3
Die Bildungsregel für
∏muss erklären, wie
∏x gebildet wird:AB(x),wenn
Aentweder ein Satz oder ein Typ ist und
B(x)entweder ein Satz oder ein Typ ist. Es gibt vier Kombinationen:
PropType1Type2:Type1:Type2:Type3⋮
∏∏x:AB(x)AB(x)
A:Propx:A⊢B(x):Prop∏x:AB(x):Prop
A:Typeix:A⊢B(x):Prop∏x:AB(x):Prop
A:Propx:A⊢B(x):Typei∏x:AB(x):Typei
A:Typeix:A⊢B(x):Typej∏x:AB(x):Typemax(i,j)
The most interesting is the difference between the second and the fourth case. The fourth rules says that if A is in the i-th universe and B(x) is in the j-th universe, then the product is in the max(i,j)-th universe. But the second rule is telling us that Prop is not just "one more universe at the bottom", because ∏x:AB(x) lands in Prop as soon as B(x) does, no matter how big A is. This is impredicative because it allows us to define elements of Prop by quantifying over Prop itself.
A concrete example would be
∏A:Type1A→A
versus
∏A:PropA→A
The first product lives in
Type2, but the second one is in
Prop (and not in
Type1, even though we are quantifying over an element of
Type1). In particular, this means that one of the possible values for
A is
∏A:PropA→A itself.