Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 3

Use unary predicates $H$ and $M$ for happiness and merriness, a binary predicate $L$ with $L(x,y)$ meaning that $x$ loves $y$, and a constant symbol $\ell$ for Lucy. The domain consists of people. The following four first-order sentences use this same first-order signature.

The existential quantifier supplies the person loved, with a choice that may depend on $x$:The outer universal quantifier ranges over everyone. The logical disjunction is inclusive; it permits a person both to be happy and to love somebody.

The property of loving at least one person is the antecedent:An equivalent first-order sentence, useful for Skolemization, is $\forall x\forall y[L(x,y)\to L(x,\ell )]$. The person loved in the antecedent need not be Lucy; the conclusion concerns Lucy specifically.

The same person $y$ must both love $x$ and be loved by $x$:Equivalently, use $\forall x\forall y[(L(y,x)\wedge L(x,y))\to H(x)]$. There is no restriction that $x$ and $y$ be distinct; this matters when the later ground resolution proof considers Lucy loving herself.

Lucy's happiness is a single antecedent, while the conclusion applies to everyone:Since $x$ does not occur in the antecedent, this is equivalent to $\forall x[H(\ell )\to M(x)]$. The universal quantifier does not assert that everyone is happy; it is the merriness conclusion that is universal.

First convert the four first-order sentences to clausal form. In the first, pull the existential quantifier across the logical disjunction, then replace its witness by a fresh unary Skolem function $f(x)$. The usual nonempty-domain convention for first-order logic makes this transformation valid even when $H(x)$ already holds. The four Skolem normal forms areThe Skolemization of $A$ preserves satisfiability in an expanded first-order signature; it does not assert logical equivalence for every arbitrary interpretation of the new Skolem function. The other three first-order sentences only require elimination of implications and movement of universal quantifiers.

For a ground resolution refutation, negate the desired conclusion and introduce a fresh constant $c$ for a person who is not merry. This adds the ground clause $\neg M(c)$. Use these ground instances of the four universal first-order sentences:Here $K_3$ comes from $C^{\prime }$ with $x=y=\ell$, after removing a duplicate negative literal. All first-order terms in these ground clauses are ground. Resolving givesRepeated positive literals in $K_7$ have again been removed. The empty ground clause proves unsatisfiability of the premises together with the negated conclusion. ThereforeThe key is to apply the first three premises to Lucy herself: either she is already happy, or she loves somebody, hence loves herself, which forces her happiness and activates the final premise.

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.