Technology
G\"odel coding on fibrations and geminal categories
Key Points
Announce Type: cross Abstract: Ramesh's 2023 dissertation introduces the categorical notions of introspective theories and geminal categories, which formalize "self-internalizing" structures sharing the form of L\"ob'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\"odel coding. This framework leads to a significant...
arXiv:2606.01165v1 Announce Type: cross
Abstract: Ramesh's 2023 dissertation introduces the categorical notions of introspective theories and geminal categories, which formalize "self-internalizing" structures sharing the form of L\"ob'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\"odel coding. This framework leads to a significant simplification of the proof of L\"ob's theorem for geminal categories, as well as to a new categorical counterpart of the G\"odel-L\"ob axiom ($\Box(\Box A \to A) \to \Box A$). This formulation offers an accessible framework for Ramesh's approach and suggests connections to modal type theories, where similar meta- and object-level interactions arise.