Intuitionistic logic
Intuitionistic logic is a formal system of symbolic logic that differs from classical logic by rejecting the law of the excluded middle (A ∨ ¬A) and the principle of double negation elimination (¬¬A → A), instead requiring constructive proofs for the validity of statements, particularly for existential claims and disjunctions.[1] It was developed to formalize the principles of mathematical intuitionism, a philosophy initiated by L.E.J. Brouwer in his 1907 doctoral dissertation Over de grondslagen der wiskunde, where he argued that mathematics is a mental construct independent of language and logic, emphasizing that truth arises from effective constructions rather than abstract existence.[2] Brouwer's views, further elaborated in his 1908 paper "The Unreliability of the Logical Principles," led to the rejection of non-constructive proofs like reductio ad absurdum without providing a positive construction.[3] The formalization of intuitionistic logic was achieved by Brouwer's student Arend Heyting in a series of papers published in 1930, titled Die formalen Regeln der intuitionistischen Logik, which provided axiomatic systems for both propositional and predicate intuitionistic logic.[4] These systems include standard connectives such as conjunction (∧), disjunction (∨), implication (→), and negation (¬), but interpret them constructively: for instance, a proof of A ∨ B requires a proof of A or B, not merely the assumption that one must hold.[1] Independently, Andrey Kolmogorov contributed in 1925 with his paper "On the Principle of the Excluded Middle," interpreting intuitionistic connectives in terms of problem-solving, which aligned with Brouwer's ideas and later formed part of the Brouwer-Heyting-Kolmogorov (BHK) interpretation.[5] The BHK interpretation defines a proof of a disjunction as a proof of one disjunct, a proof of implication as a method transforming proofs of the antecedent into the consequent, and negation as a construction leading to a contradiction.[6] Key differences from classical logic lie in its constructivism: while classical logic accepts the law of excluded middle as an axiom, allowing proofs by contradiction without construction, intuitionistic logic views such methods as invalid for establishing positive existence.[3] This results in intuitionistic logic being strictly weaker than classical logic, as shown by Gödel's 1932 translation embedding classical propositions into intuitionistic ones, and it has implications for mathematics, such as the intuitionistic continuum being non-Archimedean due to Brouwer's principle of continuous choice.[1] Despite these differences, intuitionistic logic retains core principles like the law of non-contradiction (¬(A ∧ ¬A)) and ex falso quodlibet (⊥ → A).[1] Its development influenced proof theory, with Gerhard Gentzen providing natural deduction systems in 1935 that highlighted its structural properties.[7]Overview and History
Core Definition and Motivation
Intuitionistic logic is a formal system of deductive reasoning that emphasizes constructive proofs, wherein the truth of a proposition is established only through an explicit construction of the mathematical object it describes, rather than merely by demonstrating non-contradiction.[7] Unlike classical logic, it rejects the law of excluded middle, according to which every proposition A satisfies A \vee \neg A, meaning that in intuitionistic logic, this disjunction is not generally provable.[7] It also forgoes double negation elimination, such that while A implies \neg\neg A, the converse—provability of \neg\neg A implying A—does not hold, though the reverse implication is valid in classical systems.[7] The primary motivation for intuitionistic logic stems from the demand in constructive mathematics for proofs that actively build mathematical entities, contrasting with classical logic's acceptance of indirect proofs, such as reductio ad absurdum, which establish existence by assuming the opposite and deriving a contradiction.[7] This approach ensures that assertions of existence are backed by verifiable constructions, aligning reasoning with effective computability and avoiding non-constructive methods that rely on infinite or idealized processes.[7] A representative example illustrates this distinction: to intuitionistically prove the existence of a natural number n such that P(n) holds for some property P, one must explicitly construct such an n and verify P(n), whereas a classical proof might suffice by showing that assuming no such n exists leads to absurdity, without providing the instance.[7]Historical Development
Intuitionistic logic emerged from L.E.J. Brouwer's foundational work in the philosophy of mathematics, beginning with his 1907 doctoral dissertation Over de grondslagen der wiskunde, where he rejected the law of excluded middle as a non-constructive principle and emphasized mental constructions as the basis of mathematical truth.[8] This philosophical stance laid the groundwork for intuitionism, influencing the development of a distinct logical system that prioritizes constructive proofs over existential assumptions inherent in classical logic. A key early milestone came in 1925 when Andrei Kolmogorov critiqued the redundancy of classical logic's law of excluded middle in his paper "On the Principle of the Excluded Middle," providing the first partial formalization of intuitionistic propositional logic and interpreting it as the logic of problem-solving schemes rather than absolute truths.[9] Building on Brouwer's ideas, Arend Heyting formalized intuitionistic logic in 1930 through a Hilbert-style axiomatic system in his paper "Die formalen Regeln der intuitionistischen Logik," which systematically captured the inference rules consistent with constructive mathematics.[1] In 1932, Kurt Gödel advanced the field with his double negation translation, embedding intuitionistic propositional logic into classical modal logic S4 and demonstrating that intuitionistic theorems correspond to classically provable sentences under double negation, thus establishing a precise relationship between the two systems.[10] The mid-20th century saw further evolution through the influences of Russian constructivism (e.g., Andrey Markov Jr.) and recursion theory (e.g., Stephen Kleene), which developed recursive and computable interpretations of intuitionistic principles, emphasizing effective procedures in logic and arithmetic during the 1950s and 1960s.[11] A significant semantic breakthrough occurred in 1965 when Saul Kripke introduced Kripke models, providing a possible-worlds semantics for intuitionistic logic that models truth as monotonically increasing over time-like stages of knowledge, proving completeness relative to Heyting's system.[12] This shifted intuitionistic logic from a purely philosophical rejection of non-constructive principles to a rigorous, semantically grounded system. In the 21st century, intuitionistic logic maintains its relevance in computer science, particularly through proof assistants like Coq, which originated in the 1990s as an implementation of the Calculus of Inductive Constructions—a type theory extension of intuitionistic logic developed by Thierry Coquand and others for formal verification.[13] However, no major axiomatic changes have occurred since the 1980s, with developments focusing instead on applications in automated reasoning and constructive mathematics.Philosophical Foundations
Brouwer's Intuitionism
L.E.J. Brouwer's intuitionism posits mathematics as a subjective mental activity rooted in the primordial intuition of time, where all mathematical objects and proofs must arise from constructive processes within the human mind. Central to this view is the rejection of actual infinity, treating infinity only as a potential process of ongoing construction rather than a completed totality, and the dismissal of the law of the excluded middle (LEM) as non-constructive, since it asserts that every proposition is either true or false without requiring an explicit mental construction to verify one or the other. Brouwer argued that mathematical truth resides in the inner experience of construction, independent of external language or symbols, emphasizing the "two-ity" derived from the intuition of time as the foundation for all mathematics.[14] In his 1907 doctoral dissertation, Over de Grondslagen der Wiskunde (On the Foundations of Mathematics), Brouwer introduced choice sequences as infinite sequences generated by free, lawless choices at each step, serving as the basis for an intuitionistic reconstruction of the continuum. These sequences allow real numbers to be defined dynamically through mental acts, avoiding the classical view of the continuum as a pre-existing set of points, and instead portraying it as a medium of individual point-cores emerging from subjective constructions. The dissertation also critiques Hilbert's formalism for reducing mathematics to meaningless symbol manipulation devoid of intuitive content, and Russell's logicism for erroneously subordinating mathematics to a rigid logical framework that presupposes non-constructive principles. Brouwer contended that both approaches fail to ground mathematics in genuine intuition, leading to unreliable foundational claims.[14] During the 1920s, Brouwer engaged in heated debates with formalists, particularly David Hilbert, over the nature of mathematical foundations, culminating in the Brouwer-Hilbert controversy and the 1928 "Annalen Affair," where Brouwer was removed from the editorial board of the Mathematische Annalen after protesting Hilbert's influence. In his 1928 address "Intuitionism and Formalism," Brouwer reiterated that exactness in mathematics exists only in the human intellect, not in formal symbols, and accused formalism of ignoring the subjective origin of mathematical creation. A key idea in his theory of choice sequences is the continuity principle, which posits that functions on choice sequences depend continuously on their initial segments, ensuring constructive uniformity in infinite processes without assuming completed infinities.[1] Brouwer's ideas profoundly influenced the formalization of intuitionistic logic by his student Arend Heyting, who in 1930 provided a precise axiomatic system capturing intuitionistic principles, thereby making them accessible for rigorous study. However, Brouwer viewed such formalizations as secondary tools at best, rejecting their rigidity as an imposition of language that could distort the fluid, intuitive essence of mathematics, and he considered them largely pointless for true intuitionistic practice.[1][15]Constructive Mathematics
Constructive mathematics requires that every proof of existence provides an explicit algorithm or construction for the object in question, ensuring that mathematical statements are verifiable through effective methods rather than non-constructive assumptions. This approach aligns closely with intuitionistic logic, where the existential quantifier demands a witness that can be computed or described finitistically, rejecting indirect proofs based on contradiction alone. Influenced by Brouwer's intuitionism, constructive mathematics emphasizes the primacy of finite constructions in building mathematical knowledge.[16] A cornerstone of modern constructive mathematics is Errett Bishop's program, outlined in his 1967 book Foundations of Constructive Analysis, which demonstrates that a significant portion of classical analysis can be reconstructed using intuitionistic logic without loss of utility for practical mathematics. Bishop's framework, often denoted as BISH, treats the positive integers as the foundational building blocks and develops concepts like sequences and functions through algorithms that operate on these integers. Complementing this, the Russian school of constructive mathematics, founded by Andrey A. Markov Jr. in the late 1940s, focuses on recursive constructions grounded in computability theory, as formalized in the system RUSS; this school integrates Markov's principle to allow limited non-constructive steps while maintaining recursive realizability for proofs.[16][17] In constructive mathematics, real numbers are typically defined as equivalence classes of Cauchy sequences of rational numbers equipped with a modulus of convergence, which provides an explicit rate ensuring the sequence's terms get arbitrarily close; this modulus guarantees computability, unlike classical definitions that may rely on non-uniform convergence. For instance, the intermediate value theorem, which classically asserts that a continuous function on a closed interval taking values of opposite signs must cross zero, fails in its full form constructively unless the function is uniformly continuous, requiring an algorithm to locate the root within specified precision rather than merely proving its existence.[16] The absence of the law of excluded middle (LEM) in constructive mathematics leads to the failure of certain classical theorems that depend on exhaustive case analysis. For example, while classical logic proves that every real-valued function on the reals is either continuous at some point or discontinuous everywhere, this dichotomy cannot be established constructively, as it would require deciding undecidable properties for arbitrary functions without explicit constructions. Similarly, statements like "every vector space has a basis" or "for any given Turing machine and input, it either halts or runs forever indefinitely" rely on non-constructive principles like the axiom of choice or LEM that are inadmissible here, highlighting how constructive approaches prioritize effective proofs over existential completeness.[16]Syntax
Propositional Connectives
In propositional intuitionistic logic, the primitive connectives are implication (→), conjunction (∧), disjunction (∨), and negation (¬).[7] There is no primitive truth constant (⊤), though it can be defined if needed (e.g., ⊤ ≡ ¬⊥, with falsehood ⊥ defined as an absurdity such as p ∧ ¬p for atomic p).[7] These connectives were formalized by Arend Heyting in his axiomatic system for intuitionistic logic.[7] Well-formed formulas (wffs) are constructed recursively from a countable set of atomic propositions, denoted by variables such as p, q, r, using the connectives and parentheses for grouping.[7] Specifically, atomic propositions are wffs; if A and B are wffs, then so are (A \wedge B), (A \vee B), (A \to B), and \neg A; falsehood \bot may be introduced as a defined constant representing contradiction.[7] This recursive definition ensures all formulas are finitely structured, mirroring the constructive emphasis of the logic.[18] Intuitively, the connectives capture constructive proofs rather than mere truth values.[7] A proof of A \wedge B provides explicit constructions for both A and B; a proof of A \to B yields a method to construct a proof of B given any proof of A; a proof of A \vee B specifies which of A or B is constructively verified; and a proof of \neg A constructs a contradiction from any proof of A.[7] These interpretations align with the Brouwer-Heyting-Kolmogorov (BHK) view of proofs as constructive objects.[7] Unlike classical propositional logic, where double negation elimination (\neg\neg A \to A) holds as a theorem, intuitionistic logic rejects it, ensuring that proofs remain constructive and rejecting non-constructive principles like the law of excluded middle (A \vee \neg A).[7] This treatment of negation highlights the logic's focus on effective constructions over bivalent truth.[7]Predicate Logic Extensions
In first-order intuitionistic logic, the syntax extends the propositional framework by incorporating a signature consisting of constant symbols, function symbols, and predicate symbols (of various arities), along with terms and quantified formulas to reason about objects and relations. Terms are constructed recursively from variables (denoted x, y, z, \dots), constants (c), and function applications: if f is an n-ary function symbol and t_1, \dots, t_n are terms, then f(t_1, \dots, t_n) is a term.[19] Atomic formulas are obtained by applying predicate symbols to terms: if P is an n-ary predicate symbol and t_1, \dots, t_n are terms, then P(t_1, \dots, t_n) is an atomic formula. Complex formulas are then formed by closing under the propositional connectives—such as conjunction (\wedge), disjunction (\vee), implication (\to), and negation (\neg)—applied to atomic or previously formed formulas, as well as by the universal quantifier \forall and existential quantifier \exists: if A is a formula and x a variable, then \forall x \, A and \exists x \, A are formulas.[19] Examples include \forall x \, P(x) and \exists x \, (P(x) \wedge Q(x)), where P and Q are predicates.[20] Variables in formulas are classified as free or bound: an occurrence of x is bound if it lies within the scope of a matching quantifier \forall x or \exists x, and free otherwise. Formulas are considered equivalent up to \alpha-conversion, which systematically renames bound variables without altering meaning (e.g., \forall x \, P(x) is \alpha-equivalent to \forall y \, P(y)). Substitution of a term t for a free variable x in a formula A, denoted A[t/x], is defined recursively while ensuring that no variable in t becomes inadvertently bound.[19] From a constructive perspective, the universal quantifier \forall x \, A(x) intuitively demands a uniform method of construction that, given any specific x, produces a proof of A(x), reflecting the need for generality applicable to all instances without exhaustive verification.[1] In contrast, the existential quantifier \exists x \, A(x) requires exhibiting a particular witness x_0 (or a method to construct one) along with a proof that A(x_0) holds, emphasizing explicit evidence of existence.[1] The complete grammar for well-formed formulas thus unifies these predicate elements with propositional connectives, allowing nested expressions such as \neg \forall x \, P(x), which aligns syntactically with forms involving existential negation like \exists x \, \neg P(x) in the broader language.[20]Deductive Systems
Hilbert-Style Calculi
Hilbert-style calculi provide a foundational axiomatic approach to intuitionistic logic, emphasizing a finite set of axiom schemas and inference rules to derive theorems from assumptions. These systems, pioneered in the early 20th century and refined for intuitionistic purposes, treat logical connectives through implication-based schemas, avoiding classical principles like the law of the excluded middle. A standard formulation for intuitionistic propositional logic, known as H–IPC, consists of the following axiom schemas, along with the inference rule of modus ponens: from A and A \to B, infer B [Kleene 1952, §33; as detailed in Moschovakis 2023]. The core propositional axioms are: \begin{align*} &1.\ A \to (B \to A) \\ &2.\ (A \to B) \to ((A \to (B \to C)) \to (A \to C)) \\ &3.\ A \to (B \to (A \land B)) \\ &4.\ (A \land B) \to A \\ &5.\ (A \land B) \to B \\ &6.\ A \to (A \lor B) \\ &7.\ B \to (A \lor B) \\ &8.\ (A \to C) \to ((B \to C) \to ((A \lor B) \to C)) \end{align*} These schemas capture the behaviors of implication (\to), conjunction (\land), and disjunction (\lor) in a constructive manner, ensuring that proofs build explicit constructions rather than relying on indirect assumptions [Kleene 1952, §33; Moschovakis 2023]. Negation (\neg) is treated definitionally as \neg A \equiv A \to \bot, where \bot denotes falsehood (often realized as an atomic contradiction with no introduction rule). To handle negation constructively, two additional axioms are included: \begin{align*} &9.\ (A \to B) \to ((A \to \neg B) \to \neg A) \\ &10.\ \neg A \to (A \to B) \end{align*} These prevent the derivation of double negation elimination (\neg \neg A \to A) while allowing ex falso quodlibet (from \bot, infer any B) as a derived rule [Kleene 1952, §33; Moschovakis 2023]. For intuitionistic predicate logic (H–IQC), the propositional axioms remain, augmented by quantifier axioms and rules to manage variables and substitutions properly. The quantifier axioms are: \begin{align*} &11.\ \forall x\, A(x) \to A(t) \quad (\text{where } t \text{ is free for } x \text{ in } A(x)) \\ &12.\ A(t) \to \exists x\, A(x) \quad (\text{where } t \text{ is free for } x \text{ in } A(x)) \end{align*} Inference rules extend modus ponens with universal generalization: from C \to A(x) (where x is not free in C), infer C \to \forall x\, A(x); and existential elimination: from A(x) \to C (where x is not free in C), infer \exists x\, A(x) \to C [Kleene 1952, §33; Moschovakis 2023]. A key derived principle is the axiom schema \forall x\, (A \to B) \to (A \to \forall x\, B) when x is not free in A, which follows from the generalization rule and supports monotonicity of universal quantification under intuitionistic constraints [Kleene 1952, §34; Moschovakis 2023]. No primitive equivalence rules are included; equivalences such as A \leftrightarrow B \equiv (A \to B) \land (B \to A) are derived from the implication and conjunction axioms [Kleene 1952, §33; Moschovakis 2023]. This system ensures soundness and completeness with respect to Kripke semantics, though metatheoretic details lie beyond the axiomatic presentation here.Sequent and Natural Deduction
Sequent calculus provides a formal system for intuitionistic logic through Gentzen's LJ framework, where proofs are constructed as trees of sequents of the form Γ ⊢ Δ, with Γ and Δ being multisets of formulas, but restricted in intuitionistic logic to having at most one formula in Δ to avoid classical implications. This system includes structural rules such as weakening, which allows adding a formula to the antecedent or succedent without affecting provability (e.g., from Γ ⊢ Δ infer Γ, A ⊢ Δ), and contraction, which merges duplicate formulas in the antecedent (e.g., from Γ, A, A ⊢ Δ infer Γ, A ⊢ Δ).[21] Logical rules operate on connectives; for instance, the right introduction for implication is: from Γ, A ⊢ B infer Γ ⊢ A → B, while the left introduction for disjunction is: from Γ, A, B ⊢ C infer Γ, A ∨ B ⊢ C. Intuitionistic restrictions exclude classical rules like right weakening for negation, ensuring that negated formulas do not behave as in classical logic.[21] For quantifiers in sequent calculus, the universal introduction on the right requires that the eigenvariable x does not occur free in the antecedent Γ or in the succedent formula, yielding from Γ ⊢ A(x) infer Γ ⊢ ∀x A(x), while existential elimination on the left uses a similar freshness condition to prevent non-constructive inferences. These rules align with intuitionistic principles by enforcing constructivity in variable handling. Natural deduction offers an alternative proof system for intuitionistic logic, often presented in tree or Fitch-style formats, where derivations build from assumptions to conclusions using introduction and elimination rules for each connective.[22] Gentzen's original formulation, known as NJ, includes rules such as implication introduction, which discharges an assumption A to derive A → B from a subproof assuming A and concluding B, and universal elimination, which instantiates ∀x A(x) to A(t) for any term t. Intuitionistic natural deduction includes an elimination rule for absurdity (⊥) that allows inferring any formula A (ex falso quodlibet), similar to classical systems, while preserving constructivity since no proof can construct ⊥.[21][7] Quantifier rules in natural deduction follow Barcan-like principles adapted for intuitionism: universal introduction requires proving A(x) under assumptions where x is an eigenvariable not free in any undischarged assumptions, ensuring the proof is parametric in x. Sequent calculus facilitates cut-elimination, Gentzen's Hauptsatz, which transforms proofs into cut-free forms to establish consistency and subformula properties, while natural deduction better mirrors informal mathematical reasoning through its assumption-discharge mechanism.Semantics
Heyting Algebra Models
A Heyting algebra is a bounded lattice equipped with a binary implication operation \to that satisfies the adjunction property: for all elements a, b, c, a \leq (b \to c) if and only if a \wedge b \leq c.[23] Equivalently, the implication b \to c is defined as the greatest element x such that x \wedge b \leq c, known as the relative pseudocomplement.[24] This structure generalizes Boolean algebras, which correspond to classical logic, by omitting the requirement that every element is complemented in a way that enforces the law of excluded middle.[23] In the algebraic semantics of intuitionistic propositional logic, a Heyting algebra H serves as a model where propositional variables are interpreted as elements of H, and compound formulas are evaluated using the lattice operations. Specifically, the conjunction \wedge is interpreted as the meet, disjunction \vee as the join, implication \to as the relative pseudocomplement, falsehood \bot as the bottom element $0, and negation \neg A as A \to 0.[24] A formula is valid in H if its interpretation equals the top element \top under any assignment. This provides a static, lattice-based validation of intuitionistic inferences, contrasting with dynamic possible-worlds approaches.[25] For intuitionistic predicate logic, the semantics extends to generalized Heyting algebras, where the domain of discourse is fixed, predicates are mapped to elements of the algebra, and the universal quantifier \forall x \, \phi(x) is interpreted as the infimum (greatest lower bound) over the domain of the interpretations of \phi(x).[26] The existential quantifier is dually defined using the supremum. This algebraic framework ensures that quantifiers preserve the intuitionistic principles, such as monotonicity under implication.[27] The Heyting algebra semantics is both sound and complete for intuitionistic propositional logic: a formula is provable if and only if it is valid in every Heyting algebra.[24] This result, originally established in the 1950s through algebraic methods, also extends to predicate logic via complete Heyting-valued models.[28]Kripke Frame Semantics
Kripke frame semantics, introduced by Saul Kripke, offers a possible-worlds model for intuitionistic logic that captures the idea of knowledge evolving over time through a partial order on worlds.[29] A Kripke frame is a pair (W, \leq), where W is a nonempty set of worlds and \leq is a reflexive and transitive partial order, reflecting stages where information at earlier worlds is preserved or extended in later ones.[7] The valuation function V assigns to each atomic proposition p and world w \in W a truth value such that it is monotone: if w \leq w' and V(p, w) = \top, then V(p, w') = \top.[29] This monotonicity ensures that once a proposition becomes true at a world, it remains true in all accessible future worlds, modeling the persistence of verified knowledge in intuitionistic reasoning.[7] The semantics is defined via a forcing relation \Vdash between worlds and formulas. For propositional connectives, the clauses are as follows:- w \Vdash A \land B if and only if w \Vdash A and w \Vdash B;
- w \Vdash A \lor B if and only if w \Vdash A or w \Vdash B;
- w \Vdash A \to B if and only if for all w' \geq w, if w' \Vdash A then w' \Vdash B;
- w \Vdash \neg A if and only if for all w' \geq w, w' \not\Vdash A;
- w \Vdash \bot never holds.[29]
- w \Vdash \forall x \, A(x) if and only if for every w' \geq w and every d \in D(w'), w' \Vdash A(d);
- w \Vdash \exists x \, A(x) if and only if there exists d \in D(w) such that w \Vdash A(d).[7]