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

[Thorsten Altenkirch]

Indeed in the case of Prop this is just Kripke’s semantics, that is
propositions are modelled as monotone functions from a preordered set of
worlds to a subset of atomic propositions written as w ||- P (w forces P).
Now w ||- ~P if P is not forced in any future of w. \/ is interpreted
pointwise w ||- P \/ Q iff w ||- P or w ||- Q. To construct a
counterexample to excluded middle you need just 2 worlds w0 <= w1 where
only w1 ||- P. Now w0 doesn’t force P and it doesn’t force ~P hence it
doesn’t force P \/ ~P.

T.

On 12/10/2014 15:10, "Paolo Capriotti" <paolo at capriotti.io> wrote:

>On Sun, Oct 12, 2014 at 1:20 PM, Paolo Capriotti <paolo at capriotti.io>
>wrote:
>>
>> That raises a further question: is the statement
>>
>>     not not ((A : Prop) -> A + not A)
>>
>> provable (where Prop = Σ (A : Set) . isProp(A))?
>
>The answer should be no again. I think it suffices to look at the
>copresheaf category Set^ω. There, if I'm not mistaken, the type
>corresponding to "propositional" LEM is not just uninhabited, but
>globally 0.  Therefore its double negation is 0 as well.
>
>Paolo
>_______________________________________________
>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.