Is there an equivalent of the incompleteness theorems/halting problem in category theory?

Question

Taking the doctrine of computational trinitarianism ( https://ncatlab.org/nlab/show/computational+trinitarianism ), if one understands the incompleteness theorems as the "logic" version, and the answer to the halting problem as the "language theory" version, is there a known expression of this "pair of abstract computational theorems" in category theory ? Or applied category theory ? Something along the lines of "there exists no category of all categories" or "there exists no generalized mathematical model encompassing all applied mathematical models" maybe ? (IIRC, Cat is only the category of locally small categories.)

Answer 1

There is a category theoretic version of the incompleteness theorem originally due to André Joyal that has been unavailable for a long time, but has been written up not so long ago by Joost van Dijk and Alexander Gietelink Oldenziel.

It is a much more technical statement than what you are looking for and it is very close to the original incompleteness theorem but phrased in a purely category theoretic language, so I think it is worth mentioning.

Very roughly, an "arithmetic universe" is a pretopos with list object. It is an essentially algebraic notion, so you can consider free arithmetic universe.

What is interesting with this notion is that arithmetic universe are the category theoretic structure that allows to construct "internally" free model for essentially algebraic theory (e.g., you can construct a Free monoid on an object of an arithmetic universe... this is exactly the list object).

These free algebraic structure are closely related to induction/recursion which is somehow the hearth of the traditional incompleteness theorem. In fact the free arithmetic universe admits a description in terms of primitive recursive functions, so this makes somehow very natural the use of recursion theory in the traditional proof of Gödel theorem. But in the category theoretic approach recursive functions can be completely hidden away.

So, in particular, you can consider a "free arithmetic universe object" inside an arithmetic universe.

I suggest to go read the paper linked above for a rigorous statement, but the idea of Gödel incompleteness in this language is that you consider the free arithemtic universe object T' internal to the free arithmetic universe T. That is T is a category (an arithmetic universe) and T' is a category object in T. Then T' it is not "provably consistent" in T in the sense that the sub-terminal object of T that parametrize equality between the two maps "0" and "1" of T' is non-trivial.