[Iris-Club] Excluded middle leads to inconsistency

Derek Dreyer dreyer at mpi-sws.org
Wed May 3 08:32:08 CEST 2017


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