Editing Intuitionistic logic (section)

===Relation to other logics===
==== Paraconsistent logic ====
Intuitionistic logic is related by [[duality (mathematics)|duality]] to a [[paraconsistent logic]] known as ''Brazilian'', ''anti-intuitionistic'' or ''dual-intuitionistic logic''.{{sfn|Aoyama|2004}}

The subsystem of intuitionistic logic with the FALSE (resp. NOT-2) axiom removed is known as [[minimal logic]] and some differences have been elaborated on above.

==== Intermediate logics ====
In 1932, [[Kurt Gödel]] defined a system of logics intermediate between classical and intuitionistic logic. Indeed, any finite Heyting algebra that is not equivalent to a Boolean algebra defines (semantically) an [[intermediate logic]]. On the other hand, validity of formulae in pure intuitionistic logic is not tied to any individual Heyting algebra but relates to any and all Heyting algebras at the same time.

So for example, for a [[Axiom schema|schema]] not involving negations, consider the classically valid <math>(A\to B)\lor(B\to A)</math>. Adopting this over intuitionistic logic gives the intermediate logic called [[Gödel-Dummett logic]].

==== Relation to classical logic ====
The system of classical logic is obtained by adding any one of the following axioms:
* <math>\phi \lor \neg \phi</math> (Law of the excluded middle)
* <math>\neg \neg \phi \to \phi</math> (Double negation elimination)
* <math>(\neg \phi \to \phi) \to \phi</math> ([[Consequentia mirabilis]], see also [[Peirce's law]])

Various reformulations, or formulations as schemata in two variables (e.g. Peirce's law), also exist. One notable one is the (reverse) law of contraposition
* <math>(\neg \phi \to \neg \chi ) \to (\chi \to \phi)</math>
Such are detailed on the [[intermediate logic]]s article.

In general, one may take as the extra axiom any classical tautology that is not valid in the two-element [[Kripke frame]] <math>\circ{\longrightarrow}\circ</math> (in other words, that is not included in [[intermediate logic|Smetanich's logic]]).

==== Many-valued logic ====
[[Kurt Gödel]]'s work involving [[many-valued logic]] showed in 1932 that intuitionistic logic is not a [[finite-valued logic]].{{sfn|Burgess|2014}} (See the section titled [[#Heyting algebra semantics|Heyting algebra semantics]] above for an [[infinite-valued logic]] interpretation of intuitionistic logic.)

==== 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}}