The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

You'd probably need to assume the axiom of choice as well, in order to
say anything about whether (forall n:U, P n) is empty or not.
-- 
Daniel Schepler

On Wed, May 14, 2014 at 11:22 AM, 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