A Natural Homomorphism between the Model Constructions of the Completeness and Compactness Theorems

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.