The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Daniel,

This is great, thanks! Putting this in with the other pieces I already have, 
it looks like the following are equivalent, assuming propositional excluded 
middle:

Predicative Excluded Middle
Choice
The Type-Theoretic Description Axiom
Strong Sums (of the form given in a previous email on this list)
not_all_ex_not_pred


Note that the story is a bit more complicated if you want to restrict the 
universe levels of these things; e.g., TTDA at level i+1 implies Predicative 
Excluded Middle at level i, which implies TTDA at level i.

It seems reasonable to assume that none of these are implied by just 
propositional excluded middle by itself. At least, in (classical) ZF set 
theory, we know that choice is independent of the rest of the theory. So I 
can stop looking… :)

Thanks again,
-Eddy


On May 14, 2014, at 12:58 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:

> And here's a proof that not_all_ex_not_pred is equivalent to the axiom
> of choice, modulo propositional excluded middle:
> 
> Require Import Classical.
> 
> Definition choice := forall (A B:Type) (R:A->B->Prop),
>  (forall x:A, exists y:B, R x y) ->
>  exists f:A->B, forall x:A, R x (f x).
> 
> Definition dep_type_choice := forall (A:Type) (B:A->Type),
>  (forall x:A, inhabited (B x)) ->
>  inhabited (forall x:A, B x).
> 
> Lemma dep_type_choice_impl_choice :
>  dep_type_choice -> choice.
> Proof.
> intros ? A B R ?.
> pose proof (H A (fun x:A => { y:B | R x y })).
> refine (let _ := H1 _ in _).
> intros.
> destruct (H0 x) as [y].
> constructor.
> exists y; trivial.
> 
> destruct _H as [f].
> exists (fun x:A => proj1_sig (f x)).
> intros; apply proj2_sig.
> Qed.
> 
> Lemma choice_impl_dep_type_choice :
>  choice -> dep_type_choice.
> Proof.
> intros ? A B ?.
> set (B' := sigT B).
> set (R := fun (x:A) (y:B') => projT1 y = x).
> pose proof (H A B' R).
> refine (let _ := H1 _ in _).
> intros.
> destruct (H0 x) as [y].
> exists (existT B x y).
> reflexivity.
> 
> destruct _H as [f].
> constructor.
> exact (fun x:A => eq_rect _ _ (projT2 (f x)) _ (H2 x)).
> Qed.
> 
> Ltac suppose_not := apply NNPP; intro.
> 
> Lemma not_all_ex_not :
> forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P 
> n.
> Proof.
> intros.
> suppose_not.
> contradict H.
> intros.
> suppose_not.
> contradict H0.
> eauto.
> Qed.
> 
> Definition not_all_ex_not_pred :=
> forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) ->
> exists n : U, P n -> False.
> 
> Lemma not_all_ex_not_pred_impl_dep_type_choice :
>  not_all_ex_not_pred -> dep_type_choice.
> Proof.
> intros ? A B ?.
> suppose_not.
> pose proof (H A B).
> refine (let _ := H2 _ in _).
> intros.
> contradict H1.
> eauto.
> destruct (_H) as [x].
> destruct (H0 x) as [y].
> auto.
> Qed.
> 
> Lemma dep_type_choice_impl_not_all_ex_not_pred :
>  dep_type_choice -> not_all_ex_not_pred.
> Proof.
> intros ? U P ?.
> suppose_not.
> assert (inhabited (forall n:U, P n)).
> apply H.
> intros.
> suppose_not.
> contradict H1.
> exists x.
> intros; contradict H2.
> auto.
> 
> destruct H2 as [f].
> auto.
> Qed.
> -- 
> Daniel Schepler
> 
> On Wed, May 14, 2014 at 12:27 PM, Daniel Schepler 
> <dschepler AT gmail.com>
>  wrote:
>> 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