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?

  • 2
    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.
    – PW_246
    Commented Mar 15, 2023 at 12:38

1 Answer 1


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.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .