Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of intuitionistic logic do not assume the law of the excluded middle and double negation elimination, which are fundamental inference rules in classical logic.
Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for L. E. J. Brouwer's programme of intuitionism. From a proof-theoretic perspective, Heyting’s calculus is a restriction of classical logic in which the law of excluded middle and double negation elimination have been removed. Excluded middle and double negation elimination can still be proved for some propositions on a case by case basis, however, but do not hold universally as they do with classical logic. The standard explanation of intuitionistic logic is the BHK interpretation.
Several systems of semantics for intuitionistic logic have been studied. One of these semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models. These, however, are technical means for studying Heyting’s deductive system rather than formalizations of Brouwer’s original informal semantic intuitions. Semantical systems claiming to capture such intuitions, due to offering meaningful concepts of “constructive truth” (rather than merely validity or provability), are Kurt Gödel’s dialectica interpretation, Stephen Cole Kleene’s realizability, Yurii Medvedev’s logic of finite problems, or Giorgi Japaridze’s computability logic. Yet such semantics persistently induce logics properly stronger than Heyting’s logic. Some authors have argued that this might be an indication of inadequacy of Heyting’s calculus itself, deeming the latter incomplete as a constructive logic.
In the semantics of classical logic, propositional formulae are assigned truth values from the two-element set
\{\top,\bot\}
Intuitionistic logic is a commonly-used tool in developing approaches to constructivism in mathematics. The use of constructivist logics in general has been a controversial topic among mathematicians and philosophers (see, for example, the Brouwer–Hilbert controversy). A common objection to their use is the above-cited lack of two central rules of classical logic, the law of excluded middle and double negation elimination. David Hilbert considered them to be so important to the practice of mathematics that he wrote:
"Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists. To prohibit existence statements and the principle of excluded middle is tantamount to relinquishing the science of mathematics altogether."[1] Intuitionistic logic has found practical use in mathematics despite the challenges presented by the inability to utilize these rules. One reason for this is that its restrictions produce proofs that have the existence property, making it also suitable for other forms of mathematical constructivism. Informally, this means that if there is a constructive proof that an object exists, that constructive proof may be used as an algorithm for generating an example of that object, a principle known as the Curry–Howard correspondence between proofs and algorithms. One reason that this particular aspect of intuitionistic logic is so valuable is that it enables practitioners to utilize a wide range of computerized tools, known as proof assistants. These tools assist their users in the generation and verification of large-scale proofs, whose size usually precludes the usual human-based checking that goes into publishing and reviewing a mathematical proof. As such, the use of proof assistants (such as Agda or Coq) is enabling modern mathematicians and logicians to develop and prove extremely complex systems, beyond those that are feasible to create and check solely by hand. One example of a proof that was impossible to satisfactorily verify without formal verification is the famous proof of the four color theorem. This theorem stumped mathematicians for more than a hundred years, until a proof was developed that ruled out large classes of possible counterexamples, yet still left open enough possibilities that a computer program was needed to finish the proof. That proof was controversial for some time, but, later, it was verified using Coq.
The syntax of formulas of intuitionistic logic is similar to propositional logic or first-order logic. However, intuitionistic connectives are not definable in terms of each other in the same way as in classical logic, hence their choice matters. In intuitionistic propositional logic (IPL) it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬A as an abbreviation for . In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.
Intuitionistic logic can be defined using the following Hilbert-style calculus. This is similar to a way of axiomatizing classical propositional logic.
In propositional logic, the inference rule is modus ponens
\phi\to\psi
\phi
\psi
\psi\to(\phi\to\psi)
(\chi\to(\phi\to\psi))\to((\chi\to\phi)\to(\chi\to\psi))
\phi\land\chi\to\phi
\phi\land\chi\to\chi
\phi\to(\chi\to(\phi\land\chi))
\phi\to\phi\lor\chi
\chi\to\phi\lor\chi
(\phi\to\psi)\to((\chi\to\psi)\to((\phi\lor\chi)\to\psi))
\bot\to\phi
\forall
\psi\to\phi
\psi\to(\forallx \phi)
x
\psi
\exists
\phi\to\psi
(\existsx \phi)\to\psi
x
\psi
(\forallx \phi(x))\to\phi(t)
t
x
\phi
t
\phi(t)
\phi(t)\to(\existsx \phi(x))
If one wishes to include a connective
\neg
\phi\to\bot
(\phi\to\bot)\to\neg\phi
\neg\phi\to(\phi\to\bot)
There are a number of alternatives available if one wishes to omit the connective
\bot
(\phi\to\chi)\to((\phi\to\neg\chi)\to\neg\phi)
\chi\to(\neg\chi\to\psi)
(\phi\to\neg\chi)\to(\chi\to\neg\phi)
(\phi\to\neg\phi)\to\neg\phi
The connective
\leftrightarrow
\phi\leftrightarrow\chi
(\phi\to\chi)\land(\chi\to\phi)
(\phi\leftrightarrow\chi)\to(\phi\to\chi)
(\phi\leftrightarrow\chi)\to(\chi\to\phi)
(\phi\to\chi)\to((\chi\to\phi)\to(\phi\leftrightarrow\chi))
IFF-1 and IFF-2 can, if desired, be combined into a single axiom
(\phi\leftrightarrow\chi)\to((\phi\to\chi)\land(\chi\to\phi))
See main article: Sequent calculus. Gerhard Gentzen discovered that a simple restriction of his system LK (his sequent calculus for classical logic) results in a system that is sound and complete with respect to intuitionistic logic. He called this system LJ. In LK any number of formulas is allowed to appear on the conclusion side of a sequent; in contrast LJ allows at most one formula in this position.
Other derivatives of LK are limited to intuitionistic derivations but still allow multiple conclusions in a sequent. LJ' is one example.
The theorems of the pure logic are the statements provable from the axioms and inference rules. For example, using THEN-1 in THEN-2 reduces it to
(\chi\to(\phi\to\psi))\to(\phi\to(\chi\to\psi))
\bot
\psi
(\chi\to\neg\phi)\to(\phi\to\neg\chi)
\chi
\phi
\phi
\chi
(\chi\to\neg\phi)\leftrightarrow(\phi\to\neg\chi)
A double negation does not affirm the law of the excluded middle (PEM); while it is not necessarily the case that PEM is upheld in any context, no counterexample can be given either. Such a counterexample would be an inference (inferring the negation of the law for a certain proposition) disallowed under classical logic and thus PEM is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that
((\psi\lor(\psi\to\varphi))\to\varphi)\leftrightarrow\varphi
\varphi
\neg\neg(\psi\lor\neg\psi)
\neg(\psi\lor\neg\psi)
When assuming the law of excluded middle implies a proposition, then by applying contraposition twice and using the double-negated excluded middle, one may prove double-negated variants of various strictly classical tautologies. The situation is more intricate for predicate logic formulas, when some quantified expressions are being negated.
Akin to the above, from modus ponens in the form
\psi\to((\psi\to\varphi)\to\varphi)
\psi\to\neg\neg\psi
(\neg\neg\psi)\to\phi
\psi\to\phi
An implication
\psi\to\neg\phi
\neg\neg\psi\to\neg\phi
\psi=\neg\phi
\neg\neg\neg\phi\to\neg\phi
In general,
\neg\neg\psi\to\phi
\psi\to\phi
\neg\neg(\psi\to\phi)
\psi\to(\neg\neg\phi)
(\neg\neg\psi)\to(\neg\neg\phi)
\neg\phi\to\neg\psi
\neg\neg(\neg\neg\phi\to\phi)
When
\psi
\neg\neg\psi
\psi
(\phi\to\neg\psi)\to\neg\phi
Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the double-negation translation. It constitutes an embedding of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. For example, any theorem of classical propositional logic of the form
\psi\to\phi
\psi\to\neg\neg\phi
Already minimal logic easily proves the following theorems, relating conjunction resp. disjunction to the implication using negation:
(\phi\lor\psi)\to\neg(\neg\phi\land\neg\psi)
(\phi\lor\psi)\to(\neg\phi\to\neg\neg\psi)
(\phi\land\psi)\to\neg(\neg\phi\lor\neg\psi)
(\phi\land\psi)\to\neg(\phi\to\neg\psi)
(\phi\to\psi)\to\neg(\phi\land\neg\psi)
\psi
\neg\neg\psi
\neg\psi
\phi
\phi
In contrast, in classical propositional logic it is possible to take one of those three connectives plus negation as primitive and define the other two in terms of it, in this way. Such is done, for example, in Łukasiewicz's three axioms of propositional logic. It is even possible to define all in terms of a sole sufficient operator such as the Peirce arrow (NOR) or Sheffer stroke (NAND). Similarly, in classical first-order logic, one of the quantifiers can be defined in terms of the other and negation.These are fundamentally consequences of the law of bivalence, which makes all such connectives merely Boolean functions.The law of bivalence is not required to hold in intuitionistic logic. As a result, none of the basic connectives can be dispensed with, and the above axioms are all necessary. So most of the classical identities between connectives and quantifiers are only theorems of intuitionistic logic in one direction. Some of the theorems go in both directions, i.e. are equivalences, as subsequently discussed.
Firstly, when
x
\varphi
(\existsx(\phi(x)\to\varphi))\to((\forallx \phi(x))\to\varphi)
\forallx\phi(x)
If the domain of discourse is not empty and
\phi
x
(\phi\to\varphi)\to(\phi\to\varphi)
((\phi\to\varphi)\land\phi)\to\varphi
\varphi
\neg(\phi\land\neg\phi)
Considering a false proposition
\varphi
(\existsx \neg\phi(x))\to\neg(\forallx \phi(x))
x
\phi
\phi
The quantifier formula with negations also immediately follows from the non-contradiction principle derived above, each instance of which itself already follows from the more particular
\neg(\neg\neg\phi\land\neg\phi)
\neg\phi
\neg\neg\phi
\phi
\forallx \phi(x)
\forallx((\phi(x)\to\varphi)\to\varphi)
(\existsx \neg\phi(x))\to\neg(\forallx\neg\neg\phi(x))
x
\phi
\phi
Secondly,
(\forallx(\phi(x)\to\varphi))\leftrightarrow((\existsx \phi(x))\to\varphi)
(\forallx \neg\phi(x))\leftrightarrow\neg(\existsx \phi(x))
(\chi\to\neg\phi)\leftrightarrow(\phi\to\neg\chi)
(\forallx \phi(x))\to\neg(\existsx \neg\phi(x))
(\existsx \phi(x))\to\neg(\forallx \neg\phi(x))
(\forallx\neg\phi(x))\to\neg(\existsx\neg\neg\phi(x))
\to
More general variants hold. Incorporating the predicate
\psi
(\forallx \phi(x)\to(\psi(x)\to\varphi))\leftrightarrow((\existsx \phi(x)\land\psi(x))\to\varphi)
\psi
x
\psi
x
A=\{x\mid\phi(x)\}
B=\{x\mid\psi(x)\}
\varphi
A\capB=\emptyset
\forall(x\inA).x\notinB\leftrightarrow\neg\exists(x\inA).x\inB
There are finite variations of the quantifier formulas, with just two propositions:
(\neg\phi\lor\neg\psi)\to\neg(\phi\land\psi)
(\neg\phi\land\neg\psi)\leftrightarrow\neg(\phi\lor\psi)
\neg\psi
\phi
\neg\psi\lor\neg\neg\psi
\neg\psi\lor\neg\neg\psi\lor(\neg\neg\psi\to\psi)
\neg\phi\lor\neg\psi
\neg(\phi\land\psi)
The converse variants of those two, and the equivalent variants with double-negated antecedents, had already been mentioned above. Implications towards the negation of a conjunction can often be proven directly from the non-contradiction principle. In this way one may alos obtain the mixed form of the implications, e.g.
(\neg\phi\lor\psi)\to\neg(\phi\land\neg\psi)
(\neg\neg\phi\lor\neg\neg\psi)\to\neg\neg(\phi\lor\psi)
In predicate logic, the constant domain principle is not valid:
\forallx(\varphi\lor\psi(x))
\varphi\lor\forallx\psi(x)
From the general equivalence also follows import-export, expressing incompatibility of two predicates using two different connectives:
(\phi\to\neg\psi)\leftrightarrow\neg(\phi\land\psi)
(\phi\to\neg\psi)\leftrightarrow(\psi\to\neg\phi)
(\phi\to\psi)\to\neg(\phi\land\neg\psi)
\phi\to\psi
\phi\to\neg\neg\psi
Now when using the principle in the next section, the following variant of the latter, with more negations on the left, also holds:
\neg(\phi\to\psi)\leftrightarrow(\neg\neg\phi\land\neg\psi)
\neg\neg(\phi\land\psi)\leftrightarrow(\neg\neg\phi\land\neg\neg\psi)
Already minimal logic proves excluded middle equivalent to consequentia mirabilis, an instance of Peirce's law. Now akin to modus ponens, clearly
(\phi\lor\psi)\to((\phi\to\psi)\to\psi)
\phi
\psi\to\varphi
In intuitionistic logic, one obtains variants of the stated theorem involving
\bot
\neg(\phi\land\psi)
(\neg\phi\vee\neg\psi)\to(\phi\to\neg\psi)
\neg\psi
(\neg\phi\lor\psi)\to(\phi\to\psi)
\neg\phi
\phi
P
Q
P
Q
Non-contradiction and explosion together also prove the stronger variant
(\neg\phi\lor\psi)\to(\neg\neg\phi\to\psi)
\psi
\psi
\neg\neg(\psi\lor\neg\psi)
Of course the formulas established here may be combined to obtain yet more variations. For example, the disjunctive syllogism as presented generalizes to
((\existsx \neg\phi(x))\lor\varphi)\to((\forallx \phi(x))\to\varphi)
\existsx(\phi(x)\to\varphi)
The bulk of the discussion in these sections applies just as well to just minimal logic. But as for the disjunctive syllogism with general
\psi
(\neg\phi\lor\psi)\to(\neg\neg\phi\to\psi')
\psi'
\neg\neg\psi\land(\psi\lor\neg\psi)
\psi
The above lists also contain equivalences.The equivalence involving a conjunction and a disjunction stems from
(P\lorQ)\toR
P\toR
\bot
R
P
Q
P
Q
An equivalence itself is generally defined as, and then equivalent to, a conjunction (
\land
\to
(\phi\leftrightarrow\psi)\leftrightarrow((\phi\to\psi)\land(\psi\to\phi))
(\phi\to\psi)\leftrightarrow((\phi\lor\psi)\leftrightarrow\psi)
(\phi\to\psi)\leftrightarrow((\phi\land\psi)\leftrightarrow\phi)
(\phi\land\psi)\leftrightarrow((\phi\to\psi)\leftrightarrow\phi)
(\phi\land\psi)\leftrightarrow(((\phi\lor\psi)\leftrightarrow\psi)\leftrightarrow\phi)
In turn,
\{\lor,\leftrightarrow,\bot\}
\{\land,\leftrightarrow,\neg\}
As shown by Alexander V. Kuznetsov, either of the following connectives – the first one ternary, the second one quinary – is by itself functionally complete: either one can serve the role of a sole sufficient operator for intuitionistic propositional logic, thus forming an analog of the Sheffer stroke from classical propositional logic:
((P\lorQ)\land\negR)\lor(\negP\land(Q\leftrightarrowR))
P\to(Q\land\negR\land(S\lorT))
The semantics are rather more complicated than for the classical case. A model theory can be given by Heyting algebras or, equivalently, by Kripke semantics. Recently, a Tarski-like model theory was proved complete by Bob Constable, but with a different notion of completeness than classically.
Unproved statements in intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). One can prove that such statements have no third truth value, a result dating back to Glivenko in 1928. Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.
A consequence of this point of view is that intuitionistic logic has no interpretation as a two-valued logic, nor even as a finite-valued logic, in the familiar sense. Although intuitionistic logic retains the trivial propositions
\{\top,\bot\}
In classical logic, we often discuss the truth values that a formula can take. The values are usually chosen as the members of a Boolean algebra. The meet and join operations in the Boolean algebra are identified with the ∧ and ∨ logical connectives, so that the value of a formula of the form A ∧ B is the meet of the value of A and the value of B in the Boolean algebra. Then we have the useful theorem that a formula is a valid proposition of classical logic if and only if its value is 1 for every valuation—that is, for any assignment of values to its variables.
A corresponding theorem is true for intuitionistic logic, but instead of assigning each formula a value from a Boolean algebra, one uses values from a Heyting algebra, of which Boolean algebras are a special case. A formula is valid in intuitionistic logic if and only if it receives the value of the top element for any valuation on any Heyting algebra.
It can be shown that to recognize valid formulas, it is sufficient to consider a single Heyting algebra whose elements are the open subsets of the real line R. In this algebra we have:
\begin{align} Value[\bot]&=\emptyset\\ Value[\top]&=R\\ Value[A\landB]&=Value[A]\capValue[B]\\ Value[A\lorB]&=Value[A]\cupValue[B]\\ Value[A\toB]&=int\left(Value[A]\complement\cupValue[B]\right) \end{align}
where int(X) is the interior of X and X∁ its complement.
The last identity concerning A → B allows us to calculate the value of ¬A:
\begin{align} Value[\negA]&=Value[A\to\bot]\\ &=int\left(Value[A]\complement\cupValue[\bot]\right)\\ &=int\left(Value[A]\complement\cup\emptyset\right)\\ &=int\left(Value[A]\complement\right) \end{align}
With these assignments, intuitionistically valid formulas are precisely those that are assigned the value of the entire line. For example, the formula ¬(A ∧ ¬A) is valid, because no matter what set X is chosen as the value of the formula A, the value of ¬(A ∧ ¬A) can be shown to be the entire line:
\begin{align} Value[\neg(A\land\negA)]&=int\left(Value[A\land\negA]\complement\right)&&Value[\negB]=int\left(Value[B]\complement\right)\\ &=int\left(\left(Value[A]\capValue[\negA]\right)\complement\right)\\ &=int\left(\left(Value[A]\capint\left(Value[A]\complement\right)\right)\complement\right)\\ &=int\left(\left(X\capint\left(X\complement\right)\right)\complement\right)\\ &=int\left(\emptyset\complement\right)&&int\left(X\complement\right)\subseteqX\complement\\ &=int(R)\\ &=R \end{align}
So the valuation of this formula is true, and indeed the formula is valid. But the law of the excluded middle, A ∨ ¬A, can be shown to be invalid by using a specific value of the set of positive real numbers for A:
\begin{align} Value[A\lor\negA]&=Value[A]\cupValue[\negA]\\ &=Value[A]\cupint\left(Value[A]\complement\right)&&Value[\negB]=int\left(Value[B]\complement\right)\\ &=\{x>0\}\cupint\left(\{x>0\}\complement\right)\\ &=\{x>0\}\cupint\left(\{x\leqslant0\}\right)\\ &=\{x>0\}\cup\{x<0\}\\ &=\{x ≠ 0\}\\ & ≠ R \end{align}
The interpretation of any intuitionistically valid formula in the infinite Heyting algebra described above results in the top element, representing true, as the valuation of the formula, regardless of what values from the algebra are assigned to the variables of the formula. Conversely, for every invalid formula, there is an assignment of values to the variables that yields a valuation that differs from the top element. No finite Heyting algebra has the second of these two properties.
See main article: Kripke semantics.
Building upon his work on semantics of modal logic, Saul Kripke created another semantics for intuitionistic logic, known as Kripke semantics or relational semantics.
It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete. However, Robert Constable has shown that a weaker notion of completeness still holds for intuitionistic logic under a Tarski-like model. In this notion of completeness we are concerned not with all of the statements that are true of every model, but with the statements that are true in the same way in every model. That is, a single proof that the model judges a formula to be true must be valid for every model. In this case, there is not only a proof of completeness, but one that is valid according to intuitionistic logic.
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
(\negA)\to(B\lorC)
(\negA\toB)\lor(\negA\toC)
(A\toB)\to(A\lorC)
((A\toB)\toA)\lor((A\toB)\toC)
Intuitionistic logic is related by duality to a paraconsistent logic known as Brazilian, anti-intuitionistic or dual-intuitionistic logic.
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.
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 schema not involving negations, consider the classically valid
(A\toB)\lor(B\toA)
The system of classical logic is obtained by adding any one of the following axioms:
\phi\lor\neg\phi
\neg\neg\phi\to\phi
(\neg\phi\to\phi)\to\phi
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
(\neg\phi\to\neg\chi)\to(\chi\to\phi)
\circ{\longrightarrow}\circ
Kurt Gödel's work involving many-valued logic showed in 1932 that intuitionistic logic is not a finite-valued logic. (See the section titled Heyting algebra semantics above for an infinite-valued logic interpretation of intuitionistic logic.)
Any formula of the intuitionistic propositional logic (IPC) may be translated into the language of the normal modal logic S4 as follows:
\begin{align} \bot*&=\bot\\ A*&=\BoxA&&ifAisprime(apositiveliteral)\\ (A\wedgeB)*&=A*\wedgeB*\\ (A\veeB)*&=A*\veeB*\\ (A\toB)*&=\Box\left(A*\toB*\right)\\ (\negA)*&=\Box(\neg(A*))&&\negA:=A\to\bot \end{align}
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. The above set of formulae are called the Gödel–McKinsey–Tarski translation.There is also an intuitionistic version of modal logic S4 called Constructive Modal Logic CS4.
There is an extended Curry–Howard isomorphism between IPC and simply-typed lambda calculus.