Library Coq.Logic.Classical_Pred_Type



Classical Predicate Logic on Type

Require Import Classical_Prop.

Section Generic.
Variable U : Type.

de Morgan laws for quantifiers

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

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

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

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

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

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

End Generic.