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

[Dmytro Starosud]

Btw, I was trying to look into this, but there is something missing with it:

isProp : Set → Set
isProp = _

PROP = ∃ λ A → isProp A

prop : ¬ ¬ ((A : PROP) → A ⊎ ¬ A)
prop = _

Agda doesn't want type check type of little prop
_⊎_ expects types as an arguments and negation expects type as an argument
but A is of type PROP and thus is not type, but term.

Could you clarify what you meant to write? (unfortunately I failed to
recover original meaning)

Thanks in advance,
Dima


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

> On Sun, Oct 12, 2014 at 12:05 PM, 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)
>
> Well, I wrote that `X` is such that `X + not X` is not inhabited, but
> that doesn't mean that `not (X + not X)` is inhabited, so there's no
> contradiction here.
>
> Nevertheless, I realised that what I wrote is incorrect. The negation
> of LEM is not (globally) true in the topos I was thinking about, so
> the statement you want to prove actually holds there. Sorry about
> that.
>
> It is still true that the statement is unprovable, but the argument
> needs to be a bit subtler. For example, Corollary 3.2.7 in the HoTT
> book (http://homotopytypetheory.org/book/) shows that any model of
> type theory compatible with univalence falsifies the statement.
>
> That raises a further question: is the statement
>
>     not not ((A : Prop) -> A + not A)
>
> provable (where Prop = Σ (A : Set) . isProp(A))?
>
> Paolo
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141014/a9359886/attachment.html