The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Well, but given that it is a choice principle, maybe we can conclude (in response to Jonathan’s original question) that it is not really constructive…?

-Eddy

On Oct 2, 2014, at 9:41 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Well, this principle of choice is equivalent to the dependent version of Pierre-Marie's above: [forall A B, (forall x:A, inhabited B) -> inhabited (forall x:A, B)]. I don't think it implies excluded-middle by itself. But it does if you add in quotient types. The non-dependent version, however, seems pretty weak.

On 2 October 2014 18:01, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

Yes, you are right, thanks!

I got the name TTDA from Werner's paper "Sets in Types, Types in Sets", where he has a different axiom that he calls a choice principle.

It also looks like AC_fun in Coq.Logic.ChoiceFacts.

So, then, does this version of choice imply excluded middle? I can't find a proof in the standard library...

Eddy

Sent from my iPhone

> On Oct 1, 2014, at 6:12 PM, Jonathan <jonikelee AT gmail.com> wrote:
>
>> On 10/01/2014 09:01 PM, Eddy Westbrook wrote:
>> 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)).
>
> That looks like Coq.Logic.ClassicalChoice.choice.
>
>>
>> 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
>