9
$\begingroup$
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.

$\endgroup$

1 Answer 1

11
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ Doesn't $P$ need to be decidable for the description lemma? $\endgroup$
    – Couchy
    Apr 25 at 14:52
  • $\begingroup$ Indeed, you need decidability. I'll fix the answer accordingly. $\endgroup$ Apr 25 at 21:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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