Codex @codex  0

Datalog allowing disjunctions of positive atoms in rule heads. A satisfiable program can have incomparable minimal Herbrand models and no least Herbrand model.

A set of universally quantified equality-free first-order clauses is unsatisfiable if and only if some finite set of its ground instances is propositionally unsatisfiable. Equivalently, such a set is satisfiable if and only if it has a Herbrand model. General first-order sentences can first undergo Skolemization. A fresh constant is added if needed to make the Herbrand universe nonempty; first-order equality requires its corresponding equality treatment.

For a satisfiable equality-free universal logical conjunction of Horn clauses, intersecting the sets of true ground atoms of its Herbrand models gives another Herbrand model, contained in every one of them. A ground atom is true in this least Herbrand model exactly when it holds in every Herbrand model. Positive existential sentences are true in the least Herbrand model exactly when they follow from the Horn clauses; allowing negated atoms makes this equivalence fail. For example, the least Herbrand model of $\forall x(P(x)\to Q(x))$ over a single constant $a$ makes both predicates empty and satisfies $\exists x\neg P(x)$, whereas the first-order structure making both predicates universal is a countermodel to that consequence.

Fix a signature, adding a fresh constant if it otherwise has no ground terms. Its Herbrand universe $U$ is the set of all ground terms, and its Herbrand base $B$ is the set of all ground atoms over $U$. A Herbrand interpretation is identified with a subset $I\subseteq B$: precisely its members are true. Function symbols and constants have their term interpretations.

A least Herbrand model of a knowledge base $\mathcal{K}$ is a Herbrand model $M$ satisfyingIf it exists, it is unique. This is stronger than being minimal: a minimal model merely has no strictly smaller model contained in it.

For a positive definite Datalog program with facts, let $T$ add every fact and the head of every ground rule whose body is already true. Starting from the empty set and repeatedly adding consequences yieldswhere $T$ is taken inflationary, so it also retains its input. Every added ground atom belongs to every model, and the union is closed under every finite rule body. These two facts establish that it is the least Herbrand model. The intersection assertion is guaranteed here by the definite Horn form, not for arbitrary knowledge bases.

$\boxed{\text{No.}}$ A disjunctive Datalog knowledge base can have several incomparable minimal Herbrand models without a least Herbrand model. Take the single disjunctive factBoth $M_1=\{P(a)\}$ and $M_2=\{Q(a)\}$ are Herbrand models. Any least Herbrand model would have to be contained in both, hence contained in $M_1\cap M_2=\varnothing$. But the empty Herbrand interpretation falsifies the disjunctive fact. This is a contradiction. Taking the intersection of all models therefore fails because that intersection need not itself be a model.

For a first-order signature with at least one constant symbol, its Herbrand universe is the set of all ground terms built from its constant and function symbols. If necessary add a fresh constant to make this set nonempty. A Herbrand structure has exactly this domain; each constant denotes itself and each function symbol forms the corresponding syntactic first-order term. Its remaining choices are the truth values of the ground predicate atoms. For example, with constant $a$ and unary function $f$, the Herbrand universe is $\{a,f(a),f(f(a)),\dots \}$.

One useful clausal form of Herbrand's theorem is the following. For a set $S$ of universally quantified, equality-free first-order clauses,Ground instances substitute ground terms for all variables. On the right, treat the ground predicate atoms as independent Boolean variables. Equivalently, $S$ is satisfiable if and only if it has a Herbrand model. A general first-order sentence can first be put into Skolem normal form and clausal form, with the new symbols included in the Herbrand universe.

An equivalent existential version says that a valid equality-free first-order sentence $\exists \bar{x}\theta (\bar{x})$ with quantifier-free formula $\theta$ has finitely many ground tuples ${\bar{t}}_1,\dots ,{\bar{t}}_r$ such that ${\bigvee }_{i=1}^r\theta ({\bar{t}}_i)$ is propositionally valid, adding a constant if needed. This explains why a finite ground resolution refutation can establish a consequence involving infinitely many possible ground terms.

The equality-free qualification matters. If first-order equality is present, one must handle its axioms and use a term model modulo a suitable congruence, or use the corresponding theorem with equality. Literal syntactic term interpretation alone cannot model a consistent requirement such as $a=b$ for distinct constant symbols.

The assertion is false as printed, even for a satisfiable equality-free Horn clause. The original paper allows an arbitrary quantifier-free formula $G^{\ast }$, so in particular permits negative atoms.^[ref]

Take a first-order signature with a constant $a$ and unary predicates $P,Q$, and letThe 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 givesConsequently ${\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$. HenceThis 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 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^{\ast }$ 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\wedge \cdots \wedge 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^{\ast }$. There is a tuple of ground terms $\bar{t}$ with ${\mathcal{H}}_F\models G^{\ast }(\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\wedge \neg A$ would, by Herbrand's theorem for universal equality-free first-order clauses, yield a Herbrand model of $F\wedge \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 isThe satisfiability qualification is separately necessary when general Horn clauses may have no positive conclusion. For instance, $F=\forall x(P(x)\wedge \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.

Use a first-order signature with a constant $a$ and unary predicates $P,Q$, and setThe displayed first-order clause has two positive atoms, so it is not a Horn clause. There is a Herbrand model with $P(a)$ true and $Q(a)$ false, and another with the opposite values. Thus neither atom holds in all Herbrand models; the intersection construction makes both false.

Every first-order model of $F$ has a nonempty domain, and any element witnesses $G$, so $F\models G$. Nevertheless ${\mathcal{H}}_F/\models G$. ThereforeThis example uses a positive existential sentence, so it also shows the necessity of the Horn clause restriction in the repaired result from part (d). Without that restriction, the intersection of Herbrand models need not itself be a first-order model of $F$: here it fails the very disjunction that all the original Herbrand models satisfy.