<div dir="ltr">Which models do you mean?<div>Please share few keywords to google, or links.</div><div><br></div><div>Thanks!</div></div><div class="gmail_extra"><br><div class="gmail_quote">2014-10-12 0:12 GMT+03:00 Paolo Capriotti <span dir="ltr">&lt;<a href="mailto:paolo@capriotti.io" target="_blank">paolo@capriotti.io</a>&gt;</span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Sat, Oct 11, 2014 at 8:50 PM, Dmytro Starosud &lt;<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>&gt; wrote:<br>
</span><span class="">&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>
<br>
</span>It&#39;s not. There are models where the negation of LEM holds, and<br>
clearly ¬¬lem is false there.<br>
<span class="HOEnZb"><font color="#888888"><br>
Paolo<br>
</font></span></blockquote></div><br></div>