Semantic explanation for converting intuitionistic logic into classical logic by adding LEM as an axiom

Question

I have a question about converting intuitionistic logic (IL) into classical logic (CL) by adding LEM as an axiom. IL is usually understood as a logic without LEM.

$$\textrm{LEM}:=A\vee\neg A.$$

In many proof assistants, by adding LEM, we can make a shift from the intuitionistic reasoning to classical reasoning.

But I have a question regarding the role of LEM from a semantic perspective. It is well-known that the relational semantics for IL is given in terms of Kripke's possible worlds. But for the semantics of CL, we will not need possible worlds anymore.

My question is: since by adding LEM to IL, we obtain CL, how could we understand the addition of LEM from a semantic perspective? That is to say, why can we get rid of the possible worlds in the semantics of IL by adding LEM, moving towards a simpler semantics for CL?

Thanks!

Answer 1

Here's a somewhat-informal interpretation of the situation which may help:

Many extensions/fragments of intuitionistic logic can be thought of, via the Kripke frame semantics, as corresponding to frame properties - namely, those properties which validate the principles of that logic. So, for example, one such validated property of intuitionistic logic is that every world see itself, since given a frame not satisfying this condition we can whip up a family of models on that frame such that at some world $A$ is true but $\neg\neg A$ is false.

Now let's interpret LEM as a frame property. The frames validating (intuitionistic logic +) LEM turn out to be those in which each world $w$ sees itself and only itself. Clearly every such frame validates LEM. In the other direction, if world $a$ saw world $b$ with $a\not=b$ we could make $A$ false at $a$ but true at $b$, in which case neither $A$ nor $\neg A$ would hold at world $a$.

But such a frame is basically just a bunch of classical models put next to each other, with no interesting relationships to each other. At this point the whole Kripkean idea trivializes: technically there may be multiple worlds floating around in such a frame, but it's not really "multiple-worldy" in any meaningful sense.

---

FWIW, Chagrov/Zakharyaschev says a lot about frame properties and intuitionistic logic (and its relatives), and is all-around an amazing source to have on hand. While it can be quite difficult at first, it's ultimately very rewarding.