Todd Trimble
Hyperdoctrine version of Gödel incompleteness

Categorical preliminaries

We define the equational theory PRA (Primitive Recursive Arithmetic) to be initial among Lawvere theories whose generator 1 is a parametrized natural numbers object. The set of morphisms 01 in PRA is the set of equivalence classes of closed terms, and is identified with the set of numerals . (This 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)= to the set T(j) consisting of j-ary predicates in the language of PA, modulo provable equivalence in PA. If f:jk is a morphism of PRA and RT(k), we let f *(R) denote T(f)(R)T(j); it can be described as the result of substituting or pulling back R along f. There is a corresponding “action” of PRA on T,

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 T as a PRA-module.

Syntactic terminology and notation

Let Form(PA) be the set of all formulas of PA, with Φ(j) the set of formulas with j free variables. There is an equivalence relation on Φ(j), where two formulas F,F belong to the same equivalence class [F] if they are provably equivalent in PA. Thus []:Φ(j)T(j) is the corresponding quotient map. Let Term(0) denote the set of closed terms in the logical theory PRA; morphisms 01 in the Lawvere theory PRA are equivalence classes of terms, and we let ev:Term(0)PRA(0,1) be the corresponding quotient map. The map ev has a section num:PRA(0,1)Term(0) which sends each morphism 0n1 to the corresponding numeral term (the n-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 τ in for the free variable of FΦ(1), giving a closed formula sub(τ,F)Φ(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 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) and RΦ(1), we define the pairing FRsub(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:11 in PRA) such that for all tΦ(1), we have dcode(t)=code(tt).1


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


Pick a formula tΦ(1) such that [t]=d *[R], and then put s=tt. 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).


There is a binary primitive recursive predicate Pf such that Pf(p,x) is true in if p is the code of a proof of a sentence (a closed formula) with code x. Thus there is an unary recursive predicate Prov pPf(p,x)T(1). Similarly, there is an unary recursive predicate R=¬ProvT(1).


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

Thus, if s is false in , then s 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 s is true in , but then this true sentence (in the language of PA) has no PA proof.


Indeed, let R be a formula that represents the unary predicate ¬Prov, and let s be a fixed point in the sense [s]=[sR]. The equality here is logical equivalence, and [sR]=code(s) *(¬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 02:08:27 by Todd Trimble