[Iris-Club] Excluded middle leads to inconsistency

[Aleš Bizjak]

On 03 May 2017, at 10:19:13, Ralf Jung wrote:

> Didn't you use "P * Q -> P /\ Q" to go from "y |-> 0 * not (y |-> 0)" to
> False?  In a linear separation logic, "y |-> 0 * not (y |-> 0)" is
> actually satisfiable.

Wasn't the last step using (in part) the following sequence

y ↦ 0 ⋆ □(¬(y ↦ 0)) ⊢ y ↦ 0 ∧ □(¬(y ↦ 0)) ⊢ ⊥

Which still relies on some form of weakening, albeit a weaker one.

But there are also other properties of the □ which are used and don't seem to be
possible in general (if we relax the upwards-closure). For instance ⊤ ⊢ □⊤ in
the first step, if I am not mistaken.

-- Aleš