[Iris-Club] Excluded middle leads to inconsistency

[Ralf Jung]

Well, but it's not like we know the canonical set of rules we will get
in the presence of box without * elimination.  For example, it seems
likely that we will *not* have "box P |- P".  (However, we will have
"box P |- P * box P".)  So if you use box in linear Iris, you better
state which rules you use.

I think however that "True |- box True" is something we do get;
otherwise it'll be hard to prove anything under the box...

; Ralf

On 03.05.2017 10:50, Derek Dreyer wrote:
> 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
>