The Coq mailing list

[Jonas Kaiser <jonas.kaiser.it AT gmail.com>]

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