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

[Dmytro Starosud]

Which models do you mean?
Please share few keywords to google, or links.

Thanks!

2014-10-12 0:12 GMT+03:00 Paolo Capriotti <paolo at capriotti.io>:

> On Sat, Oct 11, 2014 at 8: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)?
>
> It's not. There are models where the negation of LEM holds, and
> clearly ¬¬lem is false there.
>
> Paolo
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141012/abbe3dee/attachment.html