# What's the constructivist's view to the S4 modal logic?

Intuitionistic logic can be translated to S4 modal logic by parsing intuitionistic P→Q to classical □(P→Q). There is no other way round, for there is no intuitionistic equivalent to ◊P. To analyze more, ◊P is equivalent to classical ¬□¬P, and that would be like ¬¬P where the inner negation is intuitionistic and the outer negation is classical.

I wonder how a constructivist would treat statements like ◊P. How would they?

• This could be said to be interpreted as the non-tautological knowledge that there exists a proof of P in some possible world accessible from the actual world while it cannot be qualified as constructive per se obviously... Commented Feb 21, 2023 at 1:57
• There is a negation operator that can be added to Intuitionistic Logic which allows one to express \$\Diamond \Diamond p\$, which is equivalent to \$\Diamond p\$ in S4. That is if \$\sim p\$ is verified at some state \$w\$, then there is a state \$v\$ such that \$w R v\$ and \$p\$ is not verified at v. Then, we have that \$\sim \neg p\$ is the translation for \$\Diamond \Diamond p\$. The resulting logic is non-constructive. Commented Mar 15, 2023 at 12:38

## 1 Answer

The translation you are referring to is the Gödel-McKinsey-Tarski translation. Actually, the S4 translation of intuitionistic P → Q is □(□P → □Q) which can be understood informally as: I can prove that a proof of P can be converted into a proof of Q. Intuitionistic ¬P translates into classical S4 as □¬□P which can be understood as: I can prove that there is not a proof of P.

A constructivist can undertand classical S4 □P as saying that P is provable. But there is no simple constructive way to understand classical ◇P. Classical ◇P says in effect that it is not the case that not-P is provable, but without constructing a proof to show that this is so.

This is analogous to how classical (∃x)Fx says that something is F, but without constructing it. However, we can use the double negation translation to represent classical (∃x)Fx within intuitionistic logic as ¬¬(∃x)Fx. If we use intuitionistic modal logic, then we might be able to represent classical ◇P as intuitionistic ¬¬◇P. In practice, the interpretation of ◇P in intuitionism depends on context, so I am not confident this would always work.