2 范畴桥梁：连接 Henkin 构造与 Lawvere 固定点定理：统一完备性与紧致性
综合数学
2025-05-19 v1
摘要
我们提出了一个统一的范畴框架，将一阶完备定理中的语法 Henkin 构造与 Lawvere 固定点定理相连接。具体而言，我们定义了从一阶理论范畴到其模型范畴的两个标准函子，并引入一个将 Henkin 基于的项模型与紧致性或饱和性论证中构建的语义模型相联系的标准自然变换。我们证明了该自然变换的每个组成部分都是同构，从而在语法视角与语义视角之间建立了强等价。进一步，我们展示了该变换在 2 范畴层面上具有刚性：该设置下的任何其他自然变换都唯一同构于它。我们的框架突出了 Henkin 方法与 Lawvere 方法所基于的共享对角化原则，并在自动定理证明、形式化验证以及高级类型论系统设计方面 demonstrate了具体应用。
引用
@article{arxiv.2504.03797,
title = {A 2-Categorical Bridge Between Henkin Constructions and Lawvere's Fixed-Point Theorem: Unifying Completeness and Compactness},
author = {Barreto Joaquim Reizi},
journal= {arXiv preprint arXiv:2504.03797},
year = {2025}
}
备注
28pages