[Agda] excluded-middle

[Katsutoshi Itoh]

Thanks all.

I got things below from your advices.

1. std-lib's excluded-middle is NOT excluded middle.
2. excluded middle is invalid in intuitionistic logic
3. double negate elimination is valid in the logic

I've beleave dne and em are the same thing, but 2 and 3 suggest dne
and em are NOT.
And, we couldn't prove the theorem  A∪Aᶜ≈U, could we?

2016-06-21 19:43 GMT+09:00 Martín Hötzel Escardó <m.escardo at cs.bham.ac.uk>:
>
>
> On 21/06/16 08:08, Nils Anders Danielsson wrote:
>>
>> On 2016-06-20 22:57, Martin Escardo wrote:
>>>
>>> [...] but the intuitionistically valid principle that not-not(every
>>> type has an inhabitant or not).
>>
>>
>> Or rather "for every type, not not (this type has an inhabitant or
>> not)".
>
>
> All that glitters is not gold. :-)
>
> Martin



-- 
----
いとう かつとし
cutsea110 at gmail.com