UC Berkeley

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, □ 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 following from Löb's theorem. Later, it was also seen that the same formal pattern of Löb's theorem described certain fixed point constructions studied under the name of "guarded recursion".

The aim of these notes is to draw attention to a certain simple class of category-theoretic structures which serve as an abstract environment for deriving Löb's theorem and such fixed point constructions, allowing for a vastly generalized and unified understanding of the scope of applicability of such constructions. These are the structures we call "introspective theories".

This very minimal categorical definition nontrivially entails Löb's theorem and 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, along with the interpretation by Birkedal et al of guarded recursion in presheaves over well-founded orders, along with the distinct classical interpretation of the GL modal logic in well-founded transitive Kripke frames.

We also explore free instances of our structure, which turn out to admit a tractable explicit description. The free introspective theory is what we call "the theory of geminal categories", and we explore also some further illuminating relationships between the concepts of introspective theories and geminal categories.