Editing Intuitionistic logic (section)

==Metalogic==
===Admissible rules===
In intuitionistic logic or a fixed theory using the logic, the situation can occur that an implication always hold metatheoretically, but not in the language. For example, in the pure propositional calculus, if <math>(\neg A)\to(B\lor C)</math> is provable, [[independence of premise|then so is]] <math>(\neg A\to B)\lor(\neg A\to C)</math>. Another example is that <math>(A\to B)\to(A\lor C)</math> being provable always also means that so is <math>\big((A\to B)\to A\big)\lor\big((A\to B)\to C\big)</math>. One says the system is closed under these implications as [[admissible rule|rules]] and they may be adopted.

===Theories' features===
Theories over constructive logics can exhibit the [[disjunction property]]. The pure intuitionistic propositional calculus does so as well.

In particular, it means the excluded middle disjunction for an un-rejectable statement <math>A</math> is provable exactly when <math>A</math> is provable.
This also means, for examples, that the excluded middle disjunction for some the excluded middle disjunctions are not provable also.

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

===Lambda calculus===
There is an extended [[Curry–Howard isomorphism]] between IPC and [[simply typed lambda calculus]].{{sfn|Alechina|Mendler|De Paiva|Ritter|2003}}