Intuitionistic Logic

Origin. L.E.J. Brouwer founded mathematical intuitionism (1907-1920s), rejecting non-constructive existence proofs. Arend Heyting formalized intuitionistic logic (1930). Kolmogorov gave the "problem interpretation" (1932). Connected to computation via Curry-Howard: proofs are programs, propositions are types. Foundation for constructive mathematics and type-theoretic proof assistants.

Models. Constructive truth: a proposition is true only if we have a method to verify it. A proof of "A or B" must specify which; a proof of "there exists x" must provide a witness. Rejects non-constructive principles: you cannot prove existence by contradiction alone.

Formalism.

Syntax: Same as classical propositional/first-order logic: ¬, ∧, ∨, →, ∀, ∃.

Rejected principles:

Law of excluded middle: A ∨ ¬A (not valid)
Double negation elimination: ¬¬A → A (not valid)
Peirce's law: ((A → B) → A) → A (not valid)
¬¬∃x.P(x) → ∃x.P(x) (not valid)

Valid but classically equivalent forms that differ:

¬¬¬A ↔ ¬A (valid)
A → ¬¬A (valid, but converse not)
¬(A ∧ B) ↔ (A → ¬B) (valid)
De Morgan: ¬A ∨ ¬B → ¬(A ∧ B) is valid; the converse ¬(A ∧ B) → ¬A ∨ ¬B is not
De Morgan: ¬(A ∨ B) ↔ ¬A ∧ ¬B is valid in both directions

BHK Interpretation (Brouwer-Heyting-Kolmogorov):

A proof of A ∧ B is a pair (proof of A, proof of B)
A proof of A ∨ B is a tagged proof: either (left, proof of A) or (right, proof of B)
A proof of A → B is a function transforming proofs of A into proofs of B
A proof of ∀x.P(x) is a function giving a proof of P(a) for any a
A proof of ∃x.P(x) is a pair (witness a, proof of P(a))
There is no proof of ⊥ (falsity)
¬A means A → ⊥

Kripke semantics: A frame is a partial order (W, ≤) of states of information, with a valuation that is persistent: if w ⊩ p and w ≤ v then v ⊩ p.

w ⊩ A ∧ B iff w ⊩ A and w ⊩ B
w ⊩ A ∨ B iff w ⊩ A or w ⊩ B — decided at w itself, which is why excluded middle fails
w ⊩ A → B iff for every v ≥ w, if v ⊩ A then v ⊩ B
w ⊩ ¬A iff for every v ≥ w, v ⊮ A
w ⊩ ∀x.P(x) iff for every v ≥ w and every a in the domain of v, v ⊩ P(a)
w ⊩ ∃x.P(x) iff for some a in the domain of w, w ⊩ P(a) Persistence extends from atoms to all formulas: truth is never lost as information grows. The two-element chain refutes A ∨ ¬A: at the bottom neither disjunct holds.

Algebraic semantics: A Heyting algebra is a bounded lattice with a residual → satisfying c ≤ a → b iff c ∧ a ≤ b. Validity is truth-value 1 under every assignment in every Heyting algebra. Kripke frames are the special case of algebras of upward-closed sets; topological spaces give the case of open sets, with → the interior of the material conditional.

Symbols.

Symbol	Unicode	Name	Meaning
⊥	U+22A5	Up tack / Falsum	Absurdity; primitive, with ¬A defined as A → ⊥
⊤	U+22A4	Down tack / Verum	The top of a Heyting algebra; the designated value
¬	U+00AC	Not sign / Negation	Defined: ¬A is A → ⊥
∧	U+2227	Logical and / Conjunction	Meet in the Heyting algebra
∨	U+2228	Logical or / Disjunction	Join; not definable from ¬ and ∧ here
→	U+2192	Rightwards arrow / Implication	Relative pseudo-complement; the residual of ∧
↔	U+2194	Left right arrow / Biconditional	Interderivability in both directions
∀	U+2200	Universal quantifier	Constructive reading: a uniform method
∃	U+2203	Existential quantifier	Constructive reading: a witness plus a proof
⊢ᵢ	—	Intuitionistic derivability	Provable in IPC or in intuitionistic predicate logic
⊩	U+22A9	Forces	Kripke forcing at a state
⊮	U+22AE	Does not force	Failure of forcing at a state
≤	U+2264	Less-than or equal to	The information order on Kripke states; also the lattice order
≥	U+2265	Greater-than or equal to	Later states, in the forcing clauses for → and ¬
W	—	Set of states	The carrier of a Kripke frame
w, v	—	States of information	Points of a Kripke frame
A, B	—	Formula metavariables	Range over formulas

Metatheory. IPC is sound and complete for Heyting algebras (Rasiowa–Sikorski) and for Kripke frames (Kripke 1965), and it has the finite model property, so it is decidable; Statman (1979) showed derivability is PSPACE-complete, matching classical validity in complexity while differing in every other respect. The disjunction property — if ⊢ A ∨ B then ⊢ A or ⊢ B — holds, and with it the existence property for the predicate calculus; both fail classically, and the disjunction property is what makes the logic a plausible account of constructive assertion. Glivenko's theorem (1929) pins the exact gap at the propositional level: ⊢_CPC A iff ⊢_IPC ¬¬A, so classical and intuitionistic logic agree on negated formulas and IPC is not a weaker logic so much as a finer one. Gödel–Gentzen extends this to predicate logic and to arithmetic, giving a relative consistency proof of PA in HA. Gödel's □-translation embeds IPC into S4 faithfully. De Jongh's theorem says the propositional logic of Heyting arithmetic is exactly IPC, so arithmetic adds no propositional principles. Curry–Howard identifies IPC derivations with simply typed lambda terms, and normalization with cut elimination. First-order intuitionistic logic is undecidable, as in the classical case.

Applies to. Constructive mathematics. Type theory and proof assistants (Coq, Agda, Lean). Program extraction from proofs. Topos theory. Semantics of programming languages. Situations where computational content matters.

Limitations. There is no finite characteristic matrix: Gödel (1932) showed IPC is not the logic of any finite algebra, so no truth table decides it and the finite model property must be obtained frame by frame. The connectives are independent — ∨ and ∃ are not definable from the others, as they are classically — so there is no disjunctive or prenex normal form, and proof search cannot be reduced to a clausal one. The logic is not structurally complete: admissible rules properly exceed derivable ones, the Kreisel–Putnam and Harrop rules being the standard witnesses, so "adding a rule that preserves theoremhood" is not the same as adding a theorem. Decidability stops at the propositional level; intuitionistic predicate logic is undecidable even in the monadic fragment, where the classical logic is decidable. And the Kripke completeness theorem is not itself constructive — Kreisel showed that completeness for intuitionistic predicate logic implies Markov's principle — so the semantics that justifies the logic cannot be justified within it.