[Iris-Club] Excluded middle leads to inconsistency

[Joseph Tassarotti]

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.