Categorical structures for Gödel incompleteness and Löb’s theorem

In provability logic, a key principle is Löb’s theorem, stating that if the provability of $P$ provably entails $P$, then $P$ itself is provable (in modal logic notation, $\mathrm{\square }P⊢P$ has as a consequence $⊢P$). This was first discovered in the follow-up work on Gödel’s incompleteness theorems, with Gödel’s results viewable as a special case of Löb’s theorem. This same formal pattern of Löb’s theorem was later observed to also arise in several other seemingly unrelated contexts. For example, the formal pattern of Löb’s theorem is also of note in modal logic as corresponding to well-founded transitive Kripke frames. And the formal pattern of Löb’s theorem also describes certain fixed point constructions studied under the name of “guarded recursion” in programming language theory.

In the author’s dissertation [4], currently being prepared for publication, it is observed that a particularly simple class of category-theoretic structures serve as an abstract environment for deriving Löb’s theorem and its associated fixed point constructions, allowing for a vastly generalized and unified understanding of the scope of applicability of these, including all of the above contexts. These are the structures we call “introspective theories”.

Specifically, we define an “introspective theory” to be a category with finite limits $T$ with an internal category with finite limits $C$, along with a natural transformation from the self-indexing of $T$ to $C$ (construed as contravariant functors from $T$ to the category of categories with finite limits).

Remarkably, this simple structure is in itself enough to derive Löb’s theorem, as well as guarded recursion at both the term and type level. We also demonstrate how this abstraction offers a clean unification of the interpretation of the Gödel-Löb incompleteness theorems in traditional logic or via arithmetic universes a la Joyal (as in [2]), along with the interpretation by Birkedal et al of guarded recursion in presheaves over well-founded orders (as in [1]), along with the distinct classical interpretation of the GL modal logic in well-founded transitive Kripke frames.

This significantly extends the connection between Gödel’s incompleteness theorem and category theory observed by Lawvere in [3], by now giving a category-theoretic account of the the Gödel coding process itself. As this account is not tied to the specific context of natural number arithmetic, it also allows us to furthermore observe uncountable and uncomputable structures in which the Gödel incompleteness phenomena still arise.

We also explore free instances of our structure, which turn out to admit a tractable explicit description. The free introspective theory is called in the author’s dissertation “the theory of geminal categories”, and there are a number of further illuminating relationships discovered between introspective theories and geminal categories.