Deciding Amalgamation Beyond Arity Two: The Semantic Horn Case
We study the amalgamation decision problem: given a universal first-order sentence $\Phi$, decide whether the class $\mathrm{fm}(\Phi)$ of its finite models has the amalgamation property. We call $\Phi$ semantic Horn if $\mathrm{fm}(\Phi)$ is closed under binary direct products. By McKinsey's theorem, this is equivalent to $\Phi$ being logically equivalent to a universal Horn sentence; the distinction is one of input representation, since $\Phi$ itself need not be given in Horn form and conversion to an explicit Horn normal form can incur an exponential blow-up. We prove that the problem is decidable under this semantic promise. Moreover, it belongs to 2EXPTIME, and to EXPTIME for every fixed bound on the arity of the input signature. Thus the semantic Horn fragment admits an unconditional decision procedure for signatures of unbounded relational arity. Our proof starts from the inside-out correspondence, which we use as a black box for the semantic reduction to a finite completion problem. We encode finite completions as homomorphisms to a finite relational template and introduce a finite set-valued local-consistency certificate for completion problems whose template has bounded width. For semantic Horn inputs, the local completions over each fixed source chart are closed under relationwise intersection of the added relations, and these intersections are compatible with restriction maps. This yields a semilattice polymorphism of the completion template. Since the template is binary, the semilattice operation gives width $2$, making the local-consistency certificate complete. The same construction gives a decision procedure whenever the associated completion template has bounded width.