# Can I prove this axiom without using excluded-middle property?

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

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.