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
|
1 Answer
$\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$– srghmaSep 5, 2019 at 9:11
-
1$\begingroup$ @srghma no, the same thing holds for Coq. Consistency with LEM (classical logic) is a common expected feature in proof assistants. $\endgroup$ Sep 5, 2019 at 17:47