Hello Katsutoshi,<div><br></div><div>What makes 'excluded-middle' in Data.Relation.Nullary valid is not just that it is double negated, but that the quantifier is in a different place. Look at the type definition:</div><div><pre><font color="#000000" face="Helvetica Neue, Helvetica, Arial, sans-serif" size="3"><span style="white-space:normal;background-color:rgba(255,255,255,0)"><a name="3396" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3396" class="Function">excluded-middle</a><a name="3411"> </a><a name="3412" class="Symbol">:</a><a name="3413"> </a><a name="3414" class="Symbol">∀</a><a name="3415"> </a><a name="3416" class="Symbol">{</a><a name="3417" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3417" class="Bound">p</a><a name="3418" class="Symbol">}</a><a name="3419"> </a><a name="3420" class="Symbol">{</a><a name="3421" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421" class="Bound">P</a><a name="3422"> </a><a name="3423" class="Symbol">:</a><a name="3424"> </a><a name="3425" class="PrimitiveType">Set</a><a name="3428"> </a><a name="3429" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3417" class="Bound">p</a><a name="3430" class="Symbol">}</a><a name="3431"> </a><a name="3432" class="Symbol">→</a><a name="3433"> </a><a name="3434" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398" class="Function Operator">¬</a><a name="3435"> </a><a name="3436" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398" class="Function Operator">¬</a><a name="3437"> </a><a name="3438" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468" class="Datatype">Dec</a><a name="3441"> </a><a name="3442" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421" class="Bound">P</a></span></font></pre></div>Intuitively you could read <font color="#000000" size="2"><span style="background-color:rgba(255,255,255,0)"><a name="3438" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468" class="Datatype">Dec</a><a name="3441"> </a><a name="3442" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421" class="Bound">P</a></span></font> as "a proof that P is decidable", <font color="#000000" size="2"><span style="background-color:rgba(255,255,255,0)"><a name="3436" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398" class="Function Operator">¬</a><a name="3437"> </a><a name="3438" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468" class="Datatype">Dec</a><a name="3441"> </a><a name="3442" href="http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421" class="Bound">P</a></span></font> as "a proof that P is not decidable", so the whole thing reads as:<br><div><br></div><div> "For all sentences P, it is not possible to prove that P is not decidable"</div><div><br></div><div>Compare to the excluded middle which says</div><div><br></div><div> "For all sentences P, P is decidable"</div><div><br></div><div>So you can see intuitively these mean different things.<br><div><br></div><div>Best,</div><div>Owen</div><div><br>On Wednesday, June 22, 2016, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Excluded middle should only apply to propositions, where a proposition is a type with at most one inhabitant.<br>
<br>
Otherwise it is much stronger because it chooses an element in each inhabited set and incompatible with univalence (I think).<br>
<br>
Thorsten<br>
<br>
<br>
<br>
On 22/06/2016, 09:10, "<a href="javascript:;" onclick="_e(event, 'cvml', 'agda-bounces@lists.chalmers.se')">agda-bounces@lists.chalmers.se</a> on behalf of Nils Anders Danielsson" <<a href="javascript:;" onclick="_e(event, 'cvml', 'agda-bounces@lists.chalmers.se')">agda-bounces@lists.chalmers.se</a> on behalf of <a href="javascript:;" onclick="_e(event, 'cvml', 'nad@cse.gu.se')">nad@cse.gu.se</a>> wrote:<br>
<br>
>On 2016-06-22 03:59, Katsutoshi Itoh wrote:<br>
>> 3. double negate elimination is valid in the logic<br>
><br>
>No, it's not.<br>
><br>
>> I've beleave dne and em are the same thing, but 2 and 3 suggest dne<br>
>> and em are NOT.<br>
><br>
>The standard library module Relation.Nullary.Negation contains proofs<br>
>showing that excluded middle and double-negation elimination are<br>
>logically equivalent.<br>
><br>
>--<br>
>/NAD<br>
>_______________________________________________<br>
>Agda mailing list<br>
><a href="javascript:;" onclick="_e(event, 'cvml', 'Agda@lists.chalmers.se')">Agda@lists.chalmers.se</a><br>
><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please send it back to me, and immediately delete it.<br>
<br>
Please do not use, copy or disclose the information contained in this<br>
message or in any attachment. Any views or opinions expressed by the<br>
author of this email do not necessarily reflect the views of the<br>
University of Nottingham.<br>
<br>
This message has been checked for viruses but the contents of an<br>
attachment may still contain software viruses which could damage your<br>
computer system, you are advised to perform your own checks. Email<br>
communications with the University of Nottingham may be monitored as<br>
permitted by UK legislation.<br>
<br>
</blockquote></div></div>