Intuitionistic Logic

Intuitionistic logic is a system of logic that formalizes constructive reasoning: establishing a proposition requires appropriate evidence, rather than merely excluding its falsity. It provides a logical basis for constructive mathematics and differs from classical logic principally by not accepting unrestricted excluded middle or double-negation elimination. Its standard forms include propositional logic and first-order logic. These are proper subsystems of their classical counterparts: every intuitionistically provable formula is classically provable, but not conversely. (plato.stanford.edu)

Historical development

The subject arose from L. E. J. Brouwer’s early-twentieth-century intuitionism, which regarded mathematical objects as constructions rather than independently existing abstract entities. Brouwer challenged the unrestricted application of classical logical principles, especially to infinite collections. Arend Heyting published formal systems for intuitionistic propositional logic, predicate logic, and arithmetic in 1930, making these principles accessible to systematic mathematical investigation. (math.ucla.edu)

Heyting’s explanations of proof and Andrey Kolmogorov’s interpretation of propositions as problems contributed to the modern constructive interpretation. In 1932, Kolmogorov described logical operations in terms of problems and their solutions. The resulting proof interpretation became known as the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation. The formal logic can be studied independently of adopting Brouwer’s broader philosophical position. (plato.stanford.edu)

Constructive meaning of the connectives

The BHK interpretation explains logical operations through what counts as a proof:

• A proof of $A\land B$ supplies both a proof of $A$ and a proof of $B$.
• A proof of $A\lor B$ supplies a proof of one specified alternative, together with an indication of which alternative was established.
• A proof of $A\to B$ supplies a construction transforming any proof of $A$ into a proof of $B$.
• A proof of $\exists x\,P(x)$ supplies a witness and a proof that it satisfies $P$.
• A proof of $\forall x\,P(x)$ supplies a uniform construction producing a proof of $P(x)$ for an arbitrary object in the domain. (plato.stanford.edu)

Negation is understood as implication to absurdity:

Thus, proving $\neg A$ means showing that a proof of $A$ would yield a contradiction. It does not mean merely that no proof of $A$ is currently known. Standard intuitionistic logic retains the principle of explosion, $\bot\to B$, allowing any proposition to follow from absurdity. (cs.cornell.edu)

Differences from classical reasoning

The law of excluded middle,

is not a general intuitionistic theorem. Its constructive interpretation would require establishing one alternative for an arbitrary proposition. Nevertheless, excluded middle holds for propositions whose alternatives can constructively be decided; its omission is not a claim that every particular instance fails. Adding it as an unrestricted axiom schema recovers classical logic. (plato.stanford.edu)

Likewise, double-negation elimination, $\neg\neg A\to A$, is not generally valid. An argument showing that the impossibility of $A$ leads to contradiction need not supply evidence for $A$. However, $A\to\neg\neg A$ remains valid. Proof by contradiction therefore still establishes a negation when assuming its target leads to absurdity; what is unavailable is unrestricted elimination of the resulting double negation. (plato.stanford.edu)

Formal proof systems

Intuitionistic logic admits axiomatic presentations, natural deduction, and sequent calculus. Natural deduction specifies introduction and elimination rules for each connective. For example, deriving $B$ under an assumption $A$ permits deriving $A\to B$ while discharging that assumption. Implication elimination is modus ponens: from $A$ and $A\to B$, infer $B$. (cs.cmu.edu)

In the standard intuitionistic sequent calculus, a judgment has the form

where $\Gamma$ collects assumptions and the right-hand side contains a single conclusion. This contrasts with the multiple-conclusion formulation of classical sequent calculus. Such systems provide structured methods for automated proof search and the study of derivations. (cs.cmu.edu)

Semantic models

Algebraically, intuitionistic propositional logic is interpreted in Heyting algebras. These are bounded distributive lattices with an implication operation satisfying

Boolean algebras are special cases, corresponding to classical logic. In a general Heyting algebra, a proposition joined with its negation need not equal the greatest element. (mikeshulman.github.io)

A concrete interpretation comes from open sets in a topological space. Conjunction is intersection, disjunction is union, and negation is the interior of the complement. Consequently, double negation need not return the original open set. (mikeshulman.github.io)

Kripke semantics instead uses ordered stages of information. Once a proposition is forced at a stage, it remains forced at later stages. An implication holds when every later stage forcing its antecedent also forces its consequent. Crucially, not forcing $A$ at a stage is different from forcing $\neg A$. These models give soundness and completeness results for intuitionistic logic. (plato.stanford.edu)

Proofs and computation

Through the Curry–Howard correspondence, propositions correspond to types and proofs to programs. Implication corresponds to a function type, conjunction to a product type, and disjunction to a tagged sum type. Applying an implication proof to evidence for its antecedent corresponds to function application. (cs.cmu.edu)

This connection links intuitionistic logic to type theory and the design of programming languages. Constructive existential proofs carry witnesses, while proofs of disjunction carry an identified alternative. Proof reduction supplies a computational interpretation of logical derivations, allowing reasoning systems to treat evidence as structured, executable objects rather than only as assertions of truth. (cs.cmu.edu)