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

[Arseniy Alekseyev]

The way I convinced myself about ¬¬lem being unprovable was by
noticing that LEM violates parametricity. So if you believe in
parametricity you should be happy not being able to prove ¬¬lem,
thereby keeping your consistency.

I made a topic a while ago about this subject. Can't say I understood
much of the discussion that followed:

https://lists.chalmers.se/pipermail/agda/2012/003916.html


On 12 October 2014 12:05, Dmytro Starosud <d.starosud at gmail.com> wrote:
> Looks really interesting; I will definitely look into it.
>
> But currently it is out of scope of my question. All I need is to
> investigate this inside Agda.
> And In Agda I can prove that you cannot give me such `X` for which `X + not
> X` is *not* inhabited (see `not-In-Agda` below):
>
> ¬¬lem′ : (A : Set) → ¬ ¬ (A ⊎ ¬ A)
> ¬¬lem′ _ ¬lem = ¬lem (inj₂ (¬lem ∘ inj₁))
>
> not-In-Agda : ¬ (Σ Set λ X → ¬ (X ⊎ ¬ X))
> not-In-Agda (X , p) = ¬¬lem′ X p
>
> So, it's not the case in [at least 'standard'] Agda.
> (Or probably I am missing the key essence of your message :-D)
>
> Probably in Agda it is still possible to prove this?
>
> Thanks,
> Dmytro
>
>
> 2014-10-12 12:46 GMT+03:00 Paolo Capriotti <paolo at capriotti.io>:
>>
>> On Sun, Oct 12, 2014 at 8:24 AM, Dmytro Starosud <d.starosud at gmail.com>
>> wrote:
>> > Which models do you mean?
>> > Please share few keywords to google, or links.
>>
>> There are models in which there exists a (small) type `X` such that `X
>> + not X` is *not* inhabited (e.g. any non-boolean Grothendieck topos).
>> In such a model, the type `not ((A : Set) -> A + not A)` is inhabited.
>> It follows that the type corresponding to the statement you want to
>> prove is not.
>>
>> Paolo
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>