The Coq mailing list

[Amin Timany <amintimany AT gmail.com>]

Hmmm,

I just tried and proved it. Just need to define disjunction and excluded middle in Type: 

Inductive T_disj (A B : Type) : Type :=

  | Left : A -> T_disj A B

  | Right : B -> T_disj A B

.

Axiom T_classical : forall X : Type, T_disj X (X -> False).

Lemma not_all_ex_not_pred :

forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) -> exists n : U, P n -> False.

Proof.

  intros U P H.

  destruct (T_classical (exists n : U, P n -> False)) as [H1|H1].

  assumption.

  exfalso; apply H.

  intros n.

  destruct (T_classical (P n)) as [H3 | H3].

  assumption.

  exfalso; apply H1.

  exists n; exact H3.

Qed.

On 14 May 2014, at 21:30, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

If you make your existential quantifier "constructive" too,  your lemma is unprovable

More precisely, the following is unprovable:

Lemma GMarkov :

forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) 

-> sigT (fun n => P n -> False).

If you don't care about the version above, you can skip the rest of this email.

The Markov principle can be viewed as a special case of GMarkov above where U is nat, and P is decidable

http://en.wikipedia.org/wiki/Markov's_principle.

Informally, an unbounded search over numbers can serve an a witness of the Markov principle, i.e.

check P 0 , then check P 1 and so on. Classical reasoning can guarantee that such a search would terminate.

However, Coq does not allow such classical termination arguments (unless you add axioms).

The unprovability of the Markov principle implies the unprovability of GMarkov above.

Intuitively there are even more difficulties in coming up with a realizer for the Lemma GMarkov above:

Firstly, you are not assuming that P is decidable.

Moreover, U is an arbitrary type (unlike nat) and given an arbitrary type and no other information about it you cannot enumerate

or even cook up its elements (in order to do an unbounded search). The two hypotheses do not seem to provide any computationally

usable information.

Regards,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, May 14, 2014 at 2:22 PM, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

All,

The library Coq.Logic.Classical_Pred_Type gives a proof, using (propositional) excluded middle, that the negation of a forall is an exists:

Lemma not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.

Does anyone know if the version of this that makes P predicative, using Type, is provable as well? That is, I am trying to prove:

Lemma not_all_ex_not_pred :
 forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) -> exists n : U, P n -> False.

Thanks,
-Eddy