We define the equational theory (Primitive Recursive Arithmetic) to be initial among Lawvere theories whose generator is a parametrized natural numbers object. The set of morphisms in 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
taking to the set consisting of -ary predicates in the language of PA, modulo provable equivalence in PA. If is a morphism of and , we let denote ; it can be described as the result of substituting or pulling back along . There is a corresponding “action” of on ,
which allows us to regard as a -module.
Let be the set of all formulas of PA, with the set of formulas with free variables. There is an equivalence relation on , where two formulas belong to the same equivalence class if they are provably equivalent in PA. Thus is the corresponding quotient map. Let denote the set of closed terms in the logical theory ; morphisms in the Lawvere theory are equivalence classes of terms, and we let be the corresponding quotient map. The map has a section which sends each morphism to the corresponding numeral term (the -fold successor of the zero term). Finally, we have a substitution map
that substitutes a closed term in for the free variable of , giving a closed formula .
There is a standard Gödel coding taking formulas to numerals,
and we define an application pairing to be the composite along the top of the following commutative diagram:
In other words, for all formulas and , we define the pairing , and according to the commutative diagram, we have the equation
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 in ) such that for all , we have .1
For every there is a fixed point in \Phi(0), i.e., a closed formula such that ( is provably equivalent to ).
Pick a formula such that , and then put . We have
Recall there is also a Gödel coding of PA proofs (certain sequences of PA formulas), .
There is a binary primitive recursive predicate such that is true in if is the code of a proof of a sentence (a closed formula) with code . Thus there is an unary recursive predicate . Similarly, there is an unary recursive predicate .
(Gödel’s First Incompleteness Theorem) There exists a sentence in the language of PA such that is logically equivalent to the PA-sentence (whose interpretation in the model is that has no PA proof).
Thus, if is false in , then 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 is true in , but then this true sentence (in the language of PA) has no PA proof.
Indeed, let be a formula that represents the unary predicate , and let be a fixed point in the sense . The equality here is logical equivalence, and 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.
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.” ↩