Intuitionistic logic


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 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”, 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.

Mathematical constructivism

In the semantics of classical logic, propositional formulae are assigned truth values from the two-element set , 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 a definite truth value and are 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.
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. 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:
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 disjunction and existence properties, 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 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 Rocq.

Syntax

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 it is customary to use →, ∧, ∨, ⊥ as the basic connectives, treating ¬A as an abbreviation for. In intuitionistic first-order logic both quantifiers ∃, ∀ are needed.

Hilbert-style calculus

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
  • MP: from and infer
and the axioms are
  • THEN-1:
  • THEN-2:
  • AND-1:
  • AND-2:
  • AND-3:
  • OR-1:
  • OR-2:
  • OR-3:
  • FALSE:
To make this a system of first-order predicate logic, the generalization rules
  • -GEN: from infer, if is not free in
  • -GEN: from infer, if is not free in
are added, along with the axioms
  • PRED-1:, if the term is free for substitution for the variable in
  • PRED-2:, with the same restriction as for PRED-1

    Negation

If one wishes to include a connective for negation rather than consider it an abbreviation for, it is enough to add:
  • NOT-1':
  • NOT-2':
There are a number of alternatives available if one wishes to omit the connective . For example, one may replace the three axioms FALSE, NOT-1', and NOT-2' with the two axioms
  • NOT-1:
  • NOT-2:
as at. Alternatives to NOT-1 are or.

Equivalence

The connective for equivalence may be treated as an abbreviation, with standing for. Alternatively, one may add the axioms
  • IFF-1:
  • IFF-2:
  • IFF-3:
IFF-1 and IFF-2 can, if desired, be combined into a single axiom using conjunction.

Sequent calculus

discovered that a simple restriction of his system LK 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.

Theorems

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. A formal proof of the latter using the Hilbert system is given on that page. With for, this in turn implies. In words: "If being the case implies that is absurd, then if does hold, one has that is not the case." Due to the symmetry of the statement, one in fact obtained
When explaining the theorems of intuitionistic logic in terms of classical logic, it can be understood as a weakening thereof: It is more conservative in what it allows a reasoner to infer, while not permitting any new inferences that could not be made under classical logic. Each theorem of intuitionistic logic is a theorem in classical logic, but not conversely. Many tautologies in classical logic are not theorems in intuitionistic logicin particular, as said above, one of intuitionistic logic's chief aims is to not affirm the law of the excluded middle so as to vitiate the use of non-constructive proof by contradiction, which can be used to furnish existence claims without providing explicit examples of the objects that it proves exist.

Double negations

A double negation does not affirm the law of the excluded middle ; 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 disallowed under classical logic and thus PEM is not allowed in a strict weakening like intuitionistic logic. Formally, it is a simple theorem that for any two propositions. By considering any established to be false this indeed shows that the double negation of the law is retained as a tautology already in minimal logic. This means any is established to be inconsistent and the propositional calculus is in turn always compatible with classical logic.
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.

Double negation and implication

Akin to the above, from modus ponens in the form follows. The relation between them may always be used to obtain new formulas: A weakened premise makes for a strong implication, and vice versa. For example, note that if holds, then so does, but the schema in the other direction would imply the double-negation elimination principle. Propositions for which double-negation elimination is possible are also called stable. Intuitionistic logic proves stability only for restricted types of propositions. A formula for which excluded middle holds can be proven stable using the disjunctive syllogism, which is discussed more thoroughly below. The converse does however not hold in general, unless the excluded middle statement at hand is stable itself.
An implication can be proven to be equivalent to, whatever the propositions. As a special case, it follows that propositions of negated form are stable, i.e. is always valid.
In general, is stronger than, which is stronger than, which itself implies the three equivalent statements, and . Using the disjunctive syllogism, the previous four are indeed equivalent. This also gives an intuitionistically valid derivation of, as it is thus equivalent to an identity.
When expresses a claim, then its double-negation merely expresses the claim that a refutation of would be inconsistent. Having proven such a mere double-negation also still aids in negating other statements through negation introduction, as then. A double-negated existential statement does not denote existence of an entity with a property, but rather the absurdity of assumed non-existence of any such entity. Also all the principles in the next section involving quantifiers explain use of implications with hypothetical existence as premise.