Deciding Amalgamation Beyond Arity Two: The Semantic Horn Case

Abstract

We study the amalgamation decision problem (ADP): given a universal first-order sentence Φ, decide whether the class fm(Φ) of its finite models has the amalgamation property. We call Φ semantic Horn if fm(Φ) is closed under binary direct products. By McKinsey's theorem, this is equivalent to Φ being logically equivalent to a universal Horn sentence. The distinction concerns the input representation: Φ itself need not be given in Horn form, and converting it into an explicit Horn normal form can incur an exponential blow-up. We prove that the ADP is decidable under this semantic promise. To this end, we associate with Φ a finite-domain CSP template, called its completion template, and a distinguished infinite family of CSP instances, called its atlas instances. The class fm(Φ) has the amalgamation property precisely when all atlas instances have a solution. For semantic Horn inputs, we prove that the completion template admits a semilattice polymorphism. Consequently, its CSP has bounded width and is decided by a fixed level of local consistency. We introduce uniform contextual strategies, finite certificates expressing this local-consistency condition simultaneously for all atlas instances, and give an effective fixed-point procedure for deciding whether such a certificate exists. The resulting algorithm runs in 2ExpTime in general and in ExpTime under any fixed bound on the arities of the input relations. More generally, the construction gives a decision procedure whenever the associated completion template has bounded width. These bounds are optimal: the semantic Horn ADP is 2ExpTime-complete in general and ExpTime-complete for every fixed arity bound of at least three. Both hardness results already hold for syntactic universal Horn sentences.

Bergman's amalgamation problem over the circle
Andreas Thom
arXiv24 Sep 2026PreprintCC BY 4.0Full textAlgebra & number theoryarXiv
High-Arity Rademacher Complexity and Uniform Laws of Large Numbers
Aaron Anderson, Henry Towsner
arXiv13 Oct 2026PreprintarXiv licenceFull textCombinatorics & discrete mathematics Logic & foundationsarXiv
Degree and arity of tracial separation for self-adjoint contractions
Jie Wang
arXiv2 Nov 2026PreprintCC BY 4.0Full textAnalysis & PDEsarXiv
Mutation Sequences along Weaves and Amalgamation of Braid Varieties
Yuma Mizuno
arXiv5 Sep 2026PreprintarXiv licenceFull textAlgebra & number theory Geometry & topologyarXiv
A degree-linear upper bound for the Pólya exponent of forms with fixed arity
Yulong Li, Colin Tan
arXiv10 Oct 2026PreprintCC BY-NC-SA 4.0Full textAlgebra & number theoryarXiv

Cite

BibTeX RIS

BibTeX

@misc{rydval2026deciding,
  title = {{Deciding Amalgamation Beyond Arity Two: The Semantic Horn Case}},
  author = {Jakub Rydval},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2608.12206},
  eprint = {2608.12206},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2608.12206},
}

RIS

TY  - UNPB
TI  - Deciding Amalgamation Beyond Arity Two: The Semantic Horn Case
AU  - Jakub Rydval
PY  - 2026
DA  - 2026/09/13
PB  - arXiv
DO  - 10.48550/arxiv.2608.12206
UR  - https://arxiv.org/abs/2608.12206
AB  - We study the amalgamation decision problem (ADP): given a universal first-order sentence Φ, decide whether the class fm(Φ) of its finite models has the amalgamation property. We call Φ semantic Horn if fm(Φ) is closed under binary direct products. By McKinsey's theorem, this is equivalent to Φ being logically equivalent to a universal Horn sentence. The distinction concerns the input representation: Φ itself need not be given in Horn form, and converting it into an explicit Horn normal form can incur an exponential blow-up. We prove that the ADP is decidable under this semantic promise. To this end, we associate with Φ a finite-domain CSP template, called its completion template, and a distinguished infinite family of CSP instances, called its atlas instances. The class fm(Φ) has the amalgamation property precisely when all atlas instances have a solution. For semantic Horn inputs, we prove that the completion template admits a semilattice polymorphism. Consequently, its CSP has bounded width and is decided by a fixed level of local consistency. We introduce uniform contextual strategies, finite certificates expressing this local-consistency condition simultaneously for all atlas instances, and give an effective fixed-point procedure for deciding whether such a certificate exists. The resulting algorithm runs in 2ExpTime in general and in ExpTime under any fixed bound on the arities of the input relations. More generally, the construction gives a decision procedure whenever the associated completion template has bounded width. These bounds are optimal: the semantic Horn ADP is 2ExpTime-complete in general and ExpTime-complete for every fixed arity bound of at least three. Both hardness results already hold for syntactic universal Horn sentences.
ER  -

Abstract

Related

Cite