5
$\begingroup$

Can one create such function in Agda ?

ℕ→ℕ-undecidable : ¬ ( (f g :  ℕ → ℕ ) → Dec (f ≡ g)) 
ℕ→ℕ-undecidable = ?

I am particularly interested in proof using cubical Agda.

|cite|improve this question
$\endgroup$
7
$\begingroup$

ℕ→ℕ-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.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ What about coq? Is it possible to prove it there? $\endgroup$ – srghma Sep 5 at 9:11
  • $\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 Sep 5 at 17:47

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.