Categorical logic · The Lumenary

Lens

MotivationH

One law, three readings

Here are three facts from three different subjects.

Programming. A function of two arguments is the same thing as a function that takes the first argument and returns a function of the second. Every functional programmer meets this as currying.
Logic. From hypotheses $C$ and $A$ you can prove $B$ exactly when from $C$ alone you can prove $A \to B$ . This is the deduction theorem.
Sets. Maps $C \times A \to B$ correspond bijectively to maps $C \to B^A$ , where $B^A$ is the set of all functions $A \to B$ .

They are one fact:

\Hom(C \times A,\, B) \;\cong\; \Hom(C,\, B^A).

The functor $- \times A$ has a right adjoint $(-)^A$ . Read in a category of types and programs, this is currying. Read in a poset of propositions ordered by provability, it is the deduction theorem $C \wedge A \vdash B \iff C \vdash A \to B$ . Read in $\mathbf{Set}$ , it is the exponential law. Categorical logic studies this coincidence systematically. Connectives and quantifiers are characterised by universal properties, a logic is interpreted in any category that has the matching structure, and proofs become morphisms. William Lawvere's slogan from 1969 is that the logical operations are adjoint functors.

Two payoffs make the subject worth learning. First, a single definition (soundness in a category with structure) gives at once the set-theoretic semantics, the topological semantics, Kripke semantics, sheaf semantics and the semantics of programs. Second, the categorical view explains which logical laws hold and why. Excluded middle, for instance, is not a law of every reasonable logic. It is a special property of Boolean models, and it fails in the open sets of the real line.

IntuitionH

The dictionary

The Curry–Howard–Lambek correspondence lines up three languages:

Logic	Type theory	Category
proposition $A$	type $A$	object $A$
proof of $B$ from $A$	term $x : A \vdash t : B$	morphism $A \to B$
cut, substituting a proof	substitution $t[u/x]$	composition
truth $\top$	unit type $1$	terminal object
conjunction $A \wedge B$	product type $A \times B$	product
implication $A \to B$	function type $A \to B$	exponential $B^A$
falsity $\bot$ , disjunction $\vee$	empty type, sum type	initial object, coproduct
proof simplification	β-reduction	equations between morphisms
$\exists x$ , $\forall x$	$\Sigma$ -, $\Pi$ -types	left and right adjoints to pullback

Two ways of forgetting will matter. If you remember only whether $B$ is provable from $A$ and forget which proof, the category becomes a preorder. Identify interderivable propositions and you get a poset. In a poset, products are meets, coproducts are joins and exponentials are implications, so a cartesian closed poset with finite joins is exactly a Heyting algebra. If instead you keep the proofs, you get a genuine category in which different proofs of the same statement are different arrows, and β-reduction says when two proofs are "the same".

The exponential: every

f : C \times A \to B

factors as

\mathrm{ev} \circ (\Lambda f \times \id_A)

for exactly one

\Lambda f : C \to B^A

, the curried form of

f

DefinitionsH

Definitions

Throughout, the learner is assumed to know adjunctions, products and terminal objects and the basics of type theory and propositions as types.

Definition— cartesian closed category

A category $\mathcal{C}$ is cartesian closed (a CCC) if it has a terminal object $1$ , binary products $A \times B$ , and for every object $A$ the functor $- \times A : \mathcal{C} \to \mathcal{C}$ has a right adjoint $(-)^A$ . Equivalently, for all $A, B$ there are an object $B^A$ and a morphism $\mathrm{ev} : B^A \times A \to B$ such that for every $f : C \times A \to B$ there is a unique $\Lambda f : C \to B^A$ with $\mathrm{ev} \circ (\Lambda f \times \id_A) = f$ .

Definition— Heyting algebra

A Heyting algebra is a lattice $H$ with a least element $\bot$ and a greatest element $\top$ , together with a binary operation $\Rightarrow$ such that for all $a, b, c$ :

c \le (a \Rightarrow b) \quad\iff\quad c \wedge a \le b.

The pseudo-complement is $\neg a := a \Rightarrow \bot$ , the largest element whose meet with $a$ is $\bot$ . A Heyting algebra is Boolean if $a \vee \neg a = \top$ for all $a$ (equivalently, $\neg\neg a = a$ for all $a$ ).

In categorical terms, a Heyting algebra is a poset that is cartesian closed (finite meets and implications) and has finite coproducts (finite joins). The defining law says precisely that $- \wedge a \dashv a \Rightarrow -$ .

Definition— simply typed λ-calculus with products

Types are generated by a base type $o$ , the unit type $1$ , products $A \times B$ and function types $A \to B$ . A context is a list $\Gamma = x_1 : A_1, \dots, x_n : A_n$ . Terms are typed by the rules

\frac{x : A \in \Gamma}{\Gamma \vdash x : A} \qquad \frac{}{\Gamma \vdash \star : 1} \qquad \frac{\Gamma \vdash s : A \quad \Gamma \vdash t : B}{\Gamma \vdash \langle s, t\rangle : A \times B} \qquad \frac{\Gamma \vdash p : A \times B}{\Gamma \vdash \pi_1 p : A \quad \Gamma \vdash \pi_2 p : B}

\frac{\Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda x.\, t : A \to B} \qquad \frac{\Gamma \vdash s : A \to B \quad \Gamma \vdash u : A}{\Gamma \vdash s\,u : B}

βη-equality is the least congruence containing

\pi_1\langle s, t\rangle = s, \quad \pi_2\langle s, t\rangle = t, \quad (\lambda x.\, t)\,u = t[u/x] \qquad (\beta)

\langle \pi_1 p, \pi_2 p\rangle = p, \quad t = \star \ (t : 1), \quad \lambda x.\, f\,x = f \ (x \text{ not free in } f) \qquad (\eta)

Definition— interpretation in a CCC

Fix a CCC $\mathcal{C}$ and an object $\llbracket o \rrbracket$ . Extend to all types by $\llbracket 1 \rrbracket = 1$ , $\llbracket A \times B \rrbracket = \llbracket A \rrbracket \times \llbracket B \rrbracket$ and $\llbracket A \to B \rrbracket = \llbracket B \rrbracket^{\llbracket A \rrbracket}$ , and to contexts by $\llbracket x_1 : A_1, \dots, x_n : A_n \rrbracket = (\cdots(1 \times \llbracket A_1 \rrbracket) \times \cdots) \times \llbracket A_n \rrbracket$ . A term $\Gamma \vdash t : A$ is interpreted as a morphism $\llbracket t \rrbracket : \llbracket \Gamma \rrbracket \to \llbracket A \rrbracket$ , by induction on $t$ :

a variable $x_i$ is the $i$ -th product projection;
$\llbracket \star \rrbracket$ is the unique map to $1$ ; $\llbracket \langle s, t\rangle \rrbracket = \langle \llbracket s \rrbracket, \llbracket t \rrbracket\rangle$ ; $\llbracket \pi_i p \rrbracket = \pi_i \circ \llbracket p \rrbracket$ ;
$\llbracket \lambda x.\, t \rrbracket = \Lambda \llbracket t \rrbracket$ , the curried form of $\llbracket t \rrbracket : \llbracket \Gamma \rrbracket \times \llbracket A \rrbracket \to \llbracket B \rrbracket$ ;
$\llbracket s\,u \rrbracket = \mathrm{ev} \circ \langle \llbracket s \rrbracket, \llbracket u \rrbracket \rangle$ .

Definition— quantifiers along a map

For a map $f : X \to Y$ of sets, substitution (pulling back) is $f^* : \mathcal{P}(Y) \to \mathcal{P}(X)$ , $f^*(T) = f^{-1}(T)$ . Define

\exists_f(S) = \{\, y \mid \exists x\, (f(x) = y \wedge x \in S) \,\}, \qquad \forall_f(S) = \{\, y \mid \forall x\, (f(x) = y \Rightarrow x \in S) \,\}.

For the projection $\pi : X \times Y \to X$ these are $\{x \mid \exists y\, (x, y) \in S\}$ and $\{x \mid \forall y\, (x, y) \in S\}$ : quantifying out the variable $y$ .

Worked examplesH

Examples and non-examples

Example— Cartesian closed categories

$\mathbf{Set}$ , with $B^A$ the set of functions (proved below). Also $\mathbf{FinSet}$ , which shows that a CCC need not have infinite limits.
$\mathbf{Cat}$ (small categories), with $\mathcal{D}^{\mathcal{C}}$ the functor category.
Every presheaf category $[\mathcal{C}^{op}, \mathbf{Set}]$ . This is part of the reason presheaf categories are toposes.
Every Heyting algebra, viewed as a poset category. In particular every Boolean algebra, with $a \Rightarrow b = \neg a \vee b$ , and every finite chain $0 \lt \tfrac12 \lt 1$ , with $a \Rightarrow b = 1$ if $a \le b$ and $a \Rightarrow b = b$ otherwise.

Example— Non-examples

$\mathbf{Grp}$ is not cartesian closed. In any CCC with an initial object $0$ , the functor $- \times B$ is a left adjoint, so it preserves the initial object: $0 \times B \cong 0$ . In $\mathbf{Grp}$ the trivial group $1$ is initial, but $1 \times B \cong B$ . If $\mathbf{Grp}$ were cartesian closed, every group would be trivial.
$\mathbf{Top}$ is not cartesian closed. The functor $- \times \Q$ does not preserve all quotient maps, so it has no right adjoint. The exponentiable spaces are exactly the core-compact ones (Day and Kelly, 1970), for example the locally compact Hausdorff spaces. Algebraic topologists therefore work in a convenient subcategory such as compactly generated spaces.
$(\N, \le)$ as a poset category has products ( $\min$ ) and exponentials would be implications, but it has no top element, so no terminal object. It is not cartesian closed. Adjoining a top element repairs this.

Example— Open sets of the line

For any topological space $X$ , the open sets $\mathcal{O}(X)$ form a Heyting algebra under inclusion, with

U \Rightarrow V = \operatorname{int}\big((X \setminus U) \cup V\big), \qquad \neg U = \operatorname{int}(X \setminus U),

