Lawvere's Theorem: Generalizing Cantor, Russell, Turing, Tarski, and Gödel

Students of mathematical logic would have at some point noticed that Cantor’s proof of the uncountability of the reals, Russell’s set-theoretic paradox, Turing’s halting problem, Gödel’s incompleteness theorem, and Tarski’s undefinability theorem all share a similarity. They all employ a diagonal argument, whereby one “feeds” an argument to itself. This similarity can be formulated precisely in the language of category theory.

Lawvere’s Theorem

Definition. A category $\mathcal{C}$ is Cartesian closed if it satisfies the following.

1. $\mathcal{C}$ has a terminal object $1$.
2. $\mathcal{C}$ admits arbitrary products of finitely many objects.
3. For every $B \in \mathcal{C}$, $(-) \times B : \mathcal{C} \to \mathcal{C}$ has a right adjoint.

We call the right adjoint of $(-) \times B$ the exponential and denote $(-)^B$. Thus,

naturally in $A, B, C$. Thus Cartesian closed category is a generalization of currying. Until further notice, we assume that $\mathcal{C}$ is Cartesian closed.

Definition. The diagonalization $\Delta_A$ of $A \in \mathcal{C}$ is the unique map induced by the following diagram:

Definition. A point of $X \in \mathcal{C}$ is a morphism $1 \to X$.

Note that a point is a category-theoretic generalization of an element of a set. For example, in $\mathbf{Set}$, $\Delta_A: A \to A \times A$ is the map $a \mapsto (a, a)$.

We can thus generalize the notion of surjectivity.

Definition. $f: X \to Y$ is point surjective if for every point $y \in Y$, there exists a point $x \in X$ such that $f\circ x = y$.

I will also write $f(x) = y$ in place of $f \circ x = y$.

The following gives a category-theoretic generalization of the diagonal argument.

Lawvere’s Theorem. Let $\mathcal{C}$ be a Cartesian closed category. If $f: A \to B^A$ is point surjective, for every $g: B \to B$, there exists a point $b$ of $B$ such that $g(b) = b$.

Proof. Let $\bar{f} : A \times A \to B$ be the adjoint of $f$. Define $\phi: A \to B$ as $g \circ \bar{f} \circ \Delta_A$.

Since

let $\bar{\phi} : 1 \to B^A$ be the adjoint of $\phi$. By point surjectivity of $f$, there exists a point $a: 1 \to A$ such that $f(a) = \bar{\phi}$. By naturality of the adjunction, we have the following commutative diagram.

Chasing $\bar f$ around the square, and identifying $1 \times A$ with $A$ (under which $a \times \mathrm{id}_A$ becomes $\langle a \circ \operatorname{!}_A, \mathrm{id}_A \rangle : A \to A \times A$), we obtain

Hence, since $\langle a \circ \operatorname{!}_A, \mathrm{id}_A \rangle \circ a = \langle a, a \rangle = \Delta_A \circ a$,

Let $b := \bar f \circ \Delta_A \circ a$. The following diagram then commutes.

In particular, $g(b) = g \circ \bar f \circ \Delta_A \circ a = \phi(a) = \bar f \circ \Delta_A \circ a = b$. ■

Cantor and Russell

Corollary (Cantor). In $\mathbf{Set}$, there is no (point) surjective map $f: A \to 2^A$.

Proof. Assume otherwise. Then by Lawvere’s theorem, every map $2 \to 2$ has a fixed point. However, $0 \mapsto 1, 1 \mapsto 0$ does not have a fixed point. ■

Corollary (Russell). The axiom of naive comprehension is inconsistent.

Proof. Assume naive comprehension, and suppose the sets it produces form a Cartesian closed category as in $\mathbf{Set}$. Then $\phi(x): x = x$ defines the set of all sets $S$, and $2^S$ is the set of all propositions over $S$. Consider

By naive comprehension, every $P \in 2^S$ determines a set ${y : P(y)}$, so $f$ is (point) surjective. This contradicts Lawvere’s theorem, with $0 \mapsto 1, 1 \mapsto 0$. (Unwinding the proof, the point $a$ is the set ${x : x \notin x}$.) ■

Weak point-surjectivity

Let $\mathcal{C}_{\mathsf{PA}}$ be the category of decidable sets, i.e.

• Objects: Decidable subsets of $\mathbb{N}$ modulo PA-provable equivalence.

• Morphisms: Functions that PA proves to be total (modulo PA-provable equality).

Then $1 = {0}$ is the terminal object, and

is the product, where $\langle \cdot, \cdot \rangle$ is the code for a pair.

We prove the following lemma:

Lemma. Assuming $\mathsf{PA}$ is consistent, $\mathcal{C}_\mathsf{PA}$ is not Cartesian closed.

Proof of the lemma. Assume otherwise. Then a point of $2^\mathbb{N}$ is adjoint to a provably total function $\mathbb{N} \to 2$. In particular, $2^\mathbb{N}$ has a point $e_0$, adjoint to the constant function $0$. Since $2^\mathbb{N}$ is an object of $\mathcal{C}_\mathsf{PA}$, it is a decidable subset $E \subseteq \mathbb{N}$, with inclusion $i : E \to \mathbb{N}$.

Define $\Theta: \mathbb{N} \to 2^\mathbb{N}$ such that

Then $\Theta$ is a morphism (i.e. provably total, since $E$ is decidable), and $\Theta \circ i = \mathrm{id}_E$. Hence for every point $p$ of $2^\mathbb{N}$, $\Theta(i \circ p) = p$, so $\Theta$ is point surjective. Hence, by Lawvere’s theorem, any morphism $h: 2 \to 2$ has a fixed point. But then $0 \mapsto 1, 1 \mapsto 0$ also has a fixed point, which implies $\mathsf{PA} \vdash 0 = 1$. □

