[Agda] excluded-middle

[Katsutoshi Itoh]

> The standard library module Relation.Nullary.Negation contains proofs
> showing that excluded middle and double-negation elimination are
> logically equivalent.

sounds good.


> intuitively you could read Dec P as "a proof that P is
(snip)
> So you can see intuitively these mean different things.

Thanks for the easy-to-understand explanation.


> Excluded middle should only apply to propositions, where a proposition is > a type with at most one inhabitant.
>
> Otherwise it is much stronger because it chooses an element in each
> inhabited set and incompatible with univalence (I think).

Please teach me a little more detail.
I do not think I have read exactly the meaning.


Regards.


2016-06-22 21:07 GMT+09:00 Owen <ellbur at gmail.com>:
> Hello Katsutoshi,
>
> What makes 'excluded-middle' in Data.Relation.Nullary valid is not just that
> it is double negated, but that the quantifier is in a different place. Look
> at the type definition:
>
> excluded-middle : ∀ {p} {P : Set p} → ¬ ¬ Dec P
>
> Intuitively you could read Dec P as "a proof that P is decidable", ¬ Dec P
> as "a proof that P is not decidable", so the whole thing reads as:
>
>    "For all sentences P, it is not possible to prove that P is not
> decidable"
>
> Compare to the excluded middle which says
>
>    "For all sentences P, P is decidable"
>
> So you can see intuitively these mean different things.
>
> Best,
> Owen
>
> On Wednesday, June 22, 2016, Thorsten Altenkirch
> <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
>>
>> Excluded middle should only apply to propositions, where a proposition is
>> a type with at most one inhabitant.
>>
>> Otherwise it is much stronger because it chooses an element in each
>> inhabited set and incompatible with univalence (I think).
>>
>> Thorsten
>>
>>
>>
>> On 22/06/2016, 09:10, "agda-bounces at lists.chalmers.se on behalf of Nils
>> Anders Danielsson" <agda-bounces at lists.chalmers.se on behalf of
>> nad at cse.gu.se> wrote:
>>
>> >On 2016-06-22 03:59, Katsutoshi Itoh wrote:
>> >> 3. double negate elimination is valid in the logic
>> >
>> >No, it's not.
>> >
>> >> I've beleave dne and em are the same thing, but 2 and 3 suggest dne
>> >> and em are NOT.
>> >
>> >The standard library module Relation.Nullary.Negation contains proofs
>> >showing that excluded middle and double-negation elimination are
>> >logically equivalent.
>> >
>> >--
>> >/NAD
>> >_______________________________________________
>> >Agda mailing list
>> >Agda at lists.chalmers.se
>> >https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>>
>> This message and any attachment are intended solely for the addressee
>> and may contain confidential information. If you have received this
>> message in error, please send it back to me, and immediately delete it.
>>
>> Please do not use, copy or disclose the information contained in this
>> message or in any attachment.  Any views or opinions expressed by the
>> author of this email do not necessarily reflect the views of the
>> University of Nottingham.
>>
>> This message has been checked for viruses but the contents of an
>> attachment may still contain software viruses which could damage your
>> computer system, you are advised to perform your own checks. Email
>> communications with the University of Nottingham may be monitored as
>> permitted by UK legislation.
>>
>



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