[Iris-Club] Excluded middle leads to inconsistency
abizjak at cs.au.dk
Wed May 3 09:07:47 CEST 2017
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 ▷.
More information about the Iris-Club