Editing Intuitionistic logic (section)

==== Modal logic ====
Any formula of the intuitionistic propositional logic (IPC<!-- laking reference to this acronym, i found one usage here https://plato.stanford.edu/entries/logic-intuitionistic/ -->) may be translated into the language of the [[normal modal logic]] [[Kripke semantics#Correspondence and completeness|S4]] as follows:

:<math>\begin{align}
\bot^* &=  \bot \\
A^* &= \Box A && \text{if } A \text{ is prime (a positive literal)} \\
(A \wedge B)^*&= A^* \wedge B^* \\
(A \vee B)^* &=  A^* \vee B^* \\
(A \to B)^*&= \Box \left (A^* \to B^* \right ) \\
(\neg A)^*&= \Box(\neg (A^*)) &&  \neg A := A \to \bot
\end{align}</math>

and it has been demonstrated that the translated formula is valid in the propositional modal logic S4 if and only if the original formula is valid in IPC.{{sfn|Lévy|2011|pages=4-5}} The above set of formulae are called the [[Modal companion|Gödel–McKinsey–Tarski translation]].
There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.{{sfn|Alechina|Mendler|De Paiva|Ritter|2003}}