[Iris-Club] Excluded middle leads to inconsistency

[Aleš Bizjak]

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š