# Equality of decidable proofs?

I want to know if the decidability of equality of two decidable proofs of the same proposition can be proved without any additional axioms in Calculus of Inductive Constructions.

Specifically, I want to know if this is true without any additional axioms in Coq.

$$\forall P: \texttt{Prop}, P \vee \neg P \Rightarrow (\forall p_1 : P, \forall p_2: P, \{p_1 = p_2\} \vee \{p_1 \neq p_2\})$$

Thanks!

Edited to correct the error: Edit 2 to make Prop more explicit

• What you wrote does not make sense. If $P$ is a proposition then $p : P$ is a proof, and you cannot form $p \lor \lnot p$. Did you mean your hypothesis to be $P \lor \lnot P$ instead of $p \lor \lnot p$, i.e., "$P$ is decidable"? – Andrej Bauer Dec 11 '14 at 8:13
• Sorry, I meant the hypothesis "$P$ is decidable", i.e. $P \vee \neg P$ – Adam Barak Dec 11 '14 at 9:36
• Take $P$ to be $\mathbb{N} \to \mathbb{N}$, and the statement is false, since you can easily inhabit $(\mathbb{N} \to \mathbb{N}) \vee \lnot(\mathbb{N} \to \mathbb{N})$ with $\mathsf{inl}(\lambda x.\;x)$, and function equivalence is obviously undecidable. Are there any other conditions on $P$ you have in mind? – Neel Krishnaswami Dec 11 '14 at 11:18
• P should be a proposition. (Actually, in my development, I already use functional extensionality, so the statement can still hold for me, but let's ignore functional/propositional extensionality for now). – Adam Barak Dec 11 '14 at 16:31
• Function extensionality doesn't imply that function equivalence is decidable... And Neel's answer settles the general case: if P is an (inhabited) infinite type (which includes some types of Propositions if no extra axioms are included), then the implication fails to hold for $P\rightarrow P$. – cody Dec 11 '14 at 17:05

## 1 Answer

As Neel points out if you work under the "propositions are types" then you can easily come up with a type whose equality cannot be shown decidable (but it is of course consistent to assume that all types have decidable equality), such as $\mathbb{N} \to \mathbb{N}$.

If we understand "proposition" as a more restricted kind of type, then the answer depends on what precisely we mean. If you are working in the calculus of constructions with a Prop kind then you still cannot show that decidable propositions have decidable equality. This is so because it is consistent in the calculus of constructions to equate Prop with a proof-relevant type universe, so for all you know Prop might contains something like $\mathbb{N} \to \mathbb{N}$. This also implies you cannot prove your theorem for Coq's notion of Prop.

But in any case, the best answer comes from homotopy type theory. There a proposition is a type $P$ which satisfies $$\forall x, y : P \,.\, x = y.$$ That is, a proposition has at most one element (as it should if it is to be understood as a proof-irrelevant truth value). In this case the answer is of course positive because the definition of proposition immediately implies that its equality is decidable.

I am curious to know what you mean by "proposition".

• How would you have $\mathbb{N} \rightarrow \mathbb{N}$ inside Prop? Thanks! – Adam Barak Dec 11 '14 at 20:16
• There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there? – Andrej Bauer Dec 11 '14 at 22:37
• The confusion here is about what is meant by "the coq system". If it is "the calculus of constructions", then $\mathtt{Prop=Set=Type}$. If the more accurate "Calculus of Inductive Constructions with 1 Impredicative Universe" then $\mathtt{Type}$ is meaningless without universe level annotations. As far as I know, $\mathtt{Type_1=Prop}$ is a consistent axiom (though inconsistent with EM for subtle reasons). – cody Dec 11 '14 at 23:26
• Sure, we have to tack an index onto $\mathtt{Type}$. The point for @AdamBarak to understand is this: because $\mathtt{Prop} = \mathtt{Type}_1$ does not lead to any contradiction in Coq, we can show that something cannot be done in Coq by showing that it would lead to a contradiction if we also had $\mathtt{Prop} = \mathtt{Type}_1$. – Andrej Bauer Dec 11 '14 at 23:33
• Still not quite right, because in Coq we cannot show that functional equivalence is undecidable. The statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is what Martin Escardo calls a constructive taboo: it can be neither proved nor disproved in Coq. So the correct argument is: if $\mathtt{Prop} = \mathtt{Type}_1$ then $\mathbb{N} \to \mathbb{N}$ is a proposition, and the statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is not provable. (Whereas you said: and the statement "equality on $\mathbb{N} \to \mathbb{N}$ is decidable" is false). – Andrej Bauer Dec 12 '14 at 10:35