<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"><<a href="mailto:pumpkingod@gmail.com" target="_blank">pumpkingod@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">No, I'm reasonably sure the first one is not possible to prove. I<br>
think the result in question is called Glivenko'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 <<a href="mailto:d.starosud@gmail.com">d.starosud@gmail.com</a>> wrote:<br>
> 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>
> Thanks in advance for your help!<br>
><br>
> Best regards,<br>
> Dmytro<br>
><br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto: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>
</blockquote></div><br></div>