海廷代数上的辩证范畴
Dialectica Categories over Heyting Algebras
浏览论文内容
中文总结 AI 辅助
研究海廷代数上的辩证范畴，通过对德·派瓦对哥德尔辩证解释范畴化中偏序特化的研究，在代数环境重现证明并获特定结果，如嵌入伴随性变化、张量在不同构造中的表现及反射坍缩与选择公理的关系。
中文摘要 AI 辅助
范畴化，即构建数学部分的范畴模型的过程，常常能识别出一种连接先前不相关但已知结构的共同抽象。在德·派瓦对哥德尔辩证解释的范畴化中，我们发现其对偏序的特化产生了海廷代数到剩余格的（函子性）嵌入，而这似乎被忽视了。对于非范畴论的读者，我们展示了这种特化，并在代数环境中仔细重现了原始证明。在此过程中，我们得到了特定于该代数环境的结果：在德·派瓦的一般构造中缺乏明显伴随的嵌入在此处获得了可定义的伴随；单个辩证张量在直觉主义构造 D 中验证收缩，但在经典变体 G 中反驳它；并且，在 ZF 上，偏序集反射 PD(Set) 恰好当选择公理成立时坍缩到四元代数 PD(2)。
英文摘要
Categorification---the process of constructing a categorical model of a piece of mathematics---often identifies a common abstraction that connects formerly unrelated but known structures. In the case of de Paiva's categorification of Gödel's Dialectica interpretation, we find that its specialization to partial orders produces (functorial) embeddings of Heyting algebras into residuated lattices that appear to have been overlooked. For the non-categorical audience, we present this specialization and take care to reproduce the original proofs in the algebraic setting. Along the way we obtain results particular to this algebraic setting: an embedding lacking an evident adjoint in de Paiva's general construction acquires a definable one here; a single Dialectica tensor validates contraction in the intuitionistic construction D yet refutes it in the classical variant G; and, over ZF, the poset reflection PD(Set) collapses onto the four-element algebra PD(2) exactly when the Axiom of Choice holds.
