<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"><<a href="mailto:paolo@capriotti.io" target="_blank">paolo@capriotti.io</a>></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 <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>> wrote:<br>
</span><span class="">> Hello everyone<br>
><br>
> Could you have a look at my problem below?<br>
> I am trying to prove something that looks like just better double negation<br>
> of law of excluded middle:<br>
><br>
> ¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)<br>
> ¬¬lem = _<br>
><br>
> Which I cannot prove, whereas following one is pretty easy to prove:<br>
><br>
> ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)<br>
> ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))<br>
><br>
> Is it actually possible to prove the first one in constructive logic (in<br>
> particular in Agda)?<br>
<br>
</span>It'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>