What is "intuitionistic logic"

n. (context mathematics logic English) A type of logic which rejects the axiom law of excluded middle or, equivalently, the law of double negation and/or Peirce's law. It is the foundation of intuitionism.

Intuitionistic logic, sometimes more generally called constructive logic, is a system of symbolic logic that differs from classical logic by replacing the traditional concept of truth with the concept of constructive provability. For example, in classical logic, propositional formulae are always assigned a truth value from the two element set of trivial propositions {⊤, ⊥} ("true" and "false" respectively) regardless of whether we have direct evidence for either case. This is referred to as the 'law of excluded middle', because it excludes the possibility of any truth value besides 'true' or 'false'. In contrast, propositional formulae in intuitionistic logic are not assigned any definite truth value at all and instead only considered "true" when we have direct evidence, hence proof. (We can also say, instead of the propositional formula being "true" due to direct evidence, that it is inhabited by a proof in the Curry–Howard sense.) Operations in intuitionistic logic therefore preserve justification, with respect to evidence and provability, rather than truth-valuation.

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 {⊤, ⊥} from classical logic, each proof of a propositional formula is considered a valid propositional value, thus by Heyting's notion of propositions-as-sets, propositional formulae are (potentially non-finite) sets of their proofs.

From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not valid logical rules. The rule of double negation elimination (for any proposition P, ¬¬P → P) can be seen as a result of the law of excluded middle. This is because it asserts that a proof of ¬¬P, a proof that ¬P is false, is equivalent to a proof that P is true. 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.

Several systems of semantics for intuitionistic logic have been studied. One semantics mirrors classical Boolean-valued semantics but uses Heyting algebras in place of Boolean algebras. Another semantics uses Kripke models.

One important thing to note is that intuitionistic logic is but one of the set of approaches referred to as Constructivism. The use of constructivist logics in general is a controversial topic among mathematicians and philosophers (see, for example, the famous Brouwer–Hilbert controversy). A very 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. These are considered to be so important to the practice of mathematics that David Hilbert wrote of them: "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."

Despite the serious challenges presented by the inability to utilize these two valuable logical rules, intuitionistic logic has practical use. 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 verification (and generation) 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 which are feasible to create and check solely by hand. One example of a proof which was impossible to formally verify before the advent of these tools is the famous proof of the Four color theorem. This theorem stumped mathematicians for more than a hundred years, until a proof was developed which 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 it was finally verified using Coq.

Formalized intuitionistic logic was originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism.