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.
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?