<p>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}$.</p>

<p>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 <code>Prop</code> 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 <code>Prop</code> with a proof-relevant type universe, so for all you know <code>Prop</code> might contains something like $\mathbb{N} \to \mathbb{N}$. This also implies you cannot prove your theorem for Coq's notion of <code>Prop</code>.</p>

<p>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.</p>

<p>I am curious to know what you mean by "proposition".</p>

CC BY-SA 3.0
2014-12-11T20:16:48.673Z
How would you have $\mathbb{N} \rightarrow \mathbb{N}$ inside `Prop`? Thanks!
Adam Barak
CC BY-SA 3.0
2014-12-11T22:37:34.523Z
There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there?
Andrej Bauer
CC BY-SA 3.0
2014-12-11T23:26:24.263Z
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
CC BY-SA 3.0
2014-12-11T23:33:41.823Z
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
CC BY-SA 3.0
2014-12-12T00:45:49.567Z
I see, so, 

$$(\texttt{Prop} = \texttt{Type}_1 \wedge \texttt{hypothesis} (\mathbb{N} \rightarrow \mathbb{N})) \Rightarrow
\texttt{False}
 $$

because functional equivalence is undecidable.
Since it is known that $\texttt{Prop} = \texttt{Type}_1$ is consistent, it must be that the $\texttt{hypothesis}$ is wrong.  ($\texttt{hypothesis}$ is the proposition in the question).

Thanks!
Adam Barak
CC BY-SA 3.0
2014-12-12T10:35:23.613Z
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
CC BY-SA 3.0
2014-12-12T21:51:37.393Z
So is "equality on $\mathbb{N} \rightarrow \mathbb{N}$ is decidable" not provable even when $\texttt{Prop} = \texttt{Type}_1$, not just in Coq? 

(There seems to be two things which I still have to find/look for proofs of: "$\texttt{Prop} = \texttt{Type}$ is consistent in Coq" and "equality on $\mathbb{N} \rightarrow \mathbb{N}$ is decidable" is unprovable in Coq + $\texttt{Prop} = \texttt{Type}$)
Adam Barak
CC BY-SA 3.0
2014-12-12T22:15:20.730Z
Actually, since we're doing this for Coq, we should probably consider $\mathsf{Prop} = \mathsf{Set}$. If you look at the rules (https://coq.inria.fr/doc/Reference-Manual006.html) and change $\mathsf{Prop}$ to $\mathsf{Set}$ everything, does anything strange happen, or do you just get Coq without $\mathsf{Prop}$?
Andrej Bauer
CC BY-SA 3.0
2014-12-12T22:20:42.793Z
The product rules are weird if we do that because they cause $\mathsf{Set}$ to be impredicative (but fortunately that is consistent). Let's ignore the inductive stuff, that'll be complicated and there is the pesky "singleton elimination". Hmm. Maybe there is a simpler way to see that there are elements in `Prop` for which we cannot establish decidability of equality.
Andrej Bauer
CC BY-SA 3.0
2014-12-13T03:26:08.400Z
Isn't the hypothesis *somewhat* equivalent to "syntactic equivalence of functions whose range is `bool` and produces the same answer is undecidable"?
Adam Barak
CC BY-SA 3.0
2014-12-13T07:19:53.757Z
What's your point?
Andrej Bauer
CC BY-SA 3.0
2014-12-15T05:23:18.407Z
I do not "intuitively" see why syntactic equality of such functions is undecidable. I think it boils down to finding (as you stated), a simpler way to see that there are elements in `Prop` for which we cannot establish decidability of equality of its proofs, even though the equality of the elements is decidable. Thanks for the discussion! I think I have gotten lots of leads.
Adam Barak
CC BY-SA 3.0
2014-12-15T08:11:04.523Z
By the way, just one more comment: you should look for an inhabited propostion $P$ such that its equality is not decidable. For if $P$ is decidable and has non-decidable equality, then $P$ holds, since $\lnot P$ implies that $P$ has decidable equality.
Andrej Bauer
CC BY-SA 3.0
2014-12-11T18:48:23.007Z
2014-12-11T18:48:23.007Z
Andrej Bauer
<p>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.</p>

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

<p>$$\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\})
$$</p>

<p>Thanks!</p>

