Last month @godelian, alias Christian Espíndola, in a FOM post has mentioned Joyal's proof of Godel's second incompleteness via the so-called Arithmetic Universes, introduced by Joyal around 1973, and further investigated by Vickers, Maietti and Taylor.
After perusing the relatively sparse literature on them, I decided that the last reference
was the only one I could use as an entry door. Though the article makes a substantial effort to be self-contained, it is still to me a bit of a hard reading, especially in building the right intuition (though some great help comes from Taylor's answer here: Categories of recursive functions and by Godelian Has Goedel's Second Incompleteness Theorem been proven using Lawvere's Fixed Point Theorem? )
What I understand so far:
1 Joyal introduces Arithmetic Universes, ie pretopoi ( finite limits, effective quotients of equivalence
relations ) plus an axiom which essentially says: if you have an object A you also have
a list object LIST[A] which is to be intended as lists of elements of A (actually, LIST[-] is an endofunctor)
.
Note: an AU is in general NOT
an elementary topos, though of course all topoi with a natural number object NNO are trivially AUs. Topoi are universes of constructive set theory, they have too much (functions spaces, power object, all things that are indispensable for higher order logic, but not here).
First key point: one can inhabit an AU, and from its vantage point there is an internal typed language (developed by Maietti)
that makes it "roomy enough" to talk about primitive recursive functions, decidable predicates, etc. In other words, arithmetic universes are indeed universes of discourse which are paired with Primitive Recursive Arithmetics (PRA). It goes without saying that there is a 2-category of AUs, let us call it AUS. The functors between them preserve the AU structure.
FIRST QUESTION: who are these AUs? if I take any ordinary model of PRA, the category of
all definable functions, predicates, and whatnot of M is an AU. But, is it true that all AUS come from that? In other words, is there a canonical way to complete/embed an AU to a set-based model of PRA?
2 the theory of the AUS is essentially algebraic, so there is a distinguished
initial object in AUS, let us call it AU-0. AU-0 is the freest AU of the multiverse AUS*
3 Fact : AU-0 has an internal category, let us call it $au_0$, which is ITSELF a AU
(in the internal sense).
$au_0$ is quite intriguing: in a sense, it measures the degree of self-reflection of AU-0, ie how much AU-0 can code of itself. Moreover, as AU-0 is initial in AUS, ALL AUs have their own little au.
The construction of $au_0$ from AU-0 leverages a number of things included the infamous list object above (see reference) .
- Now we get to the real "main course", and also to the haziest area to me:
category theorists love internal cats, and have a technique called EXTERNALIZATION,
by which they can externalize internal cats. So, let us externalize little au-0:
$$
AUG = EXT(au_0).
$$
AUG is a REAL object of the arithmetic multiverse, and therefore we can compare it with
AU-0.
The fundamental piece of magic is that by looking at the interplay between AU-G and AU-0
we can get Godel 1 and 2. How? Let me point out one thing:
AU-0 is INITIAL in AUS, so there is an AU functor R FROM AU-0 TO AU-G:
$$R\colon AU\text{-}0 \rightarrow AUG $$
There is something else, 'going
the other way around:
$$L\colon AUG \rightarrow AU\text{-}0 $$
Whereas T is an AU-functor, L is not. Nevertheless we can define $\Box= LR$ which is (correct me if I am wrong ) a monad on AU-0.
Now, the magic: $\Box$ is Joyal's categorical version of the famous Provability Operator in Provability Logic! It satisfies Lob's condition and can be used to do exactly what the provability operator does in algebraic logic, for instance G 1 and G2.
SECOND QUESTION: to me this last steps still sounds like magic: what is the proper way to think of the externalized GAU? If indeed the Box is monadic, what is its category of algebras?
Best Answer
As discussed in the comments, the AU's are all models of the initial one, which is equivalent to the pretopos completion of the syntactic category of PRA (in coherent logic). In particular a set model of PRA cannot be made initial because it could collapse two different arrows in the initial AU (i.e., there could be two primitive recursive functions that are extensionally equal but whose recursive definitions are different).
The externalization of the internal initial AU is precisely the Gödel numbering on each formula. More explicitly, each object of the externalization is an arrow $1 \to O$ where $O$ is the object of "objects" of the internal arithmetic universe, so it is an arrow from the terminal object to something that is a quotient by an equivalence relation of a certain primitive recursive predicate (i.e., a decidable subset of $\mathbb{N}$), and all the numbers in the chosen equivalence class are the Gödel codes of the corresponding formula (there are several depending on which coding we use).
Now the global section functor from the externalization to the initial AU is the object that represents the hom set $[1, -]$, and since the externalization is also a syntactic category, having an arrow from $1$ is equivalent to being provable. So this functor is indeed the correct way to code the provability of the formulas represented by Gödel numbers.
But $R$ and $L$ are not adjoints, so we cannot speak of the corresponding monad, for otherwise $L$ would have to be the right adjoint. To see that this is impossible, note that the construction of Joyal sentence $J$ (the self-referential sentence "I am provably false") is proven to be equivalent to $Incon(PRA)$. By construction, the application of the functor $R$ gives us the corresponding Joyal sentence $R(J)$ of the externalization, which is never $0$ if the externalization is consistent (this is Gödel's second incompleteness theorem). So, if $L$ and $R$ were an adjoint pair, we would have in particular that $[J, L(0)] \cong [R(J), 0]$. But $[R(J), 0]$ is empty when the externalization is consistent, while $[J, L(0)] \cong [J, \square \bot] \cong [J, J]$ which is nonempty.