[Iris-Club] Excluded middle leads to inconsistency
Derek Dreyer
dreyer at mpi-sws.org
Wed May 3 10:13:09 CEST 2017
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?
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
More information about the Iris-Club
mailing list