<p>Edited to correct the error:
Edit 2 to make <code>Prop</code> more explicit</p>

CC BY-SA 3.0
2014-12-11T08:13:57.303Z
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
CC BY-SA 3.0
2014-12-11T09:36:34.730Z
Sorry, I meant the hypothesis "$P$ is decidable", i.e. $P \vee \neg P$
Adam Barak
CC BY-SA 3.0
2014-12-11T11:18:36.080Z
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
CC BY-SA 3.0
2014-12-11T16:31:05.013Z
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
CC BY-SA 3.0
2014-12-11T17:05:18.973Z
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
CC BY-SA 3.0
2014-12-11T20:11:23.277Z
I mean Coq's `Prop` when I say Proposition. Thanks!
Adam Barak
<coq><constructive-mathematics><calculus-of-constructions>
Equality of decidable proofs?
Adam Barak
# Equality of decidable proofs?

(Asked by: username_0 on 2014-12-11)

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

**Tags:** coq, constructive-mathematics, calculus-of-constructions

> **Comments:**
> **username_1**: 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"?  
> **username_0**: Sorry, I meant the hypothesis "$P$ is decidable", i.e. $P \vee \neg P$  
> **username_2**: 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?  
> **username_0**: 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).  
> **username_3**: 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$.  
> **username_0**: I mean Coq's `Prop` when I say Proposition. Thanks!  

---

## 1 answers

### Answer by username_1 on 2014-12-11. Score: 5 | Accepted 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".

> **Comments:**
> **username_0**: How would you have $\mathbb{N} \rightarrow \mathbb{N}$ inside `Prop`? Thanks!  
> **username_1**: There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there?  
> **username_3**: 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).  
> **username_1**: 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$.  
> **username_0**: I see, so,   $$(\texttt{Prop} = \texttt{Type}_1 \wedge \texttt{hypothesis} (\mathbb{N} \rightarrow \mathbb{N})) \Rightarrow \texttt{False}  $$  because functional equivalence is undecidable. Since it is known that $\texttt{Prop} = \texttt{Type}_1$ is consistent, it must be that the $\texttt{hypothesis}$ is wrong.  ($\texttt{hypothesis}$ is the proposition in the question).  Thanks!  
> **username_1**: 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).  
> **username_0**: So is "equality on $\mathbb{N} \rightarrow \mathbb{N}$ is decidable" not provable even when $\texttt{Prop} = \texttt{Type}_1$, not just in Coq?   (There seems to be two things which I still have to find/look for proofs of: "$\texttt{Prop} = \texttt{Type}$ is consistent in Coq" and "equality on $\mathbb{N} \rightarrow \mathbb{N}$ is decidable" is unprovable in Coq + $\texttt{Prop} = \texttt{Type}$)  
> **username_1**: Actually, since we're doing this for Coq, we should probably consider $\mathsf{Prop} = \mathsf{Set}$. If you look at the rules (https://coq.inria.fr/doc/Reference-Manual006.html) and change $\mathsf{Prop}$ to $\mathsf{Set}$ everything, does anything strange happen, or do you just get Coq without $\mathsf{Prop}$?  
> **username_1**: The product rules are weird if we do that because they cause $\mathsf{Set}$ to be impredicative (but fortunately that is consistent). Let's ignore the inductive stuff, that'll be complicated and there is the pesky "singleton elimination". Hmm. Maybe there is a simpler way to see that there are elements in `Prop` for which we cannot establish decidability of equality.  
> **username_0**: Isn't the hypothesis *somewhat* equivalent to "syntactic equivalence of functions whose range is `bool` and produces the same answer is undecidable"?  
> **username_1**: What's your point?  
> **username_0**: I do not "intuitively" see why syntactic equality of such functions is undecidable. I think it boils down to finding (as you stated), a simpler way to see that there are elements in `Prop` for which we cannot establish decidability of equality of its proofs, even though the equality of the elements is decidable. Thanks for the discussion! I think I have gotten lots of leads.  
> **username_1**: By the way, just one more comment: you should look for an inhabited propostion $P$ such that its equality is not decidable. For if $P$ is decidable and has non-decidable equality, then $P$ holds, since $\lnot P$ implies that $P$ has decidable equality.  

---

