# Todd Trimble Hyperdoctrine version of Gödel incompleteness

### Categorical preliminaries

We define the equational theory $\mathbf{PRA}$ (Primitive Recursive Arithmetic) to be initial among Lawvere theories whose generator $1$ is a parametrized natural numbers object. The set of morphisms $0 \to 1$ in $\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: \mathbf{PRA}^{op} \to Bool$

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

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

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

### Syntactic terminology and notation

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

$sub: Term(0) \times \Phi(1) \to \Phi(0)$

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

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

$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:

$\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 $F \in Form(PA)$ and $R \in \Phi(1)$, we define the pairing $F \cdot R \coloneqq sub(num (code(F)), R)$, and according to the commutative diagram, we have the equation

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

which will be used in our diagonalization result.

### Diagonalization

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

###### Lemma

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

###### Theorem

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

###### Proof

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

$\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.

### Incompleteness

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

###### Lemma

There is a binary primitive recursive predicate $Pf$ such that $Pf(p, x)$ is true in $\mathbb{N}$ 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 \coloneqq \exists_p Pf(p, x) \in T(1)$. Similarly, there is an unary recursive predicate $R = \neg Prov \in T(1)$.

###### Theorem

(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)^\ast (\neg Prov)$ (whose interpretation in the model $\mathbb{N}$ is that $s$ has no PA proof).

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

###### Proof

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

###### Remark

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.

## References

• Noson S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points, arXiv:math/0305282 (web)

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