9
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ 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"? $\endgroup$ – Andrej Bauer Dec 11 '14 at 8:13
  • $\begingroup$ Sorry, I meant the hypothesis "$P$ is decidable", i.e. $P \vee \neg P$ $\endgroup$ – Adam Barak Dec 11 '14 at 9:36
  • 2
    $\begingroup$ 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? $\endgroup$ – Neel Krishnaswami Dec 11 '14 at 11:18
  • $\begingroup$ 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). $\endgroup$ – Adam Barak Dec 11 '14 at 16:31
  • $\begingroup$ 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$. $\endgroup$ – cody Dec 11 '14 at 17:05
5
$\begingroup$

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".

$\endgroup$
  • $\begingroup$ How would you have $\mathbb{N} \rightarrow \mathbb{N}$ inside Prop? Thanks! $\endgroup$ – Adam Barak Dec 11 '14 at 20:16
  • $\begingroup$ There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there? $\endgroup$ – Andrej Bauer Dec 11 '14 at 22:37
  • $\begingroup$ 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). $\endgroup$ – cody Dec 11 '14 at 23:26
  • $\begingroup$ 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$. $\endgroup$ – Andrej Bauer Dec 11 '14 at 23:33
  • 1
    $\begingroup$ 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). $\endgroup$ – Andrej Bauer Dec 12 '14 at 10:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.