Finite entailment of Positive Horn logic

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Fix a finite relational vocabulary with equality. A positive Horn sentence is built from atomic relation formulas and equalities using only conjunction and existential and universal quantification. Structures have nonempty domains; no function symbols or negations inside these sentences are assumed. Write $\phi\models\psi$ for entailment in all structures and $\phi\models_{\mathrm{fin}}\psi$ for entailment in all finite structures.

Statement recorded in the supplied source.

For every pair of positive Horn sentences $\phi,\psi$, if some structure satisfies $\phi\wedge\neg\psi$, must some finite structure satisfy it? Equivalently, does $\phi\models_{\mathrm{fin}}\psi$ imply $\phi\models\psi$? The accompanying decision question asks whether an algorithm, given $\phi,\psi$, decides $\phi\models_{\mathrm{fin}}\psi$. [S2]

Short English statement

Does every counterexample to entailment between positive Horn sentences have a finite counterexample, and is finite entailment decidable?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 3342 (OPG-37863). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Open Problem Garden, Finite entailment of Positive Horn logic, node 37863, original problem page. Original question and full discussion. https://www.openproblemgarden.org/op/finite_satisfiability_of_positive_horn_logic_entailment.