A 2-Categorical Bridge Between Henkin Constructions and Lawvere's Fixed-Point Theorem: Unifying Completeness and Compactness
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908367467839488 |
|---|---|
| author | Reizi, Barreto Joaquim |
| author_facet | Reizi, Barreto Joaquim |
| contents | We present a unified categorical framework that connects the syntactic Henkin construction for the first-order Completeness Theorem with Lawvere's Fixed-Point Theorem. Concretely, we define two canonical functors from the category of first-order theories to the category of their models, and then introduce a canonical natural transformation that links the Henkin-based term models to semantically constructed models arising from compactness or saturation arguments. We prove that every component of this natural transformation is an isomorphism, thereby establishing a strong equivalence between the syntactic and semantic perspectives. Furthermore, we show that this transformation is 2-categorically rigid: any other natural transformation in the same setting is uniquely isomorphic to it. Our framework highlights the shared diagonalization principle underlying both Henkin's and Lawvere's methods and demonstrates concrete applications in automated theorem proving, formal verification, and the design of advanced type-theoretic systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_03797 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A 2-Categorical Bridge Between Henkin Constructions and Lawvere's Fixed-Point Theorem: Unifying Completeness and Compactness Reizi, Barreto Joaquim General Mathematics We present a unified categorical framework that connects the syntactic Henkin construction for the first-order Completeness Theorem with Lawvere's Fixed-Point Theorem. Concretely, we define two canonical functors from the category of first-order theories to the category of their models, and then introduce a canonical natural transformation that links the Henkin-based term models to semantically constructed models arising from compactness or saturation arguments. We prove that every component of this natural transformation is an isomorphism, thereby establishing a strong equivalence between the syntactic and semantic perspectives. Furthermore, we show that this transformation is 2-categorically rigid: any other natural transformation in the same setting is uniquely isomorphic to it. Our framework highlights the shared diagonalization principle underlying both Henkin's and Lawvere's methods and demonstrates concrete applications in automated theorem proving, formal verification, and the design of advanced type-theoretic systems. |
| title | A 2-Categorical Bridge Between Henkin Constructions and Lawvere's Fixed-Point Theorem: Unifying Completeness and Compactness |
| topic | General Mathematics |
| url | https://arxiv.org/abs/2504.03797 |