# Has Goedel's Second Incompleteness Theorem been proven using Lawvere's Fixed Point Theorem?

This question is a request for assistance in surveying the existing literature on applications of Lawvere's Fixed Point Theorem (LFPT).

Yanofsky [0] has demonstrated several applications of LFPT to prove various limitative results, in particular Goedel's First Incompleteness Theorem, and alludes to its applicability for proofs of the Second Incompleteness Theorem:

Goedel’s second incompleteness theorem about the unprovability within arithmetic of the consistency of arithmetic. This theorem is a simple consequence of the first incompleteness theorem. However Kreisal has a direct model theoretic proofs that uses a diagonal method (see, e.g., page 860 of Smorynski’s article in [1].) This proof seems amenable to our scheme.

Has there been any work conducted to further this vein of inquiry? Can the LFPT be used to prove Goedel's Second Incompleteness Theorem?

[1] Handbook of mathematical logic. North-Holland Publishing Co., Amsterdam, 1977. Edited by Jon Barwise, With the cooperation of H. J. Keisler, K. Kunen, Y. N. Moschovakis and A. S. Troelstra, Studies in Logic and the Foundations of Mathematics, Vol. 90.

• Joyal has provided a proof of both the first and second incompleteness theorems which is a categorical version entirely analogous to Gödel's original proof. The proof has been made available at arxiv.org/abs/2004.10482 Commented Jun 9, 2022 at 21:07
• "We have the following lemma, the AU-incarnation of the diagonalization lemma. It is reminiscent of Lawvere’s fixed point theorem." - @godelian, thank you very much, this looks promising. I had read about Joyal's work on arithmetic categories here [0], and Maria Maietti's modernization of them, but did not know if they had yet been used to categorify Goedel's 2nd Incompleteness Theorem. - [0] "Categorical folklore": mathoverflow.net/questions/126513/…
– jpt4
Commented Jun 10, 2022 at 0:56
• Should you wish to convert your comment into an answer, I would mark this question resolved.
– jpt4
Commented Jun 10, 2022 at 1:00

Both Gödel's first and second incompleteness theorems have been proven by André Joyal mimicking the arithmetization of metamathematics in Gödel's original proof with internal reasoning inside the initial arithmetic universe. This latter is none other than (the pretopos completion of) the syntactic category, in coherent logic, of the sequents expressing the axioms of primitive recursive arithmetic ($$PRA$$); in particular the type theoretic treatment of arithmetic universes is not really needed in the proof. Joyal gives an alternative construction of the initial arithmetic universe by defining the category of primitive recursive predicates, which corresponds to taking a different site of definition of the classifying topos (Coste's construction).
The proof has been very recently made available on arxiv in the paper of van Dijk/Oldenziel, although it's been part of categorical folklore since the seventies. Once an internal initial arithmetic universe has been shown to exist inside the initial arithmetic universe, its externalization provides the Gödel numbering of formulas, and one can define functorially the provability predicate $$Prov(x)$$. Then the proof of the incompleteness theorems proceeds by building a self-referential sentence similar to Gödel's sentence "I am not provable", exactly as Gödel did, using that this sentence is the fixed point of $$\neg Prov(x)$$, and an argument essentially equivalent to applying Lawvere's fixed point theorem provides its construction. The sentence is however slightly changed to "I am provably false" (which I call Joyal's sentence, the fixed point of $$Prov(\neg x)$$). It is well known that a fixed point for $$\neg Prov(x)$$ is equivalent to $$\neg Prov(\bot)$$, i.e., to $$Con(PRA)$$, and similarly Joyal also proves categorically that Joyal's sentence is equivalent to $$Incon(PRA)$$.
The second incompleteness then follows from the observation that Joyal's sentence cannot be provably false (though for certain consistent but $$\omega$$-inconsistent recursive extensions of PRA it can very well be provably true; here's what goes wrong with the conclusion of the cited paper).
• @ouimerci There's nothing wrong with the proof of the second incompleteness theorem, rather just that the extra hypothesis of $\omega$-consistency has to be added to the first incompleteness theorem instead of mere consistency to derive the undecidability of Joyal's/Gödel's sentence, as expected (this is also done in Gödel's original proof). In any case this is a feature of the presentation in the cited paper but not of Joyal's proof, which is certainly correct. Commented Jun 10, 2022 at 18:27