[Iris-Club] Excluded middle leads to inconsistency

[Ralf Jung]

Hi,

> I'm a little confused.  My example did not rely on the later modality
> or *-elimination, but it does rely on state change.  I suppose that in
> my example I am using EM to prove not \later False, but \upd False?

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.

Kind regards,
Ralf

> 
> Derek
> 
> 
> On Wed, May 3, 2017 at 9:04 AM, Robbert Krebbers
> <mail at robbertkrebbers.nl> wrote:
>> Hi Joe and Derek,
>>
>> I think there are at least two results that are well-known:
>>
>> 1.) From EM (= excluded middle) and Löb we get that ▷ is degenerate (i.e. ▷
>> P |- False for any P). This is what Joe has shown. I think this result is
>> folklore in modal logic, and have seen it various times while I worked in
>> Aarhus.
>>
>> 2.) From EM + *-elimination (P * Q |- P) we get that * and /\ coincide,
>> (i.e. P /\ Q -||- P * Q). According to [1], this is also well-known from the
>> early days of separation logic.
>>
>> Best,
>>
>> Robbert
>>
>> [1] Qinxiang Cao, Santiago Cuellar, and Andrew Appel. "Putting Order To The
>> Separation Logic Jungle". Draft
>>
>>
>> http://scholar.princeton.edu/sites/default/files/qinxiang/files/putting_order_to_the_separation_logic_jungle_revised_version.pdf
>>
>>
>> On 05/03/2017 08:32 AM, Derek Dreyer wrote:
>>>
>>> Hi, Joe.  Nice to see this proven in the base logic, but is it that
>>> surprising?  I thought it was well known (or at least easy to observe)
>>> that excluded middle is inconsistent even in Iris 1.0, as follows:
>>>
>>> Let P(x) = Box(x |-> 0 \/ not(x |-> 0)).
>>>
>>> {True}
>>> {Forall x. P(x)}
>>> new 0
>>> {y. y |-> 0 * Forall x. P(x)}
>>> {y |-> 0 * P(y)}
>>> {False}
>>>
>>> Of course, this proof does not depend fundamentally on computation and
>>> could be replayed in Iris base logic, but it does seem to rely on
>>> state update.  (I'm not 100% sure whether the above proof plays out
>>> properly in vanilla separation logic in the absence of box.)
>>>
>>> Thanks,
>>> Derek
>>>
>>> On Wed, May 3, 2017 at 1:53 AM, Joseph Tassarotti
>>> <jtassaro at andrew.cmu.edu> wrote:
>>>>
>>>> Hello,
>>>>
>>>> At ETAPS last week there was a lot of discussion about linear vs. affine
>>>> separation logic and classical vs. intuitionistic logic.
>>>>
>>>> I began to wonder whether we can consistently add the axiom (P \/ P ->
>>>> False) to the Iris base logic. I was surprised to learn that the answer
>>>> is
>>>> no, as one is then able to derive (later False). I include a proof below.
>>>> This does not use any of the multiplicative connectives at all, so it's
>>>> actually probably the case for many guarded type theories as well. Is
>>>> this
>>>> mentioned anywhere? I did a bit of searching, and it appears that in the
>>>> modal/provability logic community, it is known that P \/ ~P is
>>>> inconsistent
>>>> in some even weaker provability logics than the base logic of Iris, but I
>>>> haven't seen this pointed out in the PL community.
>>>>
>>>> -Joe
>>>>
>>>> From iris.base_logic Require Import base_logic soundness.
>>>> From iris.proofmode Require Import tactics.
>>>> Set Default Proof Using "Type*".
>>>>
>>>> Module classical. Section classical.
>>>>   Context (M : ucmraT).
>>>>   Notation iProp := (uPred M).
>>>>
>>>>   Hypothesis excluded: ∀ (P: iProp), (P ∨ (P → False))%I.
>>>>
>>>>   Lemma later_false_disj (P: iProp): (▷ P ∨ ▷ (▷ P → False))%I.
>>>>   Proof using All.
>>>>     iDestruct (excluded (▷ P)) as "[HP|HlP]".
>>>>     - by iLeft.
>>>>     - iRight. by iNext.
>>>>   Qed.
>>>>
>>>>   Lemma contradiction: (▷ False : iProp)%I.
>>>>   Proof using All.
>>>>     iDestruct (later_false_disj False%I) as "[HF|HL]".
>>>>     - done.
>>>>     - iLöb as "IH".
>>>>       iNext. iApply "HL". done.
>>>>   Qed.
>>>> End classical. End classical.
>>>>
>>>>
>>>> --
>>>> 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
>>>
>>>
>>
>> --
>> 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
>