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

[Daniel Peebles]

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
>