Gödel coding on fibrations and geminal categories

Abstract

Recently, Ramesh has introduced new categorical concepts, introspective theories and geminal categories, which formalize “self-internalizing” structures sharing the form of Löb’s theorem ($\Box A \vdash A$ implies $\vdash A$). We reorganize the theory of geminal categories in a self-contained manner by introducing “code structures on fibrations,” which serve as a categorical abstraction of Gödel coding. This framework leads to a significant simplification of the proof of Löb’s theorem for geminal categories and also a new categorical counterpart of the Gödel–Löb axiom ($\Box(\Box A \to A) \to \Box A$). This formulation offers an accessible framework for Ramesh’s ideas, providing a promising perspective to unify meta- and object-level interactions in logic and computer science.