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

[Paolo Capriotti]

On Tue, Oct 14, 2014 at 10:43 AM, Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> 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.

But the question was about the double negation of LEM, not LEM itself.
With two worlds, the double negation of LEM is true, hence that is not
a sufficient counterexample. It seems to me that you need infinitely
many worlds to construct a counterexample, and in particular ω seems
to work.

Paolo