I define the following axiom.

(First, I want to prove it, and make it Theorem. However, I can not find how to start.)

Axiom functions_eq_or_not :
forall f g : (Q -> bool), 
(forall q : Q, f q = g q) \/ (exists q : Q, f q <> g q).

Can I prove it (without using excluded middle) and make it Theorem?


1 Answer 1


When Q is nat your principle is equivalent to LPO, which is not provable in intuitionistic logic.

Martín Escardó extensively studied for which Q the principle holds, see for example Exhaustible sets in higher-type computation and Infinite sets that admit fast exhaustive search.


Your Answer

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

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