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 $\mathrm{fm}(Φ)$ of its finite models has the amalgamation property. We call $Φ$ semantic Horn if $\mathrm{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 $\mathrm{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.