[Iris-Club] Excluded middle leads to inconsistency

[Derek Dreyer]

This is why I said in my original mail that I'm not sure how my proof
plays out in the absence of box.

Derek

On Wed, May 3, 2017 at 10:47 AM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
> You could replace the True at the beginning with emp.
>
> Derek
>
> On Wed, May 3, 2017 at 10:47 AM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
>> Yes.  This is exactly why I put the Box there.
>>
>> Where did I use True |- Box(True)?
>>
>> Derek
>>
>> On Wed, May 3, 2017 at 10:44 AM, Aleš Bizjak <abizjak at cs.au.dk> wrote:
>>> 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š
>>>
>>> --
>>> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
>>> Management: https://lists.mpi-sws.org/listinfo/iris-club
>>> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org