= Solution
\b[The assertion is false as printed, even for a satisfiable equality-free <Horn clause>.] The original paper allows an arbitrary <quantifier-free formula> $G^*$, so in particular permits negative atoms.<Logic and Proof examination paper of the University of Oxford (2015)>[Printed p. 4, Question 3(d), final sentence: the matrix is specified as quantifier-free, without a positivity restriction]{ref}
Take a <first-order signature> with a constant $a$ and unary predicates $P,Q$, and let
$$
F=\forall x\,[\neg P(x)\lor Q(x)],
\qquad G=\exists x\,\neg P(x).
$$
The matrix of $F$ is a <Horn clause>, and the <Herbrand universe> is the singleton $\{a\}$. The possible <Herbrand models> of $F$ assign $(P(a),Q(a))$ the values $(0,0)$, $(0,1)$, or $(1,1)$. Neither ground atom is true in every such <Herbrand model>, so the paper's intersection construction gives
$$
P^{\mathcal H_F}=Q^{\mathcal H_F}=\varnothing.
$$
Consequently $\mathcal H_F\models G$, with witness $a$. However, the one-element <first-order structure> in which both predicates hold everywhere satisfies $F$ and falsifies $G$. Hence
$$
\boxed{\mathcal H_F\models G\quad\text{but}\quad F\not\models G.}
$$
This directly refutes the requested implication; no proof of the stated equivalence is possible. It also isolates the issue: an atom being absent from the intersection means that it is false in \i[some] <Herbrand model>, not that it is false in every <first-order model>.
The standard correct version assumes that $F$ is satisfiable, uses an equality-free <first-order signature> with a nonempty <Herbrand universe>, and requires $G^*$ to be a positive <quantifier-free formula>: one built from atoms and truth constants using only <logical conjunction> and <logical disjunction>. Under those assumptions the expected argument is as follows.
First, the intersection of the ground atoms true in all <Herbrand models> is itself a <Herbrand model> of $F$. To see this, read each ground <Horn clause> as $A_1\land\cdots\land A_k\to B$, where $B$ is an atom or false. If every $A_i$ is true in the intersection, every $A_i$ is true in every <Herbrand model>. When $B$ is an atom, all these <Herbrand models> must make $B$ true, so the intersection does too. When $B$ is false, the antecedent cannot hold in any <Herbrand model>; since there is at least one such model, it cannot hold in the intersection either. Thus the intersection is the <least Herbrand model>.
Now let $\mathcal H_F\models G$ for positive $G^*$. There is a tuple of <ground terms> $\bar t$ with $\mathcal H_F\models G^*(\bar t)$. Expand the positive <quantifier-free formula> into <disjunctive normal form>; one of its <logical conjunctions> of positive atoms is true at $\bar t$. Each of those ground atoms $A$ holds in every <Herbrand model> of $F$. It also follows that $F\models A$: otherwise a <first-order model> of $F\land\neg A$ would, by <Herbrand's theorem> for universal equality-free <first-order clauses>, yield a <Herbrand model> of $F\land\neg A$, a contradiction. Every <first-order model> of $F$ therefore satisfies the same positive <logical conjunction> at the interpretations of $\bar t$, and hence satisfies $G$.
Conversely, if $F\models G$, the fact that the <least Herbrand model> is a <first-order model> of $F$ immediately gives $\mathcal H_F\models G$. Thus the repaired conclusion is
$$
\boxed{\mathcal H_F\models G\ \Longleftrightarrow\ F\models G
\quad\text{for satisfiable universal Horn }F\text{ and positive existential }G.}
$$
The satisfiability qualification is separately necessary when general <Horn clauses> may have no positive conclusion. For instance, $F=\forall x(P(x)\land\neg P(x))$ is a <logical conjunction> of <Horn clauses> with no models. The intersection convention then makes every ground atom true by vacuity, yet $F$ entails even $\exists x\neg P(x)$, which that <Herbrand structure> falsifies. The earlier satisfiable example already refutes the printed claim without relying on this further defect.
Back to article page
