coq - Coq 中 Prop、Set 和 Type_i 的基数

Question

我们可以分配cardinals在 Coq 到 Prop , Set每个 Type_i ?我只看到finite cardinals的定义在 Coq 的库中，所以也许我们需要大红衣主教的库开始。

根据证明无关语义，例如暴露here , Set和 Type_i形成inaccessible cardinals的递增序列.这可以在 Coq 中证明吗？
Prop由于不可预测性，似乎更复杂。证明无关性意味着我们识别相同 P : Prop 的所有证明, 并解释 Prop本身作为对{false, true} .所以Prop的红衣主教将是 2。但是，对于任何两个证明 p1 p2 : P , Coq 不接受 eq_refl p1作为 p1 = p2 的证明.所以 Coq 不能完全识别 p1和 p2 .另一方面，不可预测性意味着对于任何 A : Type和 P : Prop , A -> P是 Prop 类型.这使得居民比 Set 多得多。 .

如果这太难了，Coq 能否证明 Prop和 Set是不可数的？作者 Cantor's theorem , Coq 很容易证明不存在满射nat -> (nat -> Prop) .这似乎与证明不存在射程不远nat -> Prop .但是我们需要过滤器Prop -> (nat -> Prop) , 分离出 Prop有一个免费的nat多变的。我们可以在 Coq 中定义这个过滤器吗，因为我们无法在 Prop 上进行模式匹配？ ?

Answer 1

无法显示 Prop在 Coq 中是不可数的。 ClassicalFacts标准库中的模块显示命题简并公理 forall A : Prop, A = True \/ A = False , 等价于排中和命题外延性的存在。由于 Coq 的集合论模型验证了这两个公理，因此 Coq 无法反驳退化。

当然可以证明 Set和 Type是无限的，因为它们包含所有类型 Fin n以n为界的自然数，并且这些类型可证明彼此不同，因为它们具有不同的基数。我怀疑可以通过调整通常的对角化参数来证明它们是不可数的——也就是说，假设一些可逆计数函数 e : nat -> Set ，并尝试对“不包含自身”的所有自然数类型进行编码。我不知道你将如何证明这些类型是不可接近的红衣主教。