[Agda] (Stronger) double negation of law of excluded middle

[Dmytro Starosud]

Thanks a lot Daniel,
Will have a look at that theorem.

2014-10-11 23:56 GMT+03:00 Daniel Peebles <pumpkingod at gmail.com>:

> No, I'm reasonably sure the first one is not possible to prove. I
> think the result in question is called Glivenko's theorem, and that it
> only works if the quantifier is outside the negation.
>
> On Sat, Oct 11, 2014 at 3:50 PM, Dmytro Starosud <d.starosud at gmail.com>
> wrote:
> > Hello everyone
> >
> > Could you have a look at my problem below?
> > I am trying to prove something that looks like just better double
> negation
> > of law of excluded middle:
> >
> > ¬¬lem : ¬ ¬ ((A : Set) → A ⊎ ¬ A)
> > ¬¬lem = _
> >
> > Which I cannot prove, whereas following one is pretty easy to prove:
> >
> > ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
> > ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))
> >
> > Is it actually possible to prove the first one in constructive logic (in
> > particular in Agda)?
> >
> > Thanks in advance for your help!
> >
> > Best regards,
> > Dmytro
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141012/6d3401cf/attachment.html