Coq 中 Prop、Set 和 Type_i 的基数

Question

我们可以将 Coq 中的 cardinals 分配给 Prop、Set 和每个 Type_i 吗？我只在 Coq 的库中看到 finite cardinals 的定义，所以也许我们需要大红衣主教的定义。

根据证明无关语义，例如暴露的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

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

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