Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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?
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.
