6
$\begingroup$

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

  1. 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?

$\endgroup$
7
  • 1
    $\begingroup$ The first question has been discussed in my answer at mathoverflow.net/questions/424374/… . The initial arithmetic universe is the pretopos completion of the syntactic category of PRA. For the second question, note that the construction of L is that of the global section functor, while R just sends a formula to its internalization (its Gödel code), so L(x) is saying that x codes a provable formula, since the externalization can also be thought of as a syntactic category (a quotient of the initial AU). $\endgroup$
    – godelian
    Jul 3, 2022 at 19:50
  • 1
    $\begingroup$ (By the way I sent the email to FOM). $\endgroup$
    – godelian
    Jul 3, 2022 at 19:50
  • $\begingroup$ @godelian Yes on point one I know, but my first question is not exactly the same. Rather, can I further complete AU-0 so that it extend to a set-model of PRA? $\endgroup$ Jul 3, 2022 at 19:52
  • $\begingroup$ as for your second one, R is clear, L not so clear to me. I undestand its definition, but not what it represent from the logical standpoint. Is it true that GAU is a box algebra? $\endgroup$ Jul 3, 2022 at 19:55
  • 1
    $\begingroup$ I have now posted an answer. $\endgroup$
    – godelian
    Jul 3, 2022 at 21:51

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ bravo! crystal clear. More MO questions on AU to come..... $\endgroup$ Jul 3, 2022 at 22:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.