Abstract
We establish a categorical framework relating two canonical model constructions in first-order logic: the Henkin construction and compactness-based constructions via ultraproducts or saturation. By introducing a globally fixed set of Henkin witness constants, we define two functors from the category of consistent first-order theories to the category of models with elementary embeddings. The first functor assigns to each theory its Henkin term model in an expanded language, while the second assigns the Skolem closure generated by the witness constants within a fixed ultraproduct or saturated model. We construct a natural transformation such that each component is an isomorphism between the corresponding models. The key insight is that both constructions utilize the same global Henkin expansion scheme, ensuring functoriality and allowing the canonical interpretation map to be surjective onto the Skolem closure. We clarify that without the Skolem closure restriction, the map would only be an elementary embedding rather than an isomorphism, as an arbitrary saturated model may contain non-standard elements outside the range of the term model. For special classes of theories, including aleph-zero-categorical theories and atomic complete theories, the construction simplifies due to uniqueness properties of their countable models. We also correct previous claims regarding rigidity of natural transformations, noting that uniform permutations of Henkin constants yield non-trivial natural automorphisms. This work provides structural insight into the relationship between syntactic proof-theoretic and semantic model-theoretic approaches to first-order logic, with potential applications in automated theorem proving and formal verification.
本页仅发布可检索的书目信息与作者摘要。HTML 正文、PDF 和 LaTeX 源文件是独立阅读资源，不作为搜索引擎落地内容。打开页面后会按浏览器语言自动翻译标题与摘要，并写入缓存。