basic constructions:
strong axioms
further
(0,1)-category theory: logic, order theory
proset, partially ordered set (directed set, total order, linear order)
distributive lattice, completely distributive lattice, canonical extension
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit 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
</table>
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 $T$ 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 $T$. The second incompleteness theorem shows that for such theories $T$, the sentence can be taken to be a suitable arithmetization of the statement of consistency of $T$ 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 $p$ in the theory such that neither $p$ nor its negation $\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 true^{1} 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.
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 hom-set of morphisms $0 \to 1$ in $\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
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$,
which allows us to regard $T$ as a $\mathbf{PRA}$-module.
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
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,
and we define an application pairing $\cdot$ to be the composite along the top of the following commutative diagram:
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
which will be used in our diagonalization result.
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.
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)$.^{2}
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 \Leftrightarrow s \cdot R$ ($s$ is provably equivalent to $s \cdot R$).
Pick a formula $t \in \Phi(1)$ such that $[t] = d^\ast [R]$, and then put $s = t \cdot t$. We want to show $[s] = [s \cdot R]$. We have
as required.
The proof of theorem 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.
Recall there is also a Gödel coding of PA proofs (certain sequences of PA formulas), $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.
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)$.
(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.
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]$, which is guaranteed to exist by theorem . The equality here is logical equivalence, and $[s \cdot R] = code(s)^\ast (\neg Prov)$ by equation (1).
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
The following contains a careful discussion of the incompleteness theorem in the context of categorical foundations using the free topos:
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
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. ↩
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.” ↩
Last revised on July 8, 2017 at 09:02:28. See the history of this page for a list of all contributions to it.