Theorem search
  {P : nat -> Prop} (dec : forall n, {P n} + {~P n})
: ~~(exists n, P n) -> {n | P n}.

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.


1 Answer 1


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.

  • 1
    $\begingroup$ Doesn't $P$ need to be decidable for the description lemma? $\endgroup$
    – Couchy
    Commented Apr 25, 2022 at 14:52
  • $\begingroup$ Indeed, you need decidability. I'll fix the answer accordingly. $\endgroup$ Commented Apr 25, 2022 at 21:24
  • $\begingroup$ I believe the description axiom given here is, strictly speaking, constructive indefinite description as it does not include uniqueness of n as a hypothesis. However this is not really important as the natural numbers are well-ordered and so we can always add the constraint that n be minimal among elements satisfying f. $\endgroup$ Commented Feb 17 at 15:44

Your Answer

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

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