So Lawvere’s theorem, as stated, cannot be applied inside the categories where computation and arithmetic live. Fortunately, the proof never used exponentials: they only package “every $g$ has a code” into a single morphism $f : A \to B^A$. Dropping them, we get the following.

Definition. Let $\mathcal{C}$ have finite products. A morphism $\phi : A \times A \to B$ is weakly point surjective if for every $h : A \to B$ there is a point $a$ of $A$ such that $\phi(\langle a, x \rangle) = h(x)$ for every point $x$ of $A$.

Lawvere’s Theorem (finite products). Let $\mathcal{C}$ be a category with finite products. If $\phi : A \times A \to B$ is weakly point surjective, then for every $g : B \to B$, there exists a point $b$ of $B$ such that $g(b) = b$.

Proof. Let $h := g \circ \phi \circ \Delta_A$. Choose $a$ as in the definition, and let $b := \phi \circ \langle a, a \rangle$. Then

The Cartesian closed version is the special case $\phi = \bar f$.

Turing, Tarski, and Gödel

Corollary (Turing). The halting problem is undecidable.

Proof. Let $\mathbf{Rec}$ be the category whose objects are decidable subsets of $\mathbb{N}$ and whose morphisms are total computable functions (not necessarily provably total). We will equivocate decidable subsets with its corresponding decision program. As with $\mathcal{C}_\mathsf{PA}$, it has finite products via the pairing code, with $1 = {0}$ and $2 = {0, 1}$.

Assume that the halting problem is decidable, i.e. there exists a morphism $h : \mathbb{N} \times \mathbb{N} \to 2$ such that $h(e, n) = 1$ if program $e$ halts on input $n$, and $h(e, n) = 0$ otherwise. For a morphism $f: \mathbb{N} \to 2$, let $e_g$ be the program

on input n:
  if f(n) = 1: return
  else: infinite loop

Then $h(e_g, n) = f(n)$ for every $n$, so $h$ is weakly point surjective. By Lawvere’s theorem, $0 \mapsto 1, 1 \mapsto 0$ has a fixed point, a contradiction. ■

Corollary (Tarski). There is no formula $\mathrm{True}(x)$ such that

\[\mathbb{N} \models \mathrm{True}(\ulcorner \sigma \urcorner) \iff \mathbb{N} \models \sigma\]

for every sentence $\sigma$.

Proof. Fix a Gödel numbering $\psi_0, \psi_1, \dots$ of the formulas with one free variable. Let $\mathbf{Def}$ be the category whose objects are $\mathbb{N}^k \; (k = 0, 1, 2, …)$ and $2$, and whose morphisms are functions definable in the standard arithmetic.

Suppose $\mathrm{True}$ exists. The substitution function $\mathrm{sub}(m, n) = \ulcorner \psi_m(\bar n) \urcorner$ is computable, hence definable. So

is a morphism of $\mathbf{Def}$. It is weakly point surjective: if $g : \mathbb{N} \to 2$ is defined by a formula $\gamma(x, y)$, then $\psi(x) := \gamma(x, 1)$ satisfies $\phi(\ulcorner \psi \urcorner, n) = g(n)$. But $0 \mapsto 1, 1 \mapsto 0$ is definable and has no fixed point, contradicting Lawvere’s theorem. ■

For Gödel, recall the following fact about Robinson arithmetic $\mathsf{Q}$.

For every decidable $D \subseteq \mathbb{N}$, there is a formula $\psi_D(x)$ such that $n \in D \Rightarrow \mathsf{Q} \vdash \psi_D(\bar n)$ and $n \notin D \Rightarrow \mathsf{Q} \vdash \neg\psi_D(\bar n)$.

Corollary (Gödel). For every consistent, recursively enumerable axiomatization $T \supseteq \mathsf{Q}$ of arithmetic, there exists an arithmetical truth unprovable in $T$.

Proof. We prove the following lemma:

Lemma. If $T$ is a consistent extension of $\mathsf{Q}$, then the set of theorems of $T$ is undecidable.

Proof. Suppose it is decidable, and work in $\mathbf{Rec}$. Define

This is computable, since $\mathrm{sub}$ is computable and $T$ is decidable. It is also weakly point surjective; given a computable $g : \mathbb{N} \to 2$, let $D = g^{-1}(1)$. We then have:

• If $g(n) = 1$, then $T \vdash \psi_D(\bar n)$, so $\phi(\ulcorner \psi_D \urcorner, n) = 1$.
• If $g(n) = 0$, then $T \vdash \neg\psi_D(\bar n)$, so by consistency $T \nvdash \psi_D(\bar n)$, and $\phi(\ulcorner \psi_D \urcorner, n) = 0$.

By Lawvere’s theorem, $0 \mapsto 1, 1 \mapsto 0$ has a fixed point, a contradiction. □

Now suppose that $T$ is complete. Then the following procedure is total, with which $T$ becomes decidable.

for n in ℕ:
  if n is a proof of φ:
    return True
  if n is a proof of ¬φ:
    return False

This contradicts the lemma above. ■

A few remarks:

1. The argument uses only consistency, not $\omega$-consistency, so it has the strength of the Gödel–Rosser theorem.

2. Unwinding the proof, the point $a$ codes a formula representing $n \mapsto [T \nvdash \psi_n(\bar n)]$, so $\psi_a(\bar a)$ is the Gödel sentence; i.e. the sentence “I am not provable.”