The Coq mailing list

[Chris Casinghino <ccasin AT cis.upenn.edu>]

Thanks Jonas and Viktor!  It seems both of you reached the answer
"consistent, so long as Set remains predicative" very quickly.  This
is very helpful.

--Chris

On Tue, Jul 2, 2013 at 4:00 PM, Jonas Kaiser 
<jonas.kaiser.it AT gmail.com>
 wrote:
> Hi,
>
> first of all, sorry for not sending this to the whole list at first.
> Secondly I believe that
>
> dit : forall T: Type, T + T -> False
>
> is equivalent to XM and AC.
>
> The 'dit' stands for decidable inhabitance of types in the sense of for each
> type you can obtain either a member or a proof that no such member exists
> (whether one should still call this deciding is of course debatable)
>
> ragards
> Jonas
>
>
> ---------- Forwarded message ----------
> From: Jonas Kaiser 
> <jonas.kaiser.it AT gmail.com>
> Date: 2 July 2013 21:52
> Subject: Re: [Coq-Club] Excluded Middle for Type?
> To: Chris Casinghino 
> <chris.casinghino AT gmail.com>
>
>
> Hi Chris,
>
> afaik it follwos from assuming EM for Prop and the Axiom of Choice (in the
> sense of the Epsilon Library)
>
> cheers
> Jonas
>
>
> On 2 July 2013 21:44, Chris Casinghino 
> <chris.casinghino AT gmail.com>
>  wrote:
>>
>> Hi Adam,
>>
>> Thanks for the quick response.  You're certainly right, and I should
>> have been a little clearer.  I'm interested specifically in logical
>> consistency, and am not concerned about extraction or the fact that
>> the axiom will get in the way of reduction.
>>
>> --Chris
>>
>> > Such an axiom certainly breaks extraction, since it has no natural
>> > computational interpretation, but perhaps you don't care about
>> > extraction.
>> > It also makes Gallina "computation" highly non-computational, which also
>> > might not bother you, depending on the application.  I don't know if
>> > it's
>> > logically consistent.
>
>
>
>
> --
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Jonas Kaiser
> Saarbrücken
>
>
>
> --
> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
> Jonas Kaiser
> Saarbrücken