Todd Trimble
Hyperdoctrine version of Gödel incompleteness

Categorical preliminaries

We define the equational theory PRA\mathbf{PRA} (Primitive Recursive Arithmetic) to be initial among Lawvere theories whose generator 11 is a parametrized natural numbers object. The set of morphisms 010 \to 1 in PRA\mathbf{PRA} is the set of equivalence classes of closed terms, and is identified with the set of numerals \mathbb{N}. (This \mathbb{N} will serve double duty in a moment, as being also the set of objects of the Lawvere theory.)

The first-order theory of Peano Arithmetic, PA for short, can be presented as a Boolean hyperdoctrine

T:PRA opBoolT: \mathbf{PRA}^{op} \to Bool

taking jOb(PRA)=j \in Ob(\mathbf{PRA}) = \mathbb{N} to the set T(j)T(j) consisting of jj-ary predicates in the language of PA, modulo provable equivalence in PA. If f:jkf: j \to k is a morphism of PRA\mathbf{PRA} and RT(k)R \in T(k), we let f *(R)f^\ast (R) denote T(f)(R)T(j)T(f)(R) \in T(j); it can be described as the result of substituting or pulling back RR along ff. There is a corresponding “action” of PRA\mathbf{PRA} on TT,

PRA(j,k)×T(k)actionT(j)\mathbf{PRA}(j, k) \times T(k) \stackrel{action}{\to} T(j)
(f,R)f *(R),(f, R) \mapsto f^\ast(R),

which allows us to regard TT as a PRA\mathbf{PRA}-module.

Syntactic terminology and notation

Let Form(PA)Form(PA) be the set of all formulas of PA, with Φ(j)\Phi(j) the set of formulas with jj free variables. There is an equivalence relation on Φ(j)\Phi(j), where two formulas F,FF, F' belong to the same equivalence class [F][F] if they are provably equivalent in PA. Thus []:Φ(j)T(j)[-]: \Phi(j) \to T(j) is the corresponding quotient map. Let Term(0)Term(0) denote the set of closed terms in the logical theory PRAPRA; morphisms 010 \to 1 in the Lawvere theory PRA\mathbf{PRA} are equivalence classes of terms, and we let ev:Term(0)PRA(0,1)ev: Term(0) \to \mathbf{PRA}(0, 1) be the corresponding quotient map. The map evev has a section num:PRA(0,1)Term(0)num: \mathbf{PRA}(0, 1) \to Term(0) which sends each morphism 0n10 \stackrel{'n'}{\to} 1 to the corresponding numeral term (the nn-fold successor of the zero term). Finally, we have a substitution map

sub:Term(0)×Φ(1)Φ(0)sub: Term(0) \times \Phi(1) \to \Phi(0)

that substitutes a closed term τ\tau in for the free variable of FΦ(1)F \in \Phi(1), giving a closed formula sub(τ,F)Φ(0)sub(\tau, F) \in \Phi(0).

There is a standard Gödel coding taking formulas to numerals,

code:Form(PA)PRA(0,1),code: Form(PA) \to \mathbf{PRA}(0, 1),

and we define an application pairing \cdot to be the composite along the top of the following commutative diagram:

Form(PA)×Φ(1) code×1 PRA(0,1)×Φ(1) num×1 Term(0)×Φ(1) sub Φ(0) 1×[] ev×[] [] PRA(0,1)×T(1) action T(0).\array{ Form(PA) \times \Phi(1) & \stackrel{code \times 1}{\to} & \mathbf{PRA}(0, 1) \times \Phi(1) & \stackrel{num \times 1}{\to} & Term(0) \times \Phi(1) & \stackrel{sub}{\to} & \Phi(0) \\ & & & _\mathllap{1 \times [-]} \searrow & \downarrow _\mathrlap{ev \times [-]} & & \downarrow _\mathrlap{[-]} \\ & & & & \mathbf{PRA}(0, 1) \times T(1) & \underset{action}{\to} & T(0). }

