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
Theorem search
{P : nat -> Prop} (dec : forall n, {P n} + {~P n})
: ~~(exists n, P n) -> {n | P n}.
Admitted.
I don't think this is provable in Coq without additional axioms, and it is provable when assuming LEM : forall A : Prop, A \/ ~A. However, I don't think it proves LEM. What are the weakest axioms that prove search? I'm not very familiar with all the versions of the axiom of choice, but I guess this is probably equivalent to one.
This is an axiom in itself, known as Markov's principle. A more compact but equivalent way to state this axiom is
Axiom MP : forall (f : nat -> bool), ~~ (exists n, f n = true) -> exists n, f n = true.
The original phrasing of the question hardwires a bit of choice that is provable in CIC, known as constructive definite description.
Lemma description : forall (f : nat -> bool), (exists n, f n = true) -> {n | f n = true}.
This theorem is a consequence of singleton elimination.
Markov principle is not provable in CIC, but it enjoys a special status amongst semi-classical principles. As already observed, it is a consequence of classical logic in Prop. As such it does not endanger the computational properties of extraction. Even better, you can actually natively extend CIC with it without breaking strong normalization and canonicity. See for instance this other question for more details.
