A function $f : M \to N$ preserves and reflects a formula $\phi$ if $M \models \phi(\overline a) \iff N \models \phi(f(\overline a))$. For many fragments of first-order logic, there is a clear relationships between functions and the formulas they preserve and reflect. If a function preserves and reflect all first-order formula, then it is elementary; if it preserves quantifier-free formulas, then it is an embedding; functions preserving and reflecting existential formulas don't seem to have a name, but they are important in the study of existential closure.
My question is: what maps preserve and reflect basic Horn formulas (a.k.a. quantifier-free Horn formulas)? It should have been studied before, but I could not find any reference. Such maps appear to be algebraically related to direct products, but projections from direct products preserve and reflect p.p. formulas.
Any reference or thoughts would be welcome.
First of all, to clarify terminology, a basic Horn formula (or Horn clause) has the form $$\left(\bigwedge_{i<n}\varphi_i(x)\right)\to \psi(x)$$ where $n\geq 0$, each $\varphi_i$ is atomic, and $\psi$ is atomic or $\bot$. A Horn clause is strict if $\psi$ is not $\bot$. I tend to think that strict Horn clause is the more natural notion, but that's neither here nor there.
In particular, any atomic formula $\psi(x)$ is equivalent to a strict Horn clause (taking $n=0$ in the definition), and any negated atomic formula $\lnot \varphi(x)$ is equivalent to a (non-strict) Horn clause (taking $n=1$ and $\psi=\bot$ in the definition).
Now if a homomorphism preserves Horn clauses, it preserves negated atomic formulas, so it's an embedding, so it preserves and reflects all quantifier-free formulas, in particular all Horn clauses. Similarly, if a homomorphism reflects Horn clauses, then it reflects atomic formulas, so again it's an embedding, and it preserves and reflects all Horn clauses.
Thus the following conditions are all equivalent: (a) $f$ preserves Horn clauses, (b) $f$ reflects Horn clauses, (c) $f$ preserves and reflects Horn clauses, and (d) $f$ is an embedding.
What about strict Horn clauses? Since atomic formulas are strict Horn clauses, any homomorphism which reflects (or preserves and reflects) strict Horn clauses is again an embedding.
The situation is slightly more interesting for homomorphisms which preserve strict Horn clauses. Recall that the terminal $L$-structure is the one-point structure where all function and constant symbols are constant with value the unique element, and all relation symbols are true of the unique tuple of the appropriate length. Equivalently, the terminal $L$-structure is the unique $L$-structure (up to isomorphism) with the property that every atomic formula holds on every tuple.
Say a homomorphism is a zero map if it factors through the unique homomorphism to the terminal $L$-structure.
I claim that a homomorphism preserves Horn clauses if and only if it is an embedding or a zero map.
It is easy to see that embeddings and zero maps preserve strict Horn clauses. Conversely, assume $f\colon A\to B$ preserves strict Horn clauses, and assume it is not an embedding. We will show it is a zero map.
Since $f$ is not an embedding, there is some atomic formula $\varphi(x)$ and some tuple $a$ from $A^x$ such that $A\not\models \varphi(a)$ and $B \models\varphi(f(a))$.
Let $\psi(y)$ be any other atomic formula, and let $a'$ be any tuple from $A^y$. Consider the strict Horn clause $\varphi(x)\to \psi(y)$. We have $A\models \varphi(a)\to \psi(a')$, since $A\not\models\varphi(a)$. Since $f$ preserves strict Horn clauses, $B\models \varphi(f(a))\to\psi(f(a'))$. And since $B\models\varphi(f(a))$, it follows that $B\models\psi(f(a'))$. Since $\psi$ and $a'$ were arbitrary, we conclude that every atomic formula is true of every tuple in $\mathrm{im}(f)$. So $f$ is a zero map.