In other words, for all formulas FForm(PA)F \in Form(PA) and RΦ(1)R \in \Phi(1), we define the pairing FRsub(num(code(F)),R)F \cdot R \coloneqq sub(num (code(F)), R), and according to the commutative diagram, we have the equation

(1)[FR]=code(F) *([R]) [F \cdot R] = code(F)^\ast ([R])

which will be used in our diagonalization result.


The following result is routine from general recursive-arithmetic properties of Gödel coding:


There is a primitive recursive function (i.e., a morphism d:11d: 1 \to 1 in PRA\mathbf{PRA}) such that for all tΦ(1)t \in \Phi(1), we have dcode(t)=code(tt)d \circ code(t) = code (t \cdot t).1


For every RΦ(1)R \in \Phi(1) there is a fixed point in \Phi(0), i.e., a closed formula sΦ(0)s \in \Phi(0) such that [s]=[sR][s] = [s \cdot R] (ss is provably equivalent to sRs \cdot R).


Pick a formula tΦ(1)t \in \Phi(1) such that [t]=d *[R][t] = d^\ast [R], and then put s=tts = t \cdot t. We have

[tt] = code(t) *([t]) equation(1) code(t) *(d *[R]) = (dcode(t)) *([R]) (functoriality) = (code(tt)) *([R]) (bythelemma) = [(tt)R] equation(1)\array{ [t \cdot t] & = & code(t)^\ast ([t]) & equation\; (1) \\ & \coloneqq & code(t)^\ast (d^\ast [R]) & \\ & = & (d \circ code(t))^\ast ([R]) & (functoriality) \\ & = & (code (t \cdot t))^\ast ([R]) & (by\; the\; lemma)\\ & = & [(t \cdot t) \cdot R] & equation\; (1) }

as required.


Recall there is also a Gödel coding of PA proofs (certain sequences of PA formulas), code:Proof(PA)PRA(0,1)code: Proof(PA) \to \mathbf{PRA}(0, 1).


There is a binary primitive recursive predicate PfPf such that Pf(p,x)Pf(p, x) is true in \mathbb{N} if pp is the code of a proof of a sentence (a closed formula) with code xx. Thus there is an unary recursive predicate Prov pPf(p,x)T(1)Prov \coloneqq \exists_p Pf(p, x) \in T(1). Similarly, there is an unary recursive predicate R=¬ProvT(1)R = \neg Prov \in T(1).


(Gödel’s First Incompleteness Theorem) There exists a sentence ss in the language of PA such that ss is logically equivalent to the PA-sentence code(s) *(¬Prov)code(s)^\ast (\neg Prov) (whose interpretation in the model \mathbb{N} is that ss has no PA proof).

Thus, if ss is false in \mathbb{N}, then ss has a PA proof (so that PA proves a false statement in a model: is inconsistent). In classical logic, the only other alternative is that ss is true in \mathbb{N}, but then this true sentence (in the language of PA) has no PA proof.


Indeed, let RR be a formula that represents the unary predicate ¬Prov\neg Prov, and let ss be a fixed point in the sense [s]=[sR][s] = [s \cdot R]. The equality here is logical equivalence, and [sR]=code(s) *(¬Prov)[s \cdot R] = code(s)^\ast (\neg Prov) by equation (1).


The proof of theorem 1 was written to lay bare its provenance as a special case of Lawvere’s fixed point theorem, and its essential kinship with the structure of the standard fixpoint combinator in combinatory algebra. See Yanofsky’s article below.


  1. This and the next lemma demonstrate the essential truth of Paul Taylor’s quip (Practical Foundations of Mathematics, p. 192): “Lemmas do the work in mathematics: Theorems, like management, just take the credit. A good lemma also survives a philosophical or technological revolution.”

Revised on August 18, 2013 at 02:08:27 by Todd Trimble