nLab
incompleteness theorem

Context

Foundations

(0,1)(0,1)-Category theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Incompleteness theorems

Idea

In logic, an incompleteness theorem expresses limitations on provability within a (consistent) formal theory. Most famously it refers to a pair of theorems due to Kurt Gödel; the first incompleteness theorem says roughly that for any consistent theory TT containing arithmetic and whose axioms form a recursive set, there is an arithmetic sentence which is true for the natural numbers \mathbb{N} that cannot be proven in TT. The second incompleteness theorem shows that for such theories TT, the sentence can be taken to be a suitable arithmetization of the statement of consistency of TT itself, i.e., that no such theory “can demonstrate its own consistency” – can prove an arithmetic statement that encodes the assertion of its consistency.

An incompleteness theorem can be read as an undecidability result: there are formal propositions pp in the theory such that neither pp nor its negation ¬p\neg{p} have proofs in the theory. As such, it is part of a long history; for example, axiom systems for Euclidean geometry not including the parallel postulate might not decide the parallel postulate, as shown by models for both Euclidean and non-Euclidean geometry. What was novel about Gödel’s results is that they worked directly at the level of syntax and applied to any (effectively generated) extension of arithmetic, producing sentences which in effect imply their unprovability.

To some extent, Gödel’s incompleteness theorems have always had an air of mystery about them, or at least a reputation of being exceedingly difficult or subtle. The major insight of Gödel, that items in formal logic can be encoded within the recursive structures afforded by arithmetic (Gödel numbering), is of course a signal achievement not to be underestimated, and the detailed working out of the result that the provability predicate can be encoded as a recursive set can be said to form the technical core of this work. But the punchline, in the form of his diagonalization argument that produces a true1 but unprovable sentence, should be seen for what it is: one of many diagonalization arguments (including for example Cantor's theorem) that are essentially alike in structure, and familiar to all mathematicians.

In an interview (Lawvere 07) not long after Gödel’s 100th birthday, William Lawvere answered the question

We have recently celebrated Kurt Gödel’s 100th birthday. What do you think about the extra-mathematical publicity around his incompleteness theorem?

by saying (reproduced in Lawvere 69 reprint, p. 2):

“In ‘Diagonal arguments and Cartesian closed categories’ (Lawvere 69) we demystified the incompleteness theorem of Gödel and the truth-definition theory of Tarski by showing that both are consequences of some very simple algebra in the Cartesian-closed setting. It was always hard for many to comprehend how Cantor’s mathematical theorem could be re-christened as a “paradox” by Russell and how Gödel’s theorem could be so often declared to be the most significant result of the 20th century. There was always the suspicion among scientists that such extra-mathematical publicity movements concealed an agenda for re-establishing belief as a substitute for science. Now, one hundred years after Gödel’s birth, the organized attempts to harness his great mathematical work to such an agenda have become explicit.

Yuri Manin writes in Manin02, p. 7:

Baffling discoveries such as Gödel’s incompleteness of arithmetic lose some of their mystery once one comes to understand their content as a statement that a certain algebraic structure simply is not finitely generated with respect to the allowed composition laws.

This diagonalization result, so often obscured, should be laid bare as the simple piece of algebra that it is. We give one approach here, based on the algebra of hyperdoctrines.

Gödel's incompleteness theorems

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 hom-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 \mathbb{N} of numerals. (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 opBooleanAlgebraT: \mathbf{PRA}^{op} \to BooleanAlgebra

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.

Diagonalization

The following result is routine from general recursive-arithmetic properties of Gödel coding; it applies to any extension of PA (or just Robinson arithmetic) whose formulas can be recursively (computably) enumerated.

Lemma

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).2

Theorem

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

Proof

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 want to show [s]=[sR][s] = [s \cdot R]. 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.

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 03.

Incompleteness

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). The following result applies in fact to any theory like PA that extends basic Robinson arithmetic and whose axioms form a recursive set.

Lemma

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).

Theorem

(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.

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], which is guaranteed to exist by theorem 1. The equality here is logical equivalence, and [sR]=code(s) *(¬Prov)[s \cdot R] = code(s)^\ast (\neg Prov) by equation (1).

References

  • William Lawvere, Diagonal Arguments and Cartesian Closed Categories, Lecture Notes in Mathematics, 92 (1969), 134-145 (TAC)

  • Yuri Manin, Georg Cantor and his heritage, arXiv:math/0209244

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

A brief review discussion explicitly in the context of type theory/topos theory is in

A formal proof of the Gödel-Rosser incompleteness theorem in Coq is given in

Formal proof of the second incompoletenss theorem is discussed in

  • Lawrence Paulson, A Mechanised Proof of Gödel’s Incompleteness Theorems using Nominal Isabelle (pdf)

The following contains a careful discussion of the incompleteness theorem in the context of categorical foundations using the free topos:

  • Jim Lambek, Phil Scott, Reflections on Categorical Foundations of Mathematics , pp.171-185 in Sommaruga (ed.), Foundational Theories of Classical and Constructive Mathematics, Springer New York 2011. (draft)

A bref survol technique of Gödel’s theorem within the landscape of Hilbert's program can be found in the first chapters of

See also the discussion in list-arithmetic pretoposes

  • Maria Maietti, Joyal’s arithmetic universe as list-arithmetic pretopos, Theory and Applications of Categories, Vol. 24, 2010, No. 3, pp 39-83. (TAC)


  1. Assuming that the theory is consistent. If the theory is inconsistent, then it can prove falsity and thence anything, including any internal statements of consistency.

  2. 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 July 8, 2017 09:02:28 by Urs Schreiber (188.100.200.251)