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?