[Iris-Club] Excluded middle leads to inconsistency
jtassaro at andrew.cmu.edu
Wed May 3 11:49:38 CEST 2017
Thanks for the many responses. Let me just say why I found this
surprising (setting aside the point about affine/linear BI and excluded
middle). There is a well-known *classical* modal logic GL (for
"Godel-Lob") that has been studied for a long time, which has a Lob
rule. So, I didn't see any reason why the Lob rule should be
incompatible with excluded middle!
It's true that in GL the Lob rule is instead ▷(▷P -> P) -> ▷P, but
Nakano showed that the stronger version we use is derivable from this
weaker version. Therefore I assumed that the stronger rule we use should
also be compatible with excluded middle. But apparently it isn't.
I think what's going on is that in GL one does not have P -> ▷P. And
Nakano's proof of the equivalence of the two Lob rules relies on
precisely this fact. So, what you can't have is weak lob + this axiom +
excluded middle. Of course, P |- ▷P is absolutely crucial in Iris and
the other uses of the later modality in the PL community.
On 05/03/2017 03:07 AM, Aleš Bizjak wrote:
> Hi Joe.
> On 02 May 2017, at 19:53:29, Joseph Tassarotti wrote:
>> 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.
> I don't recall any specific place where this is mentioned, but it is a
> "well-known" fact that excluded middle (in general) makes ▷ trivial.
> An even easier way to see this is to assume double negation elimination instead.
> Then the Löb axiom states ¬¬▷⊥, and so ▷⊥, from which ▷P for any P.
> This uses just the Löb rule and monotonicity of ▷.
> -- Aleš
More information about the Iris-Club