The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

The nondep_AC axiom below is, I think, equivalent to the Type-Theoretic 
Description Axiom (TTDA), which is this:

Definition TTDA : Type :=
  forall (A B : Type) (P : A -> B -> Prop),
    (forall (a : A), exists b, P a b) ->
    (exists f, forall (a : A), P a (f a)).

TTDA has some sort of non-constructive content, in that it, with 
propositional Excluded Middle, allows you to prove informative Excluded 
Middle. I am not what TTDA just by itself allows, however.

-Eddy

On Oct 1, 2014, at 5:29 AM, Pierre-Marie Pédrot 
<pierre-marie.pedrot AT inria.fr>
 wrote:

> On 30/09/2014 22:47, Jonathan wrote:
>> Anyone seen it before?
> 
> It seems instead equivalent to a weak form of a non-dependent axiom of
> choice, rather than to excluded middle :
> 
> Definition nondep_AC := forall A B, (A -> inhabited B) -> inhabited (A
> -> B).
> Definition escape := forall A, inhabited (inhabited A -> A).
> 
> Lemma dir : nondep_AC -> escape.
> Proof.
> intros ac A; apply ac; trivial.
> Qed.
> 
> Lemma rev : escape -> nondep_AC.
> Proof.
> intros esc A B f.
> destruct (esc B) as [g].
> constructor; auto.
> Qed.
> 
> PMP
> 
> 
> 
>