Intuitionistic Logic — Mathematics Knowledge System

Overview

Intuitionistic logic, formalized by Arend Heyting in 1930 to capture L. E. J. Brouwer's constructivist philosophy of mathematics, rejects the law of excluded middle (φ ∨ ¬φ) as a universally valid principle, along with double-negation elimination (¬¬φ → φ), demanding instead that every proof of a disjunction φ ∨ ψ explicitly exhibit which disjunct holds, and every proof of an existential ∃x φ(x) explicitly exhibit a witness. Classically, φ ∨ ¬φ is true regardless of whether anyone can decide which disjunct holds — it is simply guaranteed by the two-valued semantics of truth tables — but intuitionistically, asserting φ ∨ ¬φ means possessing an actual method that either proves φ or proves ¬φ, and for many undecided mathematical statements no such method is known to exist, so the disjunction is not intuitionistically assertable. This gives intuitionistic logic a computational, constructive reading formalized precisely by the Curry–Howard correspondence, under which intuitionistic proofs correspond exactly to programs (terms in typed lambda calculus) and propositions correspond to types — a proof of φ → ψ literally IS a program transforming any witness of φ into a witness of ψ. Intuitionistic logic is strictly weaker than classical logic (every intuitionistically provable formula is classically provable, but not conversely) and is the logic underlying constructive mathematics and proof assistants such as Coq and Agda.

Intuition

Classical logic treats every proposition as simply 'true' or 'false' in some Platonic sense, whether or not anyone can ever find out which — so φ ∨ ¬φ is automatically true by the definition of a two-valued truth table, no proof of either disjunct required. Intuitionistic logic instead reads a proof of φ ∨ ψ as a recipe that actually produces either a proof of φ or a proof of ψ (and tells you which one), and reads a proof of ∃x φ(x) as a recipe that actually produces a specific witness a together with a proof of φ(a) — no 'proof by cases with no method to decide which case' and no 'nonconstructive existence proof' are allowed. Under this lens, proof by contradiction is exactly where the two logics part ways: from ¬¬φ, classical logic lets you conclude φ outright, but intuitionistically all you're licensed to say is that assuming ¬φ leads to absurdity — which is NOT yet a construction of φ itself, so ¬¬φ → φ is intuitionistically invalid even though φ → ¬¬φ remains perfectly valid in both logics.

Formal Definition

Definition

Intuitionistic propositional logic keeps all the usual connectives but drops classically valid principles that assert existence/decidability without constructing a witness:

\not\vdash_{\mathrm{int}} \varphi \vee \neg \varphi \qquad \text{(law of excluded middle, not intuitionistically valid in general)}

Excluded middle fails intuitionistically

\not\vdash_{\mathrm{int}} \neg\neg \varphi \rightarrow \varphi \qquad \text{(double-negation elimination fails)}

Double-negation elimination fails intuitionistically

\vdash_{\mathrm{int}} \varphi \rightarrow \neg\neg \varphi \qquad \text{(but this direction always holds)}

Only one direction of double negation is intuitionistically valid

\vdash_{\mathrm{cl}} \varphi \iff \vdash_{\mathrm{int}} \neg\neg \varphi \qquad \text{(Glivenko's theorem, propositional case)}

Classical provability equals intuitionistic double-negation provability

Worked Examples

Consider √2^√2. Classically, either it is rational or it is irrational — excluded middle guarantees one of these two cases holds, with no need to determine which.
$\sqrt{2}^{\sqrt{2}} \text{ is rational} \ \vee\ \sqrt{2}^{\sqrt{2}} \text{ is irrational}$
Case 1: if √2^√2 is rational, take a=b=√2 — done, a^b is rational as required.
$\text{Case 1: } a = b = \sqrt{2} \implies a^b = \sqrt{2}^{\sqrt{2}} \in \mathbb{Q}$
Case 2: if √2^√2 is irrational, take a=√2^√2 (irrational) and b=√2, then a^b = (√2^√2)^√2 = √2^2 = 2, a rational number.
$\text{Case 2: } a = \sqrt{2}^{\sqrt{2}},\ b=\sqrt{2} \implies a^b = \sqrt{2}^{2} = 2 \in \mathbb{Q}$
Either way some pair (a,b) works — but the classical proof never determines WHICH case actually holds, so it never exhibits an explicit witness pair.
$\exists\, a, b \text{ irrational with } a^b \in \mathbb{Q}$

Answer: The proof is classically valid (it only uses excluded middle) but intuitionistically unacceptable as given, because it proves an existential statement without constructing or identifying an actual witness pair — it merely shows that one of two candidate pairs must work, without determining which. (An intuitionistically acceptable proof does exist, e.g. taking a=√2, b=2log₂3, but it requires additional constructive work.)

Practice Problems

Difficulty 4/10

Which classical tautology is intuitionistically invalid: (a) φ → φ, (b) φ ∨ ¬φ, (c) φ → (ψ → φ)?

Difficulty 5/10

Is φ → ¬¬φ intuitionistically valid? Justify briefly.

Difficulty 7/10

Explain the Curry–Howard correspondence's reading of intuitionistic implication φ → ψ, and why this reading fails for classical logic's double-negation elimination.

Quiz

Summary

Intuitionistic logic (Heyting, 1930, formalizing Brouwer's constructivism) rejects the law of excluded middle and double-negation elimination as universally valid, requiring proofs of disjunctions and existentials to exhibit an explicit witness.
Only φ → ¬¬φ holds intuitionistically in general, not the converse ¬¬φ → φ; excluded middle is intuitionistically irrefutable (¬¬(φ∨¬φ) is provable) but not assertable outright.
The Curry–Howard correspondence gives intuitionistic proofs a direct computational reading — proofs are programs, propositions are types — making intuitionistic logic the foundation of constructive mathematics and proof assistants like Coq and Agda.

References

WebsiteWikipedia — Intuitionistic logic
WebsiteWikipedia — Curry–Howard correspondence