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

[Paolo Capriotti]

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