# Intuitionistic Logic vs Constant Domains

Quantified modal logic is a controversial field, specifically since it forces one to consider what is meant by “world” in Kripke Semantics. For example, the formula $$\Box \forall x \varphi \implies \forall x \Box \varphi$$ requires that if $$\Box \forall x \varphi$$ is true at a world $$w$$, then every object in $$w$$’s domain must also be in any world $$v$$ such that the accessibility relation $$wRv$$ holds. For math, this isn’t that big of a deal, but even in math we don’t exactly want to require a non-shrinking domains model. With that said, intuitionism also has to contend with this issue, at least when using Kripke Semantics. In like manner, $$\neg \neg \forall x \varphi \implies \forall x \neg \neg \varphi$$ is a formula that also requires a non-shrinking domain.

Both of the aforementioned formulas are theorems in their respective logics, which makes the matter even more important to get right. A standard approach to “fixing” quantified modal logic is to change the underlying logic from classical FOL to Free FOL, but no such approach is taken for intuitionism. Is there a motivation for just accepting that domains don’t shrink in intuitionism? Does it have to do with the heredity principle? Regardless of whether a “world” is a different universe or a state of an investigation, it seems too much to assume a non-shrinking domain semantics.

The idea behind intuitionistic logic (and the origin of its name) is that of a so-called "creative subject"; a mathematician who develops knowledge over time. The branches of a Kripke model represent different paths the knowledge could take; there is a possible future where they learn $$A$$ and there is another possible future where they learn $$\neg A$$. But they will never lose knowledge; what has already been established will continue to have been proven at a later point in time. This is why the set of propositions that hold at the different stages is monotonous; and as a consequence, the objects about which these statements hold can not cease to exist either.
• Your answer helps a lot, but given that $\exists x a$ $=x$ is valid in intuitionism, I have a hard time seeing the “learning new information” part as a good justification for accepting non-shrinking domains. Commented Mar 21, 2023 at 23:26