[Iris-Club] Excluded middle leads to inconsistency

[Ralf Jung]

Hi,

>> 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.

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

; Ralf