[Iris-Club] Excluded middle leads to inconsistency
Robbert Krebbers
mail at robbertkrebbers.nl
Wed May 3 09:04:23 CEST 2017
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
>
More information about the Iris-Club
mailing list