完备性与紧性定理模型构造之间的自然同态

我们建立了一个范畴论框架，将一阶逻辑中两种典范模型构造——Henkin构造与基于超积或饱和的紧性构造——联系起来。通过引入一组全局固定的Henkin见证常量，我们定义了从一致一阶理论范畴到具有初等嵌入的模型范畴的两个函子。第一个函子将每个理论映射为其在扩展语言中的Henkin项模型，第二个函子将见证常量生成的Skolem闭包映射到固定的超积或饱和模型中。我们构造了一个自然变换，使得每个分量都是对应模型之间的同构。关键洞察在于，两种构造利用了相同的全局Henkin扩张方案，确保了函子性，并使得典范解释映射到Skolem闭包上是满射。我们阐明，若不加Skolem闭包限制，该映射仅为初等嵌入而非同构，因为任意饱和模型可能包含项模型值域之外的非标准元素。对于特殊理论类，包括阿列夫零范畴理论和原子完备理论，由于其可数模型的唯一性，该构造得以简化。我们还纠正了关于自然变换刚性的先前论断，指出Henkin常量的均匀置换可产生非平凡的自然自同构。本工作为理解一阶逻辑中语法证明论与语义模型论方法之间的关系提供了结构洞察，在自动定理证明和形式验证方面具有潜在应用。