A Natural Homomorphism between the Model Constructions of the Completeness and Compactness Theorems
Barreto Joaquim Reizi
TL;DR
This work builds a categorical bridge between the Henkin completeness construction and compactness-based constructions by structuring them as functors $F,G:\mathbf{th}\to\mathbf{mod}$ and establishing a natural transformation $\eta: F\to G$ whose components are isomorphisms when $G(t)$ is restricted to the Skolem closure within a canonical ultraproduct or saturation model. By fixing a global Henkin expansion, the authors show that these two canonical procedures yield models canonically isomorphic in a functorial sense, clarifying that surjectivity requires Skolem-closure restriction while general cases may only yield elementary embeddings. The framework also identifies simplifications for $\aleph_0$-categorical or atomic complete theories and corrects prior claims about rigidity of natural transformations, highlighting a richer automorphism structure under uniform Henkin-witness permutations. Potential applications include automated theorem proving and formal verification, with avenues for extending the approach to non-classical logics and further 2-categorical coherence questions.
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.