the largest open set whose intersection with $U$ lies in $V$ . (Meets are intersections and joins are unions. The residuation law holds because $W \subseteq \operatorname{int}(U^c \cup V)$ iff $W \subseteq U^c \cup V$ , as $W$ is open, iff $W \cap U \subseteq V$ .) In $\mathcal{O}(\R)$ :

for $U = (0, \infty)$ : $\neg U = (-\infty, 0)$ , so $U \vee \neg U = \R \setminus \{0\} \ne \R$ , and $\neg\neg U = (0, \infty) = U$ ;
for $W = \R \setminus \{0\}$ : $\neg W = \operatorname{int}\{0\} = \varnothing$ , so $\neg\neg W = \R \ne W$ .

Excluded middle and double-negation elimination both fail, and the failure sits at a single boundary point. Truth values in $\mathcal{O}(X)$ are "true on an open region". An open region and its pseudo-complement can leave a boundary on which neither is true.

In the Heyting algebra of open subsets of ℝ, the open set U = (0, ∞) and its pseudo-complement ¬U = (−∞, 0) do not cover the point 0, so U ∨ ¬U ≠ ℝ.

Example— Interpreting a term

The term $p : A \times B \vdash \langle \pi_2\, p, \pi_1\, p \rangle : B \times A$ is interpreted in any CCC as $\langle \pi_2, \pi_1 \rangle \circ \pi : 1 \times (A \times B) \to B \times A$ , where $\pi$ discards the empty part of the context. It is the symmetry isomorphism of the product. The closed term $\lambda f.\, \lambda a.\, \lambda b.\, f\langle a, b\rangle$ of type $(A \times B \to C) \to (A \to (B \to C))$ is interpreted in $\mathbf{Set}$ as currying itself. Under Curry–Howard it is a proof of $(A \wedge B \to C) \to (A \to (B \to C))$ .

Example— Quantifiers as shadows

Let $S = \{(x, y) \in \R^2 \mid x \le y^2\}$ and $\pi(x, y) = x$ . Then $\exists_\pi S = \{x \mid \exists y\; x \le y^2\} = \R$ , the shadow of $S$ on the $x$ -axis, and $\forall_\pi S = \{x \mid \forall y\; x \le y^2\} = (-\infty, 0]$ , the set of $x$ whose entire vertical line lies in $S$ . Existential quantification is a direct image (a projection). Universal quantification is its dual.

ProofH

The central theorems

Theorem— Theorem 1 (Set is cartesian closed)

For sets $A, B$ , let $B^A$ be the set of functions $A \to B$ and $\mathrm{ev}(g, a) = g(a)$ . For every $f : C \times A \to B$ there is a unique $\Lambda f : C \to B^A$ with $\mathrm{ev} \circ (\Lambda f \times \id_A) = f$ .

Proof

Existence. Put $\Lambda f(c) = (a \mapsto f(c, a))$ . Then $\mathrm{ev}(\Lambda f(c), a) = f(c, a)$ .

Uniqueness. If $\mathrm{ev} \circ (g \times \id_A) = f$ , then $g(c)(a) = f(c, a)$ for all $a$ , so $g(c) = \Lambda f(c)$ by extensionality of functions, for all $c$ . With the terminal object $1 = \{\ast\}$ and the cartesian product, $\mathbf{Set}$ is cartesian closed.

∎

A useful consequence of the universal property in any CCC is the naturality of currying: for $h : C' \to C$ ,

\Lambda\big(f \circ (h \times \id_A)\big) = \Lambda f \circ h,

because both sides $g$ satisfy $\mathrm{ev} \circ (g \times \id_A) = f \circ (h \times \id_A)$ , and the map with that property is unique.

Theorem— Theorem 2 (soundness of the interpretation)

Let $\mathcal{C}$ be a CCC with an object $\llbracket o \rrbracket$ . If $\Gamma \vdash s = t : A$ is derivable by βη-equality, then $\llbracket s \rrbracket = \llbracket t \rrbracket : \llbracket \Gamma \rrbracket \to \llbracket A \rrbracket$ .

Proof

Two lemmas, both by induction on terms.

Weakening. If $t$ is a term in context $\Gamma$ and $\mathrm{wk}(t)$ is the same term regarded in context $\Gamma, x : A$ , then $\llbracket \mathrm{wk}(t) \rrbracket = \llbracket t \rrbracket \circ \pi_1$ , where $\pi_1 : \llbracket \Gamma \rrbracket \times \llbracket A \rrbracket \to \llbracket \Gamma \rrbracket$ . Variables are projections, and projections compose to projections. The $\lambda$ case uses naturality of currying.

Substitution. If $\Gamma, x : A \vdash t : B$ and $\Gamma \vdash u : A$ , then

\llbracket t[u/x] \rrbracket = \llbracket t \rrbracket \circ \langle \id_{\llbracket \Gamma \rrbracket}, \llbracket u \rrbracket \rangle .

More generally, a simultaneous substitution $\sigma$ from $\Gamma$ to $\Delta$ is interpreted as the tuple $\llbracket \sigma \rrbracket : \llbracket \Delta \rrbracket \to \llbracket \Gamma \rrbracket$ of the interpretations of the substituted terms, and $\llbracket t[\sigma] \rrbracket = \llbracket t \rrbracket \circ \llbracket \sigma \rrbracket$ . For variables this is the definition of a tuple, and the pairing, projection and application cases follow from $\langle f, g \rangle \circ h = \langle f h, g h \rangle$ . For $\lambda y.\, t$ , the substitution under the binder is $\sigma$ weakened and extended by $y$ , interpreted as $\llbracket \sigma \rrbracket \times \id$ by the weakening lemma. Then naturality of currying gives $\llbracket (\lambda y.\, t)[\sigma] \rrbracket = \Lambda(\llbracket t \rrbracket \circ (\llbracket \sigma \rrbracket \times \id)) = \Lambda \llbracket t \rrbracket \circ \llbracket \sigma \rrbracket$ .

The equations. The interpretation is defined compositionally, so it respects the congruence rules, reflexivity, symmetry and transitivity. It remains to check the axioms.

Products: $\pi_1 \circ \langle \llbracket s \rrbracket, \llbracket t \rrbracket \rangle = \llbracket s \rrbracket$ and $\langle \pi_1 \circ \llbracket p \rrbracket, \pi_2 \circ \llbracket p \rrbracket\rangle = \llbracket p \rrbracket$ hold by the universal property of the product. Any two maps into $1$ are equal.
β for functions:

\llbracket (\lambda x.\, t)\,u \rrbracket = \mathrm{ev} \circ \langle \Lambda \llbracket t \rrbracket, \llbracket u \rrbracket \rangle = \mathrm{ev} \circ (\Lambda \llbracket t \rrbracket \times \id) \circ \langle \id, \llbracket u \rrbracket \rangle = \llbracket t \rrbracket \circ \langle \id, \llbracket u \rrbracket \rangle = \llbracket t[u/x] \rrbracket .

η for functions: by weakening, $\llbracket \lambda x.\, f\,x \rrbracket = \Lambda\big(\mathrm{ev} \circ \langle \llbracket f \rrbracket \circ \pi_1, \pi_2 \rangle\big) = \Lambda\big(\mathrm{ev} \circ (\llbracket f \rrbracket \times \id)\big) = \llbracket f \rrbracket$ , by uniqueness in the universal property.

∎

Theorem 2 has a converse. Make a category whose objects are types and whose morphisms $A \to B$ are βη-classes of terms $x : A \vdash t : B$ . This syntactic category is itself cartesian closed: it is the free CCC on the base types. So an equation between terms holds in every CCC exactly when it is βη-derivable. This is the precise content of the Curry–Howard–Lambek correspondence. Lambek and Scott (1986, Part I) give the proof and the equivalence between λ-theories and cartesian closed categories that it extends to. For the single model $\mathbf{Set}$ , Friedman (1975) proved that equality in the full set-theoretic model over an infinite base set coincides with βη-equality for the simply typed λ-calculus. The computation section shows why finite base sets are not enough.

Theorem— Theorem 3 (Lawvere: quantifiers are adjoints)

For every $f : X \to Y$ , as monotone maps between the posets $\mathcal{P}(X)$ and $\mathcal{P}(Y)$ ,

\exists_f \;\dashv\; f^* \;\dashv\; \forall_f, \qquad\text{that is}\qquad \exists_f S \subseteq T \iff S \subseteq f^* T, \qquad f^* T \subseteq S \iff T \subseteq \forall_f S .

Proof

( $\exists_f \dashv f^*$ ) If $\exists_f S \subseteq T$ and $x \in S$ , then $f(x) \in \exists_f S \subseteq T$ , so $x \in f^{-1}(T)$ . Conversely, if $S \subseteq f^{-1}(T)$ and $y = f(x)$ with $x \in S$ , then $y = f(x) \in T$ .

( $f^* \dashv \forall_f$ ) Suppose $f^{-1}(T) \subseteq S$ and $y \in T$ . Any $x$ with $f(x) = y$ lies in $f^{-1}(T) \subseteq S$ , so $y \in \forall_f S$ . Conversely, suppose $T \subseteq \forall_f S$ and $x \in f^{-1}(T)$ . Then $f(x) \in T \subseteq \forall_f S$ , and $x$ itself lies over $f(x)$ , so $x \in S$ .

∎

The adjoint triple

\exists_f \dashv f^* \dashv \forall_f

: substitution has a left adjoint (existential quantification) and a right adjoint (universal quantification).

Since right adjoints preserve limits (here, meets) and left adjoints preserve colimits (joins), Theorem 3 explains familiar quantifier laws and their failures:

\forall y\,(\varphi \wedge \psi) \iff \forall y\,\varphi \wedge \forall y\,\psi, \qquad \exists y\,(\varphi \vee \psi) \iff \exists y\,\varphi \vee \exists y\,\psi,

