Cardinality of Prop, Set and Type_i in Coq

4
votes

Can we assign cardinals in Coq to Prop, Set and each Type_i ? I only see the definition of finite cardinals in Coq's library, so maybe we need that of big cardinals to begin with.

According to the proof-irrelevance semantics, for example exposed here, Set and the Type_i form an increasing sequence of inaccessible cardinals. Can this be proven in Coq ?

Prop seems more complex because of impredicativity. Proof-irrelevance means we identify all proofs of the same P : Prop, and interpret Prop itself as the pair {false, true}. So the cardinal of Prop would be 2. However, for any two proofs p1 p2 : P, Coq does not accept eq_refl p1 as a proof of p1 = p2. So Coq does not completely identify p1 and p2. And on the other hand, impredicativity means that for any A : Type and P : Prop, A -> P is of type Prop. That makes a lot more inhabitants than in Set.

If this is too hard, can Coq prove that Prop and Set are uncountable ? By Cantor's theorem, Coq easily proves that there is not surjection nat -> (nat -> Prop). This does not seem very far from proving there is not surjection nat -> Prop. But then we need the filter Prop -> (nat -> Prop), that isolates which Prop's have a free nat variable. Can we define this filter in Coq, since we cannot pattern-match on Prop ?

1
coqcardinality

1 Answers

2
votes

It is not possible to show that Prop is uncountable inside Coq. The ClassicalFacts module in the standard library shows that the axiom of propositional degeneracy, forall A : Prop, A = True \/ A = False, is equivalent to the presence of the excluded middle and propositional extensionality. Since Coq's set theoretic model validates these two axioms, Coq cannot refute degeneracy.

It is certainly possible to show that Set and Type are infinite, since they contain all types Fin n of natural numbers bounded by n, and these types are provably different from one another since they have different cardinality. I suspect that it is possible to show that they are uncountable by adapting the usual diagonalization argument -- that is, assume that some invertible count function e : nat -> Set, and try to encode something like the type of all natural numbers that "do not contain themselves". I do not know how you would go about proving that these types are inaccessible cardinals.