Can one create such function in Agda ?
ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g))
ℕ→ℕ-undecidable = ?
I am particularly interested in proof using cubical Agda.
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
2
ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda.
-
$\begingroup$ What about coq? Is it possible to prove it there? $\endgroup$srghma– srghma2019-09-05 09:11:32 +00:00Commented Sep 5, 2019 at 9:11
-
2$\begingroup$ @srghma no, the same thing holds for Coq. Consistency with LEM (classical logic) is a common expected feature in proof assistants. $\endgroup$András Kovács– András Kovács2019-09-05 17:47:05 +00:00Commented Sep 5, 2019 at 17:47
$\begingroup$
$\endgroup$
2
The flag --injective-type-constructors makes Agda anti-classical. The proof of this can be seen here. See also this question on the Proof Assitants StackExchange.
-
$\begingroup$ I think you misinterpreted the question as talking about the type of types, but it is actually talking about a specific type. $\endgroup$Trebor– Trebor2024-08-29 10:02:44 +00:00Commented Aug 29, 2024 at 10:02
-
$\begingroup$ @Trebor oh, right, the title talks about decidable equality in general, while the text is specifically about natural numbers $\endgroup$Hjulle– Hjulle2024-08-30 05:40:49 +00:00Commented Aug 30, 2024 at 5:40