Editing Intuitionistic logic (section)

==== 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]]).