Ramesh's 2023 dissertation introduces the categorical notions of 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, as well as to 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 approach and suggests connections to modal type theories, where similar meta- and object-level interactions arise.
翻译:Ramesh 2023年的学位论文引入了内省理论与对偶范畴的范畴论概念,形式化了具备勒布定理形式($\Box A \vdash A$ 蕴含 $\vdash A$)的"自内化"结构。我们通过引入"纤维化上的编码结构"——作为哥德尔编码的范畴论抽象——以自洽的方式重组了对偶范畴理论。该框架不仅显著简化了对偶范畴中勒布定理的证明,还提出了哥德尔-勒布公理($\Box(\Box A \to A) \to \Box A$)的新范畴论对应。这一表述为Ramesh方法提供了可理解的框架,并揭示了与模态类型理论(其中类似元级与对象级交互关系自然涌现)的关联。