Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
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?
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.
