The Coq mailing list

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

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.

Actually, I was mistaken: on the weak excluded middle `forall A, ~~A\/~A` can be deduced from my proof. But I found an actual proof of the principle of excluded middle which is even simpler.

Take `P n` to be `(n=0/\~A)\/(n=1/\A)\/(n=2)`. Then, by definition `P 2` holds, `P 0` is equivalent to `~A` and `P 1` is equivalent to `A`. A minimal witness of P cannot be greater than 1, otherwise `P 0` and `P 1` are false which means `~~A/\~A` holds, which is contradictory. Therefore a minimal witness of P, if it exists must be 0 or 1, hence existence of a minimal witness entails `P 0 \/ P 1` which is equivalent to `A \/ ~A`.