The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I don't think that this is intuitionistically provable when P is not
decidable though.

 

We're drifting in rather theoretical territories, but it turns out that `forall P:nat-Prop, forall n, P n -> exists m, P m /\ (forall p, p < m -> ~ P p)` is equivalent to the excluded middle.

Let A be a proposition and P n be the statement that { x:unit | A } has at most n elements. Clearly P 1 holds. However, if P has a minimal witness, then by case analyses on that minimal witness we can decide whether A\/~A.

Now, on the other hand, `forall n, P n -> exists m, P m /\ (forall p, p < m -> ~ P p)` doesn't implies that `P` is decidable. Take a function s:nat -> bool, and consider `P n` to be the proposition that `exists k>n, s k = true`. P is not decidable (this is Bishop's limited principle of omniscience), however, clearly if `P n` then there exists a minimal such n (namely 0).