<div dir="ltr">Thanks a lot Daniel,<div>Will have a look at that theorem.</div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-11 23:56 GMT+03:00 Daniel Peebles <span dir="ltr">&lt;<a href="mailto:pumpkingod@gmail.com" target="_blank">pumpkingod@gmail.com</a>&gt;</span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">No, I&#39;m reasonably sure the first one is not possible to prove. I<br>
think the result in question is called Glivenko&#39;s theorem, and that it<br>
only works if the quantifier is outside the negation.<br>
<div><div class="h5"><br>
On Sat, Oct 11, 2014 at 3:50 PM, Dmytro Starosud &lt;<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>&gt; wrote:<br>
&gt; Hello everyone<br>
&gt;<br>
&gt; Could you have a look at my problem below?<br>
&gt; I am trying to prove something that looks like just better double negation<br>
&gt; of law of excluded middle:<br>
&gt;<br>
&gt; ¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)<br>
&gt; ¬¬lem = _<br>
&gt;<br>
&gt; Which I cannot prove, whereas following one is pretty easy to prove:<br>
&gt;<br>
&gt; ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)<br>
&gt; ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))<br>
&gt;<br>
&gt; Is it actually possible to prove the first one in constructive logic (in<br>
&gt; particular in Agda)?<br>
&gt;<br>
&gt; Thanks in advance for your help!<br>
&gt;<br>
&gt; Best regards,<br>
&gt; Dmytro<br>
&gt;<br>
&gt;<br>
</div></div>&gt; _______________________________________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
&gt;<br>
</blockquote></div><br></div>