[Iris-Club] Excluded middle leads to inconsistency

Aleš Bizjak abizjak at cs.au.dk
Wed May 3 10:57:08 CEST 2017

On 03 May 2017, at 10:47:51, Derek Dreyer wrote:

> You could replace the True at the beginning with emp.

Ah yes, then you just need emp ⊢ □True, which should be a valid property if we
want a sensible box.

-- Aleš

More information about the Iris-Club mailing list