Gödel coding on fibrations and geminal categories

@mastersthesis{ikeda2026,
  author      = {Ikeda, Yuto},
  title       = {{G{\"o}del} coding on fibrations and geminal categories},
  school      = {University of Tokyo},
  address     = {Tokyo, Japan},
  year        = {2026},
  month       = feb,
  type        = {Master's thesis},
  url         = {https://ikeda.ac/pubs/ikeda2026/}
}

Abstract

In their 2023 dissertation, Ramesh has proposed two categorical notions, introspective theories and geminal categories, to unify various structures sharing the form of Löb’s theorem: $\Box A \vdash A$ implies $\vdash A$. These include classical logical systems, Joyal’s arithmetic universes, Kripke semantics for the provability logic $\mathsf{GL}$, and categorical models for guarded recursion. The remarkable feature of Ramesh’s approach is that it does not impose Löb’s theorem as a definition; instead, it directly formalizes the “self-internalizing” nature, such as the formalization of a theory within itself as seen in the proof of the incompleteness theorems. Indeed, Ramesh demonstrates that Löb’s theorem can be derived from these structures through highly non-trivial arguments.

In this thesis, we provide a mathematical and conceptual reorganization of the theory of geminal categories in a self-contained manner. As a consequence, we establish a novel categorical counterpart of the Gödel–Löb axiom $\Box(\Box A \to A) \to \Box A$ for any geminal category. We also provide a significant simplification of the proof of Löb’s theorem for geminal categories, along with a slight generalization of the result.

To achieve such an organization, we introduce the notion of code structures on fibrations, which serves as a natural abstraction of Gödel coding, and establish the fixed point theorem for them, generalizing the classical diagonal lemma. This result acts as a universal theorem that unifies various classical results possessing intensional features. We then introduce pre-geminal categories, a slight weakening of geminal categories, as a natural structure that induces code structures on codomain fibrations. Löb’s theorem for pre-geminal categories is then derived from our fixed point theorem, which simplifies and highlights the core idea of Ramesh’s original proof. The notion of geminal categories and the Gödel–Löb axiom for them are realized by internalizing our arguments for pre-geminal categories, providing a new perspective on geminal categories via code structures. We also compare our framework with the structures appearing in modal calculi for metaprogramming.

Our formulation does not rely on the notion of introspective theories or any informal internal reasoning, making the theory of geminal categories more accessible to a broader audience. We propose that the framework of geminal categories offers a promising perspective for abstracting and unifying the interaction between meta- and object-levels arising in both logic and computer science.