while $\exists$ need not distribute over $\wedge$ and $\forall$ need not distribute over $\vee$ . The same adjunctions make sense in any category with pullbacks and a poset of "predicates" (subobjects) on each object. This is Lawvere's notion of a hyperdoctrine. Two compatibility conditions are needed there. Frobenius reciprocity says $\exists_f(S \cap f^*T) = \exists_f S \cap T$ ; it is a one-line check in $\mathbf{Set}$ , done in Lean below. Beck–Chevalley says that quantification commutes with substitution along pullback squares; in syntax, $(\exists y\, \varphi(x, y))[t/x] = \exists y\, \varphi(t, y)$ . Even equality is an adjoint. For the diagonal $\delta : X \to X \times X$ , the predicate $\exists_\delta(X) = \{(x, x)\}$ is the equality relation (Lawvere 1970).

Theorem— Theorem 4 (soundness for Heyting algebras)

Let $H$ be a Heyting algebra and $v$ an assignment of elements of $H$ to propositional variables, extended to formulas by $\llbracket \top \rrbracket = \top$ , $\llbracket \bot \rrbracket = \bot$ , $\llbracket \varphi \wedge \psi \rrbracket = \llbracket \varphi \rrbracket \wedge \llbracket \psi \rrbracket$ , $\llbracket \varphi \vee \psi \rrbracket = \llbracket \varphi \rrbracket \vee \llbracket \psi \rrbracket$ and $\llbracket \varphi \to \psi \rrbracket = \llbracket \varphi \rrbracket \Rightarrow \llbracket \psi \rrbracket$ . If $\varphi$ is derivable from hypotheses $\Gamma$ in intuitionistic natural deduction, then $\bigwedge \llbracket \Gamma \rrbracket \le \llbracket \varphi \rrbracket$ .

Proof

First, a Heyting algebra is a distributive lattice. The map $a \wedge -$ is a left adjoint (of $a \Rightarrow -$ ), so it preserves joins: $a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)$ .

Now induct on the derivation, writing $c = \bigwedge \llbracket \Gamma \rrbracket$ . A hypothesis $\varphi \in \Gamma$ satisfies $c \le \llbracket \varphi \rrbracket$ . The rules for $\top$ , $\wedge$ and the $\vee$ -introductions are the universal properties of top, meet and join, and $\bot$ -elimination is $c \le \bot \Rightarrow c \le x$ .

$\to$ -introduction: from $\llbracket\varphi\rrbracket \wedge c \le \llbracket \psi \rrbracket$ the residuation law gives $c \le \llbracket \varphi \rrbracket \Rightarrow \llbracket \psi \rrbracket$ .
$\to$ -elimination: from $c \le a \Rightarrow b$ and $c \le a$ we get $c \le (a \Rightarrow b) \wedge a \le b$ , the counit of the adjunction.
$\vee$ -elimination: from $c \le a \vee b$ , $a \wedge c \le x$ and $b \wedge c \le x$ we get $c = c \wedge (a \vee b) = (c \wedge a) \vee (c \wedge b) \le x$ , by distributivity.

∎

Theorem— Theorem 5 (completeness: the Lindenbaum–Tarski algebra)

If $\llbracket \varphi \rrbracket = \top$ in every Heyting algebra under every valuation, then $\varphi$ is derivable in intuitionistic propositional logic.

Proof

Let $L$ be the set of formulas modulo interderivability ( $\varphi \equiv \psi$ iff $\varphi \vdash \psi$ and $\psi \vdash \varphi$ ), ordered by $[\varphi] \le [\psi]$ iff $\varphi \vdash \psi$ . The rules show that the connectives are well defined on classes, that $[\varphi \wedge \psi]$ is the meet, $[\varphi \vee \psi]$ the join ( $\vee$ -introduction gives the upper bounds and $\vee$ -elimination gives leastness), $[\top]$ the top and $[\bot]$ the bottom. Finally, $\chi \wedge \varphi \vdash \psi$ iff $\chi \vdash \varphi \to \psi$ by $\to$ -introduction and $\to$ -elimination, so $[\varphi \to \psi]$ is the Heyting implication. Thus $L$ is a Heyting algebra (the Lindenbaum–Tarski algebra). With the valuation $v(p) = [p]$ , induction on formulas gives $\llbracket \varphi \rrbracket = [\varphi]$ . If $\varphi$ is valid in all Heyting algebras, then $[\varphi] = \top = [\top]$ , so $\top \vdash \varphi$ and hence $\vdash \varphi$ .

∎

Theorem— Theorem 6 (excluded middle is not derivable, but its double negation is)

$\nvdash P \lor \neg P$ in intuitionistic propositional logic, while $\vdash \neg\neg(P \lor \neg P)$ .

Proof

If $\vdash P \lor \neg P$ , Theorem 4 would give $U \vee \neg U = \R$ for every open $U \subseteq \R$ . This fails for $U = (0, \infty)$ , as computed above. Here is a proof that needs no computation of $\neg U$ . In any Heyting algebra $U \wedge \neg U = \bot$ . If also $U \vee \neg U = \top$ , then $U$ and $\neg U$ are disjoint open sets covering $\R$ , so $U$ is open and closed. Since $\R$ is connected, $U$ is $\varnothing$ or $\R$ , which is false.

A derivation of $\neg\neg(P \lor \neg P)$ : assume $h : \neg(P \lor \neg P)$ . Under the further assumption $P$ , the formula $P \lor \neg P$ follows by $\vee$ -introduction, and $h$ yields $\bot$ . Discharging $P$ gives $\neg P$ , hence $P \lor \neg P$ again by $\vee$ -introduction, and $h$ yields $\bot$ . Discharging $h$ gives $\neg\neg(P \lor \neg P)$ .

∎

The same argument shows that $\neg(P \lor \neg P)$ is not derivable either: in the two-element Boolean algebra it evaluates to $\bot$ . Intuitionistic logic does not deny excluded middle. It declines to assume it, and it proves that excluded middle can never be refuted. Glivenko's theorem (1929) sharpens this: a propositional formula $\varphi$ is a classical tautology if and only if $\neg\neg\varphi$ is intuitionistically derivable.

Formal mathematicsF

Formalisation in Lean

The Lean module Lumenary.CategoricalLogic formalises three pieces of this lesson, mostly from scratch, using Mathlib for lattices, topology and the category of types.

The λ-calculus and its semantics. Terms are intrinsically typed: Tm Γ A contains only well-typed terms, so the typing rules are built into the constructors. Variables are typed de Bruijn indices, which makes substitution capture-avoiding by construction. Lean contexts grow at the front (A :: Γ denotes ⟦A⟧ × ⟦Γ⟧), the mirror image of the convention $\llbracket\Gamma\rrbracket \times \llbracket A\rrbracket$ in the human proof. That is only bookkeeping.

TmLean 4Formally verified

/-- **Terms** of the simply typed λ-calculus with unit and products, typed *intrinsically*:
`Tm Γ A` contains exactly the well-typed terms of type `A` in context `Γ`. Read through
Curry–Howard, `Tm Γ A` is the set of natural-deduction proofs of `A` from hypotheses `Γ` in the
`⊤, ∧, →` fragment of intuitionistic logic. -/
inductive Tm : List Ty → Ty → Type where
  | var {Γ : List Ty} {A : Ty} : Var Γ A → Tm Γ A
  | star {Γ : List Ty} : Tm Γ .unit
  | pair {Γ : List Ty} {A B : Ty} : Tm Γ A → Tm Γ B → Tm Γ (.prod A B)
  | fst {Γ : List Ty} {A B : Ty} : Tm Γ (.prod A B) → Tm Γ A
  | snd {Γ : List Ty} {A B : Ty} : Tm Γ (.prod A B) → Tm Γ B
  | lam {Γ : List Ty} {A B : Ty} : Tm (A :: Γ) B → Tm Γ (.arr A B)
  | app {Γ : List Ty} {A B : Ty} : Tm Γ (.arr A B) → Tm Γ A → Tm Γ B

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

ConvLean 4Formally verified

