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

Improve this question
$\endgroup$
6
  • 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
    Commented Dec 11, 2014 at 8:13
  • $\begingroup$ Sorry, I meant the hypothesis "$P$ is decidable", i.e. $P \vee \neg P$ $\endgroup$
    – Adam Barak
    Commented Dec 11, 2014 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
    Commented Dec 11, 2014 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
    Commented Dec 11, 2014 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
    Commented Dec 11, 2014 at 17:05

1 Answer 1

Reset to default
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".

Improve this answer
$\endgroup$
13
  • $\begingroup$ How would you have $\mathbb{N} \rightarrow \mathbb{N}$ inside Prop? Thanks! $\endgroup$
    – Adam Barak
    Commented Dec 11, 2014 at 20:16
  • $\begingroup$ There is nothing in the calculus of construction that prevents $\mathtt{Prop} = \mathtt{Type}$, is there? $\endgroup$
    – Andrej Bauer
    Commented Dec 11, 2014 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
    Commented Dec 11, 2014 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
    Commented Dec 11, 2014 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
    Commented Dec 12, 2014 at 10:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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