我希望考虑以下三个(相关的?)Coq定义。
Inductive nat1: Prop :=
| z1 : nat1
| s1 : nat1 -> nat1.
Inductive nat2 : Set :=
| z2 : nat2
| s2 : nat2 -> nat2.
Inductive nat3 : Type :=
| z3 : nat3
| s3 : nat3 -> nat3.
这三种类型都提供了归纳原理来证明一个命题成立。
nat1_ind
: forall P : Prop, P -> (nat1 -> P -> P) -> nat1 -> P
nat2_ind
: forall P : nat2 -> Prop,
P z2 -> (forall n : nat2, P n -> P (s2 n)) -> forall n : nat2, P n
nat3_ind
: forall P : nat3 -> Prop,
P z3 -> (forall n : nat3, P n -> P (s3 n)) -> forall n : nat3, P n
集合版本和类型版本还包含用于集合和类型上定义的归纳原理(rec和rect)。这是我对Prop和Set之间区别的全部了解;Prop的归纳性较弱。
我也读到过Prop是不明示的,而Set是明示的,但这似乎更像是一种属性而不是定义上的差异。
虽然有些实际(道德?)差别在Set和Prop之间很明显,但是Set和Prop的确切、定义上的差别以及它们如何适应类型世界并不清楚(对Prop和Set进行检查得到了类型(*(Set)+1*),我也不确定如何解释这个……
nat1
在Prop
中并没有定义自然数 - 这个问题在这里讨论过。 - Anton Trunov