[Iris-Club] Excluded middle leads to inconsistency

[Aleš Bizjak]

On 03 May 2017, at 10:41:30, Ralf Jung wrote:

> Actually I thought "not P := P -> False", no box involved.

Isn't Derek's P defined as P(x) = □(x ↦ 0 ∨ ¬(x ↦ 0)) = □(x ↦ 0) ∨ □(¬ x ↦ 0)?

-- Aleš