[Agda] excluded-middle

[Owen]

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
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3396>
: ∀ {p <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3417>}
{P <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421>
: Set p <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3417>}
→ ¬ <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398>
¬ <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398>
Dec <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468>
P <http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421>

Intuitively you could read Dec
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468>
 P
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421>
as
"a proof that P is decidable", ¬
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#398>
 Dec
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Core.html#468>
 P
<http://www.cse.chalmers.se/~nad/listings/lib/Relation.Nullary.Negation.html#3421>
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 <javascript:;> on
> behalf of Nils Anders Danielsson" <agda-bounces at lists.chalmers.se
> <javascript:;> on behalf of nad at cse.gu.se <javascript:;>> 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 <javascript:;>
> >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.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160622/b0646616/attachment.html