/-- **βη-conversion**: the equational theory of the simply typed λ-calculus with products.
It is the least congruence containing the β-rules (`fst ⟨s, t⟩ = s`, `snd ⟨s, t⟩ = t`,
`(λx. t) u = t[u/x]`) and the η-rules (`⟨fst p, snd p⟩ = p`, `t = ⋆` at unit type,
`λx. f x = f` with `x` not free in `f`). These are exactly the equations of a cartesian closed
category, read through the term ↔ morphism dictionary. -/
inductive Conv : {Γ : List Ty} → {A : Ty} → Tm Γ A → Tm Γ A → Prop where
  | refl {Γ : List Ty} {A : Ty} (t : Tm Γ A) : Conv t t
  | symm {Γ : List Ty} {A : Ty} {s t : Tm Γ A} : Conv s t → Conv t s
  | trans {Γ : List Ty} {A : Ty} {s t u : Tm Γ A} : Conv s t → Conv t u → Conv s u
  | pair {Γ : List Ty} {A B : Ty} {s s' : Tm Γ A} {t t' : Tm Γ B} :
      Conv s s' → Conv t t' → Conv (.pair s t) (.pair s' t')
  | fst {Γ : List Ty} {A B : Ty} {p p' : Tm Γ (.prod A B)} : Conv p p' → Conv (.fst p) (.fst p')
  | snd {Γ : List Ty} {A B : Ty} {p p' : Tm Γ (.prod A B)} : Conv p p' → Conv (.snd p) (.snd p')
  | lam {Γ : List Ty} {A B : Ty} {t t' : Tm (A :: Γ) B} : Conv t t' → Conv (.lam t) (.lam t')
  | app {Γ : List Ty} {A B : Ty} {s s' : Tm Γ (.arr A B)} {t t' : Tm Γ A} :
      Conv s s' → Conv t t' → Conv (.app s t) (.app s' t')
  | beta_fst {Γ : List Ty} {A B : Ty} (s : Tm Γ A) (t : Tm Γ B) : Conv (.fst (.pair s t)) s
  | beta_snd {Γ : List Ty} {A B : Ty} (s : Tm Γ A) (t : Tm Γ B) : Conv (.snd (.pair s t)) t
  | beta_arr {Γ : List Ty} {A B : Ty} (t : Tm (A :: Γ) B) (u : Tm Γ A) :
      Conv (.app (.lam t) u) (t.subst (single u))
  | eta_prod {Γ : List Ty} {A B : Ty} (p : Tm Γ (.prod A B)) : Conv (.pair (.fst p) (.snd p)) p
  | eta_unit {Γ : List Ty} (t : Tm Γ .unit) : Conv t .star
  | eta_arr {Γ : List Ty} {A B : Ty} (f : Tm Γ (.arr A B)) :
      Conv (.lam (.app (f.rename Var.succ) (.var .zero))) f

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

The interpretation lands in Lean's types and functions, the type-theoretic stand-in for $\mathbf{Set}$ . lam is currying and app is evaluation, exactly as in the definition above:

denoteLean 4Formally verified

/-- **The interpretation of terms as morphisms** `⟦Γ⟧ → ⟦A⟧` of the cartesian closed category
of types: pairing is the map into a product, `fst`/`snd` compose with projections, `lam` is
**currying** (the bijection `Hom(Γ × A, B) ≅ Hom(Γ, B^A)`), and `app` composes with
**evaluation** `B^A × A → B`. -/
def Tm.denote {X : Type} : {Γ : List Ty} → {A : Ty} → Tm Γ A → ctxDenote X Γ → A.denote X
  | _, _, .var v, γ => v.denote γ
  | _, _, .star, _ => ()
  | _, _, .pair s t, γ => (s.denote γ, t.denote γ)
  | _, _, .fst t, γ => (t.denote γ).1
  | _, _, .snd t, γ => (t.denote γ).2
  | _, _, .lam t, γ => fun a => t.denote (a, γ)
  | _, _, .app s t, γ => s.denote γ (t.denote γ)

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

The substitution lemma is the "logical relation" form of the human lemma $\llbracket t[\sigma] \rrbracket = \llbracket t \rrbracket \circ \llbracket \sigma \rrbracket$ . Instead of building the tuple $\llbracket\sigma\rrbracket$ , it assumes that each substituted term denotes the value of the variable it replaces. The soundness theorem then follows the human proof case by case:

denote_substLean 4Proved here from basic factsFormally verified

/-- **Substitution lemma** — the semantic heart of Curry–Howard–Lambek: substituting terms for
variables is interpreted by *composition* with the tuple of their interpretations. Precisely,
if every `σ v` denotes (at `δ`) the value of `v` (at `γ`), then `t.subst σ` denotes (at `δ`) the
value of `t` (at `γ`). The `lam` case needs the renaming lemma for the weakening in
`substExt`. -/
theorem denote_subst {X : Type} {Γ Δ : List Ty} {A : Ty} (t : Tm Γ A)
    (σ : ∀ {B : Ty}, Var Γ B → Tm Δ B) (δ : ctxDenote X Δ) (γ : ctxDenote X Γ)
    (h : ∀ {B : Ty} (v : Var Γ B), (σ v).denote δ = v.denote γ) :
    (t.subst σ).denote δ = t.denote γ := by
  induction t generalizing Δ with
  | var v => exact h v
  | star => rfl
  | pair s t ihs iht => exact congrArg₂ Prod.mk (ihs σ δ γ h) (iht σ δ γ h)
  | fst t ih => simp only [Tm.subst, Tm.denote, ih σ δ γ h]
  | snd t ih => simp only [Tm.subst, Tm.denote, ih σ δ γ h]
  | lam t ih =>
    funext a
    apply ih (substExt σ) (a, δ) (a, γ)
    intro B v
    cases v with
    | zero => rfl
    | succ v =>
      show ((σ v).rename Var.succ).denote (a, δ) = v.denote γ
      rw [denote_rename (σ v) Var.succ (a, δ) δ (fun _ => rfl)]
      exact h v
  | app s t ihs iht => simp only [Tm.subst, Tm.denote, ihs σ δ γ h, iht σ δ γ h]

Axioms used: propext, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

soundLean 4Proved here from basic factsFormally verified

/-- **Soundness of the interpretation** (Lambek): βη-convertible terms denote the *same*
morphism `⟦Γ⟧ → ⟦A⟧`, for every interpretation `X` of the base type. Proved by induction on
the derivation of convertibility; the congruence rules use function extensionality, β for
functions is `beta_sound`, and η for functions is the renaming lemma. -/
theorem Conv.sound {X : Type} {Γ : List Ty} {A : Ty} {s t : Tm Γ A} (h : Conv s t) :
    (s.denote : ctxDenote X Γ → A.denote X) = t.denote := by
  induction h with
  | refl t => rfl
  | symm _ ih => exact ih.symm
  | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂
  | pair _ _ ih₁ ih₂ => funext γ; exact congrArg₂ Prod.mk (congrFun ih₁ γ) (congrFun ih₂ γ)
  | fst _ ih => funext γ; simp only [Tm.denote, ih]
  | snd _ ih => funext γ; simp only [Tm.denote, ih]
  | lam _ ih => funext γ a; exact congrFun ih (a, γ)
  | app _ _ ih₁ ih₂ => funext γ; simp only [Tm.denote, ih₁, ih₂]
  | beta_fst s t => rfl
  | beta_snd s t => rfl
  | beta_arr t u => funext γ; exact beta_sound t u γ
  | eta_prod p => rfl
  | eta_unit t => rfl
  | eta_arr f =>
    funext γ a
    show (f.rename Var.succ).denote (a, γ) a = f.denote γ a
    rw [denote_rename f Var.succ (a, γ) γ (fun _ => rfl)]

Axioms used: propext, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

Two small consequences. A model proves consistency (interpret the base type as the empty type), and the Curry–Howard reading of a closed term computes to the expected function:

no_closed_term_of_baseLean 4Proved here from basic factsFormally verified

/-- **Consistency from a model.** There is no closed term of the base type: interpret the base
type as the empty type, and a closed term would denote an element of it. Through Curry–Howard:
an atomic proposition is not provable from no hypotheses. -/
theorem no_closed_term_of_base (t : Tm [] .base) : False :=
  (t.denote (X := Empty) ()).elim

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

curryTm_denoteLean 4Proved here from basic factsFormally verified

/-- The interpretation of `curryTm` in **Set** is currying itself, `Function.curry`
(by computation: both sides reduce to `fun f a b => f (a, b)`). -/
theorem curryTm_denote (X : Type) (A B C : Ty) :
    (curryTm A B C).denote (X := X) () = Function.curry := rfl

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

Mathlib knows that Type is cartesian closed (as a MonoidalClosed category for the cartesian monoidal structure):

types_cartesianClosedLean 4Applies a library theoremFormally verified

/-- Mathlib knows that the category of types is **cartesian closed**: `Type u`, with its
cartesian monoidal structure, carries a `MonoidalClosed` instance (the internal hom is the
function type and `− × B ⊣ (B → −)` is currying). This is Mathlib's instance from
`Mathlib.CategoryTheory.Monoidal.Closed.Types`. -/
theorem types_cartesianClosed : Nonempty (CategoryTheory.MonoidalClosed (Type)) :=
  ⟨inferInstance⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

Quantifiers as adjoints. The proofs of Theorem 3 are formalised verbatim. Mathlib states them as Galois connections, which are adjunctions between posets:

forallAlongLean 4Formally verified

/-- **Universal quantification along `f : X → Y`**: `y` belongs to `∀_f S` when *every* `x`
over `y` lies in `S`. (Mathlib calls this `Set.kernImage f S`.) -/
def forallAlong {X Y : Type} (f : X → Y) (S : Set X) : Set Y :=
  {y | ∀ x, f x = y → x ∈ S}

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

exists_adjointLean 4Proved here from basic factsFormally verified

/-- **∃ is left adjoint to substitution** (Lawvere): for predicates `S` on `X` and `T` on `Y`,
`∃_f S ⊆ T ↔ S ⊆ f*T`, where `∃_f S = f '' S` is the direct image and `f*T = f ⁻¹' T` is
pulling back (substitution). -/
theorem exists_adjoint {X Y : Type} (f : X → Y) (S : Set X) (T : Set Y) :
    f '' S ⊆ T ↔ S ⊆ f ⁻¹' T := by
  constructor
  · intro h x hx
    exact h ⟨x, hx, rfl⟩
  · rintro h _ ⟨x, hx, rfl⟩
    exact h hx

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

forall_adjointLean 4Proved here from basic factsFormally verified

/-- **∀ is right adjoint to substitution** (Lawvere): `f*T ⊆ S ↔ T ⊆ ∀_f S`. -/
theorem forall_adjoint {X Y : Type} (f : X → Y) (S : Set X) (T : Set Y) :
    f ⁻¹' T ⊆ S ↔ T ⊆ forallAlong f S := by
  constructor
  · intro h y hy x hxy
    apply h
    show f x ∈ T
    rw [hxy]
    exact hy
  · intro h x hx
    exact h hx x rfl

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

forall_along_fstLean 4Proved here from basic factsFormally verified

/-- Along the projection `π : X × Y → X`, the right adjoint is the **universal quantifier**:
`∀_π S = {x | ∀ y, (x, y) ∈ S}`. -/
theorem forall_along_fst {X Y : Type} (S : Set (X × Y)) :
    forallAlong Prod.fst S = {x | ∀ y, (x, y) ∈ S} := by
  ext x
  constructor
  · intro h y
    exact h (x, y) rfl
  · rintro h ⟨x', y⟩ rfl
    exact h y

Axioms used: propext, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

quantifier_adjunctions_libraryLean 4Applies a library theoremFormally verified

/-- The same two adjunctions, as Mathlib states them: Galois connections
`image f ⊣ preimage f` (`Set.image_preimage`) and `preimage f ⊣ kernImage f`
(`Set.preimage_kernImage`). A Galois connection is an adjunction between posets viewed as
categories. -/
theorem quantifier_adjunctions_library {X Y : Type} (f : X → Y) :
    GaloisConnection (Set.image f) (Set.preimage f) ∧
      GaloisConnection (Set.preimage f) (Set.kernImage f) :=
  ⟨Set.image_preimage, Set.preimage_kernImage⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

frobeniusLean 4Proved here from basic factsFormally verified

/-- **Frobenius reciprocity**: `∃_f (S ∧ f*T) = ∃_f S ∧ T`. In logic: `∃x (φ(x) ∧ ψ(f x))` is
equivalent to `(∃x φ(x)) ∧ ψ` when `ψ` only depends on `y = f x`. It is one of the two
conditions (with Beck–Chevalley) that make `∃` behave well in a hyperdoctrine. -/
theorem frobenius {X Y : Type} (f : X → Y) (S : Set X) (T : Set Y) :
    f '' (S ∩ f ⁻¹' T) = f '' S ∩ T := by
  ext y
  constructor
  · rintro ⟨x, ⟨hxS, hxT⟩, rfl⟩
    exact ⟨⟨x, hxS, rfl⟩, hxT⟩
  · rintro ⟨⟨x, hxS, rfl⟩, hyT⟩
    exact ⟨x, ⟨hxS, hyT⟩, rfl⟩

Axioms used: propext, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

Heyting algebras. The law $\neg\neg(a \vee \neg a) = \top$ is proved from the residuation law alone. Its counterpart in Lean's own logic is proved without excluded middle, and #print axioms confirms that it uses no axioms at all:

not_not_em_heytingLean 4Proved here from basic factsFormally verified

/-- **`¬¬(a ∨ ¬a) = ⊤` in every Heyting algebra.** Write `n = ¬(a ∨ ¬a)`. Since `a ≤ a ∨ ¬a`,
`n ∧ a ≤ ⊥`, so `n ≤ ¬a ≤ a ∨ ¬a`; hence `n ≤ n ∧ (a ∨ ¬a) ≤ ⊥`, i.e. `n = ⊥` and `¬n = ⊤`.
Only the defining law `c ≤ (a ⇨ b) ↔ c ∧ a ≤ b` is used. -/
theorem not_not_em_heyting {α : Type*} [HeytingAlgebra α] (a : α) : (a ⊔ aᶜ)ᶜᶜ = ⊤ := by
  -- `x ∧ ¬x ≤ ⊥`, from the residuation law with `c = ¬x`.
  have contra : ∀ x : α, xᶜ ⊓ x ≤ ⊥ := fun x => by
    rw [← le_himp_iff, himp_bot]
  have hn_le_compl : (a ⊔ aᶜ)ᶜ ≤ aᶜ := by
    have h : (a ⊔ aᶜ)ᶜ ≤ a ⇨ ⊥ := by
      rw [le_himp_iff]
      exact le_trans (inf_le_inf_left _ le_sup_left) (contra (a ⊔ aᶜ))
    rwa [himp_bot] at h
  have hn_bot : (a ⊔ aᶜ)ᶜ ≤ ⊥ :=
    calc (a ⊔ aᶜ)ᶜ ≤ (a ⊔ aᶜ)ᶜ ⊓ (a ⊔ aᶜ) := le_inf le_rfl (hn_le_compl.trans le_sup_right)
      _ ≤ ⊥ := contra (a ⊔ aᶜ)
  have h : ⊤ ≤ (a ⊔ aᶜ)ᶜ ⇨ ⊥ := by
    rw [le_himp_iff]
    exact le_trans inf_le_right hn_bot
  rw [himp_bot] at h
  exact top_le_iff.mp h

Axioms used: propextformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

not_not_emLean 4Proved here from basic factsFormally verified

/-- The same law in Lean's own logic: `¬¬(P ∨ ¬P)`, proved **without** the law of excluded
middle (`#print axioms` reports no axioms). Given `h : ¬(P ∨ ¬P)`, the function
`fun p => h (Or.inl p)` proves `¬P`, and then `h (Or.inr …)` is a contradiction. -/
theorem not_not_em (P : Prop) : ¬¬(P ∨ ¬P) :=
  fun h => h (Or.inr fun p => h (Or.inl p))

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

The non-Boolean Heyting algebra $\mathcal{O}(\R)$ is handled exactly as in the second proof of Theorem 6, by connectedness:

opens_real_not_booleanLean 4Proved here from basic factsFormally verified

/-- **The open sets of ℝ form a Heyting algebra that is not Boolean.** (`Opens ℝ` is a frame,
hence a Heyting algebra, in Mathlib.) For `U = (0, ∞)`, the pseudo-complement `¬U` is the
largest open set disjoint from `U`, and `U ∨ ¬U ≠ ℝ`: otherwise `U` would be open and closed,
hence `∅` or `ℝ`, because ℝ is connected (Mathlib's `isClopen_iff`). -/
theorem opens_real_not_boolean :
    ∃ U : TopologicalSpace.Opens ℝ, U ⊔ Uᶜ ≠ ⊤ := by
  refine ⟨⟨Set.Ioi 0, isOpen_Ioi⟩, fun h => ?_⟩
  set U : TopologicalSpace.Opens ℝ := ⟨Set.Ioi 0, isOpen_Ioi⟩ with hU
  have hdisj : U ⊓ Uᶜ = ⊥ := inf_compl_self U
  have hunion : (U : Set ℝ) ∪ (Uᶜ : TopologicalSpace.Opens ℝ) = Set.univ := by
    rw [← TopologicalSpace.Opens.coe_sup, h, TopologicalSpace.Opens.coe_top]
  have hinter : (U : Set ℝ) ∩ (Uᶜ : TopologicalSpace.Opens ℝ) = ∅ := by
    rw [← TopologicalSpace.Opens.coe_inf, hdisj, TopologicalSpace.Opens.coe_bot]
  -- So the complement of `U` (as a set) is the open set `¬U`; hence `U` is clopen.
  have hcompl : (U : Set ℝ)ᶜ = (Uᶜ : TopologicalSpace.Opens ℝ) := by
    ext x
    constructor
    · intro hx
      have : x ∈ (U : Set ℝ) ∪ (Uᶜ : TopologicalSpace.Opens ℝ) := by rw [hunion]; trivial
      rcases this with h1 | h2
      · exact absurd h1 hx
      · exact h2
    · intro hx hxU
      have : x ∈ (U : Set ℝ) ∩ (Uᶜ : TopologicalSpace.Opens ℝ) := ⟨hxU, hx⟩
      rw [hinter] at this
      exact this
  have hclopen : IsClopen (U : Set ℝ) := by
    refine ⟨?_, U.isOpen⟩
    rw [← isOpen_compl_iff, hcompl]
    exact (Uᶜ : TopologicalSpace.Opens ℝ).isOpen
  rcases isClopen_iff.mp hclopen with h0 | h1
  · have : (1 : ℝ) ∈ (U : Set ℝ) := by
      show (1 : ℝ) ∈ Set.Ioi 0
      norm_num
    rw [h0] at this
    exact this
  · have : (-1 : ℝ) ∈ (U : Set ℝ) := by rw [h1]; trivial
    have : (0 : ℝ) < -1 := this
    norm_num at this

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

Finally, intuitionistic natural deduction, its soundness for every Heyting algebra (Theorem 4), and the two halves of Theorem 6:

DerivesLean 4Formally verified

/-- **Natural deduction for intuitionistic propositional logic** (IPC): `Derives Γ φ` means
`φ` is derivable from the list of hypotheses `Γ`. There is an introduction and an elimination
rule for each connective, and *no* rule for excluded middle or double-negation elimination. -/
inductive Derives : List Form → Form → Prop where
  | hyp {Γ : List Form} {φ : Form} : φ ∈ Γ → Derives Γ φ
  | topI {Γ : List Form} : Derives Γ .top
  | botE {Γ : List Form} {φ : Form} : Derives Γ .bot → Derives Γ φ
  | andI {Γ : List Form} {φ ψ : Form} : Derives Γ φ → Derives Γ ψ → Derives Γ (.and φ ψ)
  | andE₁ {Γ : List Form} {φ ψ : Form} : Derives Γ (.and φ ψ) → Derives Γ φ
  | andE₂ {Γ : List Form} {φ ψ : Form} : Derives Γ (.and φ ψ) → Derives Γ ψ
  | orI₁ {Γ : List Form} {φ ψ : Form} : Derives Γ φ → Derives Γ (.or φ ψ)
  | orI₂ {Γ : List Form} {φ ψ : Form} : Derives Γ ψ → Derives Γ (.or φ ψ)
  | orE {Γ : List Form} {φ ψ χ : Form} :
      Derives Γ (.or φ ψ) → Derives (φ :: Γ) χ → Derives (ψ :: Γ) χ → Derives Γ χ
  | impI {Γ : List Form} {φ ψ : Form} : Derives (φ :: Γ) ψ → Derives Γ (.imp φ ψ)
  | impE {Γ : List Form} {φ ψ : Form} : Derives Γ (.imp φ ψ) → Derives Γ φ → Derives Γ ψ

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

derives_soundLean 4Proved here from basic factsFormally verified

/-- **Soundness of intuitionistic logic for Heyting algebras**: if `φ` is derivable from `Γ`,
then in *every* Heyting algebra and for *every* valuation, `⋀Γ ≤ ⟦φ⟧`. Each rule is one law of
Heyting algebras: `→I` and `→E` are the two directions of `c ≤ (a ⇨ b) ↔ c ∧ a ≤ b`, and
`∨E` uses distributivity `c ∧ (a ∨ b) = (c ∧ a) ∨ (c ∧ b)`. -/
theorem derives_sound {α : Type*} [HeytingAlgebra α] (v : ℕ → α) {Γ : List Form} {φ : Form}
    (h : Derives Γ φ) : ctxEval v Γ ≤ φ.eval v := by
  induction h with
  | hyp hm => exact ctxEval_le_of_mem v hm
  | topI => exact le_top
  | botE _ ih => exact ih.trans bot_le
  | andI _ _ ih₁ ih₂ => exact le_inf ih₁ ih₂
  | andE₁ _ ih => exact ih.trans inf_le_left
  | andE₂ _ ih => exact ih.trans inf_le_right
  | orI₁ _ ih => exact ih.trans le_sup_left
  | orI₂ _ ih => exact ih.trans le_sup_right
  | @orE Γ φ ψ χ _ _ _ ih ih₁ ih₂ =>
    -- `c ≤ a ∨ b`, `a ∧ c ≤ x` and `b ∧ c ≤ x` give `c = c ∧ (a ∨ b) = (c ∧ a) ∨ (c ∧ b) ≤ x`.
    calc ctxEval v Γ ≤ ctxEval v Γ ⊓ (φ.eval v ⊔ ψ.eval v) := le_inf le_rfl ih
      _ = (ctxEval v Γ ⊓ φ.eval v) ⊔ (ctxEval v Γ ⊓ ψ.eval v) := inf_sup_left _ _ _
      _ ≤ χ.eval v := by
        apply sup_le
        · rw [inf_comm]; exact ih₁
        · rw [inf_comm]; exact ih₂
  | @impI Γ φ ψ _ ih =>
    show ctxEval v Γ ≤ φ.eval v ⇨ ψ.eval v
    rw [le_himp_iff, inf_comm]
    exact ih
  | impE _ _ ih₁ ih₂ =>
    exact (le_inf ih₁ ih₂).trans himp_inf_le

Axioms used: propextformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

derives_not_not_emLean 4Proved here from basic factsFormally verified

/-- `¬¬(p ∨ ¬p)` **is** derivable intuitionistically. The derivation: assume
`h : ¬(p ∨ ¬p)`; to refute it, prove `p ∨ ¬p` by proving `¬p` (assume `p`, then `h (inl p)` is
absurd) and applying `inr`. -/
theorem derives_not_not_em (n : ℕ) :
    Derives [] (Form.neg (Form.neg (.or (.atom n) (Form.neg (.atom n))))) := by
  apply Derives.impI
  apply Derives.impE (Derives.hyp (List.mem_singleton_self _))
  apply Derives.orI₂
  apply Derives.impI
  apply Derives.impE (Derives.hyp (List.mem_cons_of_mem _ (List.mem_singleton_self _)))
  exact Derives.orI₁ (Derives.hyp (List.mem_cons_self))

Axioms used: No axiomsformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

not_derives_emLean 4Proved here from basic factsFormally verified

/-- **Excluded middle is not derivable** in intuitionistic propositional logic. If it were,
soundness would force `U ∨ ¬U = ⊤` for every open set `U ⊆ ℝ`, contradicting
`opens_real_not_boolean`. (The semantics does the work: no search through derivations.) -/
theorem not_derives_em (n : ℕ) : ¬ Derives [] (.or (.atom n) (Form.neg (.atom n))) := by
  intro h
  obtain ⟨U, hU⟩ := opens_real_not_boolean
  have hs := derives_sound (fun _ => U) h
  apply hU
  apply top_le_iff.mp
  simpa [ctxEval, Form.eval, Form.neg, himp_bot] using hs

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/CategoricalLogic.leanTry it in the Lean web editor

What is not formalised. The interpretation in an arbitrary cartesian closed category (Lean has one model, Type; Mathlib's MonoidalClosed API would be the place to generalise), the freeness of the syntactic category, Friedman's theorem, and the completeness theorem (Theorem 5), whose Lindenbaum–Tarski construction needs a quotient of formulas by interderivability. Note also that Lean's ambient logic is classical (Classical.choice is available). The proofs above that report no axioms are constructive, but the formal system as a whole is not intuitionistic. That is why we formalised intuitionistic logic as an object language (Derives) instead of relying on Lean's own.

ComputationC

Countermodels and coarse models

A Heyting algebra in which a formula is not $\top$ is a proof that the formula is not intuitionistically derivable (by Theorem 4). Such countermodels can be found by search. The first experiment enumerates every topology on at most three points and evaluates eight classical tautologies in each.

Heyting algebras of open sets on small spacesPythonExhaustive finite checkCounterexampleComputationally tested

"""Heyting algebras of open sets: where excluded middle fails, and where it cannot.

Every topology is a Heyting algebra: meet is intersection, join is union, and
U => V is the interior of (X \\ U) | V, the largest open W with W & U <= V.
We enumerate all 29 topologies on a three-point set, check the Heyting law
W <= (U => V)  iff  W & U <= V  exhaustively, find which topologies are
Boolean, and evaluate classical tautologies under every valuation.

A failure is a genuine countermodel: by the soundness theorem proved in the
lesson (and in Lean), a formula that is not top in some Heyting algebra is not
derivable in intuitionistic propositional logic. Success on these small spaces
is only finite evidence of derivability.
"""

import itertools

def subsets(points):
    """All subsets of ``points`` as frozensets, smallest first."""
    pts = sorted(points)
    return [frozenset(c) for r in range(len(pts) + 1)
            for c in itertools.combinations(pts, r)]

def is_topology(opens, space):
    """Contains the empty set and the space, closed under union and meet."""
    if frozenset() not in opens or space not in opens:
        return False
    return all(a | b in opens and a & b in opens for a in opens for b in opens)

def all_topologies(n):
    """All topologies on {0, ..., n-1}, as a list of frozensets of opens."""
    space = frozenset(range(n))
    middle = [s for s in subsets(space) if s and s != space]
    found = []
    for k in range(len(middle) + 1):
        for family in itertools.combinations(middle, k):
            opens = frozenset(family) | {frozenset(), space}
            if is_topology(opens, space):
                found.append(opens)
    return found

def implies(opens, u, v):
    """Heyting implication: the union of all opens W with W & u <= v."""
    return frozenset().union(*[w for w in opens if w & u <= v])

def neg(opens, u):
    """Pseudo-complement: the largest open set disjoint from u."""
    return implies(opens, u, frozenset())

def residuation_holds(opens):
    """Check W <= (U => V) iff W & U <= V for all opens W, U, V."""
    return all((w <= implies(opens, u, v)) == (w & u <= v)
               for w in opens for u in opens for v in opens)

def is_boolean(opens, space):
    """Boolean iff U | not U is the whole space for every open U."""
    return all(u | neg(opens, u) == space for u in opens)

def evaluate(formula, opens, valuation):
    """Value of a formula: an atom name or (op, args...), op in and/or/imp/not."""
    if isinstance(formula, str):
        return valuation[formula]
    op, *args = formula
    vals = [evaluate(a, opens, valuation) for a in args]
    if op == "and":
        return vals[0] & vals[1]
    if op == "or":
        return vals[0] | vals[1]
    if op == "imp":
        return implies(opens, vals[0], vals[1])
    return neg(opens, vals[0])

def atoms(formula):
    """The set of atom names in a formula."""
    if isinstance(formula, str):
        return {formula}
    return set().union(*[atoms(a) for a in formula[1:]])

def countermodel(formula, max_points=3):
    """First (space, opens, valuation) where the formula is not top, or None."""
    names = sorted(atoms(formula))
    for n in range(1, max_points + 1):
        space = frozenset(range(n))
        for opens in all_topologies(n):
            ordered = sorted(opens, key=lambda s: (len(s), sorted(s)))
            for values in itertools.product(ordered, repeat=len(names)):
                valuation = dict(zip(names, values))
                if evaluate(formula, opens, valuation) != space:
                    return space, opens, valuation
    return None

FORMULAS = [
    ("p or not p", ("or", "p", ("not", "p"))),
    ("not not (p or not p)", ("not", ("not", ("or", "p", ("not", "p"))))),
    ("not not p -> p", ("imp", ("not", ("not", "p")), "p")),
    ("p -> not not p", ("imp", "p", ("not", ("not", "p")))),
    ("((p -> q) -> p) -> p", ("imp", ("imp", ("imp", "p", "q"), "p"), "p")),
    ("not p or not not p", ("or", ("not", "p"), ("not", ("not", "p")))),
    ("(p -> q) or (q -> p)", ("or", ("imp", "p", "q"), ("imp", "q", "p"))),
    ("not (p and q) -> not p or not q",
     ("imp", ("not", ("and", "p", "q")), ("or", ("not", "p"), ("not", "q")))),
]

def show(s):
    """Print a set of points compactly, e.g. {0,1}."""
    return "{" + ",".join(str(x) for x in sorted(s)) + "}"

def main():
    print("Topologies on n points; residuation law; how many are Boolean:")
    for n in range(1, 4):
        space = frozenset(range(n))
        tops = all_topologies(n)
        ok = all(residuation_holds(t) for t in tops)
        boolean = sum(is_boolean(t, space) for t in tops)
        print(f"  n = {n}: {len(tops):2d} topologies, Heyting law holds in all:"
              f" {ok}, Boolean: {boolean}")
    sierp = frozenset([frozenset(), frozenset([1]), frozenset([0, 1])])
    u = frozenset([1])
    print("Sierpinski space, opens {}, {1}, {0,1}; U = {1}:")
    print(f"  not U = {show(neg(sierp, u))}, U or not U = "
          f"{show(u | neg(sierp, u))}, not not U = {show(neg(sierp, neg(sierp, u)))}")
    print()
    print("Classical tautologies on all spaces with at most 3 points:")
    for name, formula in FORMULAS:
        found = countermodel(formula)
        if found is None:
            print(f"  {name:<34} top in every case checked")
        else:
            space, opens, val = found
            where = ", ".join(f"{k}={show(v)}" for k, v in sorted(val.items()))
            print(f"  {name:<34} FAILS: {len(space)} points, "
                  f"{len(opens)} opens, {where}")
    print()
    print("Epistemic status: exhaustive over all topologies on at most three")
    print("points. Each FAILS line is a genuine countermodel, so by soundness that")
    print("formula is not derivable intuitionistically. A formula that is top in")
    print("every case checked is only supported by finite evidence here; the")
    print("derivations (e.g. of not not (p or not p)) are what prove it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Two points already refute excluded middle, double-negation elimination and Peirce's law. That is the Sierpiński space: two possible worlds, one of which "knows more". Weak excluded middle $\neg P \vee \neg\neg P$ , the De Morgan law $\neg(P \wedge Q) \to \neg P \vee \neg Q$ and Dummett's law $(P \to Q) \vee (Q \to P)$ need three points, arranged in a "V" in which two incomparable opens meet only in $\varnothing$ . These laws axiomatise intermediate logics between intuitionistic and classical logic. The first two are equivalent over intuitionistic logic and give the logic usually called KC. Dummett's law gives the strictly stronger Gödel–Dummett logic LC. The search counts Boolean topologies too: they are exactly the partition topologies, 1, 2 and 5 of them (the Bell numbers).

The second experiment looks at the λ-calculus side. Church numerals $\lambda f.\lambda x.\, f^n(x)$ are pairwise distinct normal forms. In a finite model, however, $f \mapsto f^n$ must eventually repeat.

λ-terms in finite sets: Church numerals and naturalityPythonExact computationExhaustive finite checkCounterexampleComputationally tested

"""Interpreting λ-terms in finite sets: sound, but too coarse to be complete.

The interpretation of the simply typed λ-calculus in Set sends the base type
to a set X. Two experiments with exact, exhaustive computation:

1. Church numerals n = λf.λx. f(f(...f(x))) are distinct normal forms, so no
   two are βη-equal. Over a finite X of size m their meanings f -> f^n must
   eventually repeat; we find the first coincidence for m = 1, 2, 3, 4.
2. The closed terms of type A×A -> A×A have four normal forms. Over X = {0, 1}
   there are 256 functions X×X -> X×X, and exactly the four definable ones are
   natural (commute with every map X -> X), as Yoneda predicts.

Friedman's theorem (1975) says that with an infinite base set, equality of
meanings is exactly βη-equality; part 1 shows why finiteness breaks this.
"""

import itertools
import math

def all_maps(m):
    """All functions {0..m-1} -> {0..m-1}, as tuples of images."""
    return list(itertools.product(range(m), repeat=m))

def compose_power(f, n):
    """The n-th iterate f^n of a map given as a tuple."""
    result = tuple(range(len(f)))
    for _ in range(n):
        result = tuple(f[x] for x in result)
    return result

def numeral_meaning(n, m):
    """Meaning of the Church numeral n over an m-element set: f -> f^n."""
    return tuple(compose_power(f, n) for f in all_maps(m))

def first_coincidence(m, limit=40):
    """Smallest (a, b), a < b <= limit, with numerals a, b equal over m points."""
    seen = {}
    for n in range(limit + 1):
        meaning = numeral_meaning(n, m)
        if meaning in seen:
            return seen[meaning], n
        seen[meaning] = n
    return None

def definable_pair_maps():
    """Meanings of the 4 closed normal terms λp.(πᵢ p, πⱼ p) of type A×A->A×A."""
    def term(i, j):
        return lambda a, b: ((a, b)[i], (a, b)[j])
    return {f"(p{i + 1}, p{j + 1})": term(i, j) for i in (0, 1) for j in (0, 1)}

def natural_pair_maps(m):
    """All g : X×X -> X×X, X of size m, with g(h a, h b) = (h×h)(g(a, b))."""
    pts = [(a, b) for a in range(m) for b in range(m)]
    maps = all_maps(m)
    found = []
    for images in itertools.product(pts, repeat=len(pts)):
        g = dict(zip(pts, images))
        if all(g[(h[a], h[b])] == (h[g[(a, b)][0]], h[g[(a, b)][1]])
               for h in maps for (a, b) in pts):
            found.append(g)
    return found

def main():
    print("1. Church numerals over an m-element base set X")
    print("   (numeral n means f -> f^n; gap = difference of the two numerals)")
    for m in range(1, 5):
        a, b = first_coincidence(m)
        lcm = math.lcm(*range(1, m + 1))
        print(f"   m = {m}: {len(all_maps(m)):3d} maps; numerals {a:2d} and"
              f" {b:2d} first agree; gap {b - a:2d}; lcm(1..{m}) = {lcm:2d}")
    print("   Distinct normal forms, same meaning: finite models are not complete.")
    print()
    print("2. Closed terms of type A*A -> A*A, interpreted over X = {0, 1}")
    natural = natural_pair_maps(2)
    pts = [(a, b) for a in range(2) for b in range(2)]
    definable = definable_pair_maps()
    print(f"   functions X*X -> X*X: {4 ** 4}; natural ones: {len(natural)}")
    tables = [tuple(g[p] for p in pts) for g in natural]
    for name, t in definable.items():
        table = tuple(t(*p) for p in pts)
        print(f"   term {name}: natural = {table in tables}")
    print()
    print("Epistemic status: exact and exhaustive for the sets checked. Part 1")
    print("exhibits genuine pairs of non-convertible terms that a finite model")
    print("cannot tell apart; it does not test Friedman's theorem, which needs an")
    print("infinite base set. Part 2 checks naturality only for endomaps of a")
    print("two-element set; the general statement is the Yoneda lemma.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

On an $m$ -element set the first coincidence is $f^{m-1} = f^{m-1 + \operatorname{lcm}(1, \dots, m)}$ . The output shows this for $m \le 4$ , and it follows in general from the structure of the full transformation monoid. Finite models are therefore sound but not complete for βη-equality, which is why Friedman's theorem needs an infinite base set. The second part shows the other side of the coin. Of the $256$ functions $X \times X \to X \times X$ on a two-element set $X$ , exactly four commute with every map $X \to X$ , and they are precisely the four that are definable by closed λ-terms. By the Yoneda lemma, $\mathrm{Nat}(\Hom(2, -), \Hom(2, -)) \cong \Hom(2, 2)$ has four elements. This is the first glimpse of parametricity: definable terms are uniform in the interpretation of the base type.

Explore

Explore: what truth tables cannot see

A classical truth table is evaluation in the two-element Boolean algebra $\{0, 1\}$ . Compare $\neg\neg(p \vee \neg p)$ with $p \vee \neg p$ below. Both are tautologies, so the truth table declares them equivalent.

Two classical tautologies

Equivalent in the two-element Boolean algebra, but not intuitionistically

Formula

Read as: ¬¬(p ∨ ¬p)

Compare with

Read as: p ∨ ¬p

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Tautology — true in all 2 rows.

Equivalent — the two formulas agree in all 2 rows.

p	¬p	p ∨ ¬p	¬(p ∨ ¬p)	¬¬(p ∨ ¬p)	p ∨ ¬p	Rows where they differ
T	F	T	F	T	T
F	T	T	F	T	T

2 rows: one for every way of making the 1 variables true or false.

Things to try:

Replace the comparison by ¬¬p → p, then by ((p → q) → p) → p (Peirce's law). Every one is a classical tautology, and the computation section exhibits a two-point topological space in which each fails.
Try (p → q) ∨ (q → p). It is a tautology too, but it is not intuitionistically derivable. Its smallest topological countermodel has three points.
Explain why no truth table can ever separate $\varphi$ from $\neg\neg\varphi$ . (Hint: in a Boolean algebra $\neg\neg a = a$ .) This is why Heyting algebras, Kripke models or topological spaces are needed to study intuitionistic logic.

Exercises

1. Categorical logic

Warm-upHuman

In the Heyting algebra $\mathcal{O}(\R)$ of open subsets of $\R$ , let $W = \R \setminus \{0\}$ . What are $\neg W$ and $\neg\neg W$ ?

Choose one

\neg W = \varnothing

and

\neg\neg W = \R

\neg W = \{0\}

and

\neg\neg W = W

\neg W = \varnothing

and

\neg\neg W = W

\neg W

is undefined because

W

is not closed

2. Categorical logic

Warm-upHuman

Which of these categories are cartesian closed? (Choose all that apply.)

Choose all that apply

\mathbf{Set}

The chain

0 \lt \tfrac12 \lt 1

as a poset category

\mathbf{Grp}

(\N, \le)

as a poset category

\mathbf{FinSet}

3. Categorical logic

CoreHuman

In the three-element Heyting algebra $0 \lt \tfrac12 \lt 1$ , for how many elements $a$ does $a \vee \neg a = 1$ hold?

4. Categorical logic

CoreHuman

Since $f^* \dashv \forall_f$ , the universal quantifier is a right adjoint, and right adjoints preserve limits (in a poset: meets). Which logical law is an instance of exactly this fact?

Choose one

\forall y\,(\varphi \wedge \psi) \iff \forall y\,\varphi \wedge \forall y\,\psi

\exists y\,(\varphi \vee \psi) \iff \exists y\,\varphi \vee \exists y\,\psi

\forall y\,(\varphi \vee \psi) \iff \forall y\,\varphi \vee \forall y\,\psi

\exists y\,(\varphi \wedge \psi) \iff \exists y\,\varphi \wedge \exists y\,\psi

5. Categorical logic

CoreHuman

In the proof that intuitionistic logic is sound for Heyting algebras, one rule needs the distributive law $c \wedge (a \vee b) = (c \wedge a) \vee (c \wedge b)$ . Which rule, and why does the distributive law hold in every Heyting algebra?

Choose one

\vee

-elimination; because

c \wedge -

is a left adjoint (of

c \Rightarrow -

) and so preserves joins

\to

-introduction; because every lattice is distributive

\vee

-introduction; because joins are least upper bounds

\to

-elimination; because

(a \Rightarrow b) \wedge a \le b

6. Categorical logic

CoreFormal

With forallAlong f S = {y | ∀ x, f x = y → x ∈ S}, which Lean statement says that ∀ is right adjoint to pulling back along f : X → Y (for S : Set X, T : Set Y)?

Choose one

f ⁻¹' T ⊆ S ↔ T ⊆ forallAlong f Sf '' S ⊆ T ↔ S ⊆ f ⁻¹' TforallAlong f S ⊆ T ↔ S ⊆ f ⁻¹' TT ⊆ forallAlong f S ↔ f '' S ⊆ T

7. Categorical logic

CoreHuman

How many closed βη-normal terms of type $A \times A \to A \times A$ are there, for a base type $A$ ?

8. Categorical logic

StretchHuman

A student claims: "Intuitionistic logic proves $\neg(P \vee \neg P)$ ; that is what rejecting excluded middle means." Which response is correct?

Choose one

The claim is false. In the two-element Boolean algebra

\neg(p \vee \neg p)

evaluates to

\bot

, so by soundness it is not derivable. In fact

\neg\neg(p \vee \neg p)

is derivable.The claim is true, because

p \vee \neg p

is not derivableThe claim is true in

\mathcal{O}(\R)

, since there

U \vee \neg U \ne \R

for

U = (0, \infty)

The question is meaningless, because intuitionistic logic has no negation

9. Categorical logic

StretchComputational

A finite topology is given as a set opens of frozensets. Write neg(opens, u), returning the pseudo-complement of the open set u (the union of all open sets disjoint from u), and is_boolean(opens, space), returning True exactly when u | neg(opens, u) == space for every open u.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Categorical semantics replaces set-theoretic semantics." It contains it. $\mathbf{Set}$ is one cartesian closed category (and one Boolean topos) among many: Heyting algebras, presheaf and sheaf categories, realizability toposes, categories of domains. Each is useful for a different purpose. Ordinary mathematics is still written in, and about, the model $\mathbf{Set}$ . The categorical view tells you which theorems remain true when you change the model.

Misconception

"Intuitionistic logic asserts that excluded middle is false." It does not assume excluded middle, and it proves $\neg\neg(P \lor \neg P)$ , so excluded middle can never be refuted. $\neg(P \lor \neg P)$ is not derivable: it evaluates to $\bot$ in the two-element Boolean algebra. Every intuitionistic theorem is also a classical theorem.

Misconception

"Since $\mathbf{Set}$ is complete for βη-equality (Friedman), it is also complete for provability." No. Friedman's theorem is about equations between terms. For inhabitation (Curry–Howard provability), $\mathbf{Set}$ is classical. Interpret the base types as any sets: the type $((A \to B) \to A) \to A$ of Peirce's law always gets a non-empty interpretation (check the cases $\llbracket A \rrbracket = \varnothing$ and $\llbracket A \rrbracket \ne \varnothing$ ), yet no closed λ-term has this type. Detecting intuitionistic unprovability needs non-Boolean models.

Misconception

"Cartesian closed means having all limits." A CCC needs only finite products and exponentials. $\mathbf{FinSet}$ is cartesian closed but has no infinite products, and a finite chain is a Heyting algebra regardless of completeness. Conversely, $\mathbf{Grp}$ has all limits but is not cartesian closed.

ViewpointsH

Many ways of seeing

Topology— Truth values are open sets

The open sets of a space form a Heyting algebra. A proposition interpreted as an open set $U$ is "true at the points of $U$ ". Openness is the mathematical shape of observability: if a property holds at a point, it holds nearby. Excluded middle fails because a property and its pseudo-complement can both fail at a boundary point. This is more than an example. Tarski (1938) proved that intuitionistic propositional logic is complete for the topological semantics on $\R$ , so a formula is derivable if and only if it evaluates to $\R$ under every assignment of open subsets of $\R$ . Stone (1937) represented Heyting algebras, then called "Brouwerian logics", by open sets. In modern form, every Heyting algebra embeds in the Heyting algebra of up-sets of its prime filters, and these up-sets are the open sets of a topology. Finite Kripke models are the special case of finite spaces, whose open sets are the up-sets of a preorder. In the other direction, frames (complete lattices in which finite meets distribute over arbitrary joins; equivalently, complete Heyting algebras) are the "spaces without points" of locale theory, and sheaves on a space form a topos whose internal logic is this topological logic, extended to quantifiers.

Geometry— ∃ is a projection

Theorem 3 says that existential quantification is the direct image under a projection, the shadow of a set. Eliminating a quantifier is therefore a theorem in geometry. The Tarski–Seidenberg theorem, that the projection $\R^{n+1} \to \R^n$ of a semialgebraic set is semialgebraic, is equivalent to quantifier elimination for the real field. Chevalley's theorem, that the image of a constructible set under a morphism of varieties over an algebraically closed field is constructible, is the corresponding statement for algebraically closed fields (see model theory and algebraic geometry). $\forall_f$ is the dual "everything over this point" operation. Beck–Chevalley says that taking shadows commutes with base change. For instance, for a subset $Z$ of the base, the shadow of the part of $S$ lying over $Z$ is the shadow of $S$ intersected with $Z$ .

Algebra— Free algebras measure a logic

The Lindenbaum–Tarski algebra on $n$ propositional variables is the free Heyting algebra on $n$ generators. Free algebras show how much a logic can distinguish. The free Boolean algebra on one generator $p$ has four elements, $\bot, p, \neg p, \top$ . The free Heyting algebra on one generator is infinite: the Rieger–Nishimura lattice (Rieger 1949, Nishimura 1960) contains $p, \neg p, \neg\neg p, p \vee \neg p, \neg\neg p \to p, \dots$ as pairwise inequivalent formulas. Algebraically, soundness and completeness (Theorems 4 and 5) say that intuitionistic propositional logic is the equational theory of Heyting algebras, a variety in the sense of universal algebra. Intermediate logics such as Dummett's correspond to subvarieties: Dummett's law axiomatises the subvariety generated by the linearly ordered Heyting algebras.

Computation— Compiling through a cartesian closed category

The interpretation of Theorem 2 is a compiler. It translates λ-terms, with their named variables, into variable-free combinators: projections, pairing, $\Lambda$ and $\mathrm{ev}$ . The Categorical Abstract Machine of Cousineau, Curien and Mauny (1985, journal version 1987) executes exactly these CCC combinators, and it gave the original Caml implementation its name. In the other direction, Curry–Howard makes proof assistants possible. Lean checks a proof by type-checking a term, and normalising a proof is running a program. #print axioms exposes the constructive/classical boundary: the proof of ¬¬(P ∨ ¬P) in this lesson uses no axioms, whereas proofs that use excluded middle depend on Classical.choice.

Logic— Hyperdoctrines: logic over a category of contexts

Lawvere's hyperdoctrines organise first-order logic categorically. There is a base category of contexts (objects are lists of variables, morphisms are tuples of terms), a poset or Heyting algebra $P(\Gamma)$ of formulas in each context, substitution functors $t^*$ , and quantifiers as their adjoints, subject to Beck–Chevalley and Frobenius. Equality is $\exists$ along a diagonal. This is the logic of a first-order theory with every structural rule made explicit, and the same pattern governs dependent type theory. There, Seely (1984) matched $\Sigma$ - and $\Pi$ -types with the left and right adjoints to pullback in a locally cartesian closed category. The precise correspondence needs care with substitution, which holds only up to isomorphism (Hofmann 1994).

Physics— A logic that is not Heyting

Birkhoff and von Neumann (1936) proposed that the propositions about a quantum system are the closed subspaces of a Hilbert space, ordered by inclusion. Meet is intersection and join is closed span. This lattice is not distributive. In $\C^2$ , take three distinct lines $L_1, L_2, L_3$ : then $L_1 \wedge (L_2 \vee L_3) = L_1 \wedge \C^2 = L_1$ , but $(L_1 \wedge L_2) \vee (L_1 \wedge L_3) = 0$ . A Heyting algebra is always distributive, because $a \wedge -$ is a left adjoint, so in quantum logic conjunction with $a$ has no right adjoint. There is no implication obeying the deduction theorem. This contrast clarifies what Heyting algebras capture. It also motivates the topos-theoretic approaches to quantum theory of Isham, Butterfield and Döring, which replace the non-distributive lattice by a Heyting algebra of subobjects in a presheaf topos. These remain a research programme, not settled physics.

ExplanationH

The landscape and where to go next

Dependent types and locally cartesian closed categories. Replacing $\times$ and $\to$ by $\Sigma$ and $\Pi$ moves the correspondence from CCCs to locally cartesian closed categories, where every slice $\mathcal{C}/X$ is cartesian closed. Lean's own type theory is a dependent type theory of this kind, with inductive types and universes added.
Toposes. A topos is a category in which the subobjects of each object form a Heyting algebra, functorially, with quantifiers as adjoints. In other words, it is a hyperdoctrine built from the category itself. Its internal logic is higher-order intuitionistic logic (Lambek and Scott, Part II).
Homotopy type theory. Identity types in dependent type theory have models in which equalities are paths. This leads to homotopy type theory and its semantics in higher categories.
Proof theory. Normalisation of proofs (Gentzen, Prawitz) is β-reduction under Curry–Howard. Categorical coherence theorems are often normalisation theorems in disguise (see proof theory).
Linear logic and monoidal closed categories. Dropping the diagonal $A \to A \times A$ (duplication of hypotheses) replaces cartesian closed categories by symmetric monoidal closed ones; see monoidal categories.

History & global context

History and global context

Intuitionism. L. E. J. Brouwer (Netherlands) criticised the unrestricted use of excluded middle from 1907 onwards. Valery Glivenko (Moscow) proved his double-negation theorem in 1929. Arend Heyting (Netherlands) formalised intuitionistic logic in 1930, and Andrey Kolmogorov (Moscow) gave its "problem" interpretation in 1932. Together with Brouwer and Heyting this became the Brouwer–Heyting–Kolmogorov interpretation.
Algebraic and topological semantics. Marshall Stone (1937) and Alfred Tarski (1938) connected intuitionistic logic with lattices of open sets. McKinsey and Tarski developed the algebra of topology in the 1940s. Ladislav Rieger (Prague, 1949) and Iwao Nishimura (Japan, 1960) described the free Heyting algebra on one generator, and Saul Kripke (1965) introduced his possible-worlds semantics.
Propositions as types. Haskell Curry noticed the match between combinators and axioms of implicational logic (1934, and with Robert Feys in 1958). William Howard's notes on "formulae-as-types" circulated in 1969 and were published in 1980.
Categories. Samuel Eilenberg and Saunders Mac Lane introduced categories in 1945, and Daniel Kan introduced adjoint functors in 1958. F. William Lawvere's thesis (1963) and papers "Adjointness in foundations" (1969) and on equality in hyperdoctrines (1970) made adjoints the organising principle of logic. Joachim Lambek's "Deductive systems and categories" (1968–1972) and "From λ-calculus to cartesian closed categories" (1980) completed the third side of the correspondence, and Lambek and Philip Scott's book (1986) became its standard reference. Harvey Friedman's completeness theorem for set-theoretic models appeared in 1975. Robert Seely's work on locally cartesian closed categories appeared in 1984.

One law, three readings

The dictionary

Definitions

Examples and non-examples

The central theorems

Formalisation in Lean

Countermodels and coarse models

Explore: what truth tables cannot see

Exercises

Common misconceptions

Many ways of seeing

The landscape and where to go next

History and global context

Further reading