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 fails (right-to-left)

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: Worlds ordered by accessibility (information growth). A ∨ B true at world w iff A or B true at some accessible world where it's "decided."

Symbols.

Symbol	Unicode	Name	Meaning
⊥	U+22A5	Bottom/Falsity	Absurdity
¬A	—	Negation	A → ⊥
∧ ∨ →	—	Connectives	(as usual)
∀ ∃	—	Quantifiers	Constructive interpretation
⊢ᵢ	—	Intuitionistic derivation	Provable intuitionistically
≤	—	Information order	Kripke accessibility

Metatheory. Disjunction property: if ⊢ A ∨ B then ⊢ A or ⊢ B. Existence property: if ⊢ ∃x.P(x) then ⊢ P(t) for some term t. These fail classically. Gödel-Gentzen translation: classical logic embeds into intuitionistic via double-negation. Curry-Howard: intuitionistic proofs correspond to simply-typed lambda terms. Decidable for propositional case (PSPACE-complete). First-order intuitionistic logic is undecidable.

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. Many classical theorems unprovable without modification. Can't prove existence by contradiction. Some proofs become longer or more complex. Classical reasoning is "safe" (double-negation translation shows no inconsistency introduced), so intuitionistic logic is more demanding, not more permissive. Not all mathematicians accept the philosophical motivation.