Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof (A10468W1)

Solutions to the three questions of the University of Oxford computer science Finals examination held on 10 June 2015. Question 3(d) has a false assertion as printed; its solution gives a countermodel and explains the additional hypotheses under which the usual least Herbrand model argument works.^[ref]

Apply the distributive law of Boolean algebra to the two logical conjunctions. With $A=P$, $B=\neg Q$, $C=\neg P$, and $D=Q$, the identity $(A\wedge B)\vee (C\wedge D)\equiv (A\vee C)\wedge (A\vee D)\wedge (B\vee C)\wedge (B\vee D)$ givesThe second step uses complementation and commutativity in Boolean algebra; the last uses the identity law for logical conjunction. The result is in conjunctive normal form: its first Boolean clause requires at least one input to be true, and its second Boolean clause prohibits both inputs being true. Together they express exclusive or.

Replace each implication by a logical disjunction and use the conjunctive normal form for exclusive or from part (a). The resulting Boolean clauses areHere the displayed array is a list of the six Boolean clauses, whose logical conjunction is equivalent to all four constraints.

Use resolution first on $I$, then on $T$, and finally on $H$:Removing the repeated Boolean literal in the final Boolean clause uses idempotence. Neither $C_4$ nor $C_6$ is needed: even the weaker assumptions that the coin has at least one outcome and that at least one person wins already force $Y$, once the two implications hold.

Take the single Boolean clauseThis is a 3-CNF formula. Suppose a 2-CNF formula $K$ were logically equivalent to $F$. Every Boolean clause $C$ of $K$ would then be a consequence of $F$.

Consider any nontautological Boolean clause $C$ containing at most two Boolean literals. Choose a Boolean valuation falsifying its Boolean literals. At least one of $P,Q,R$ does not occur in $C$; assign that Boolean variable true. The resulting Boolean valuation satisfies $F$ while falsifying $C$. This contradicts $F\models C$. An empty Boolean clause also cannot be a consequence of the satisfiable $F$.

Consequently every Boolean clause of $K$ would have to be a tautology. Their logical conjunction would be true under every Boolean valuation, whereas $F$ is false when $P=Q=R=0$. This proves that no such $K$ exists.

The argument even allows additional ordinary Boolean variables in $K$: at most two Boolean literals still leave one of $P,Q,R$ free to be made true. Introducing extra variables together with existential quantification would change the requested notion of logical equivalence, so it is not a way around the argument.

Enumerate the vertices as $V=\{1,\dots ,n\}$ and introduce a Boolean variable $X_{u,v}$ for each ordered pair of vertices. Its intended meaning is that a proposed graph automorphism sends $u$ to $v$. Build four groups of Boolean clauses.

First require exactly one image for each vertex:Next require that distinct vertices have distinct images:Together $A$ and $B$ specify an injective function $f:V\to V$. Since $V$ is finite, this function is a bijection; a separate surjectivity condition is unnecessary.

Write $e(u,w)=1$ when $(u,w)\in E$ and $e(u,w)=0$ otherwise. Prohibit every pair of images that would change adjacency:Checking both possible mismatches preserves both edges and nonedges. Finally require a moved vertex:The desired propositional formula is

If a Boolean valuation satisfies ${\phi }_G$, $A$ selects a unique image for every vertex, $B$ makes the resulting function a bijection, $C$ preserves adjacency in both directions, and $D$ makes this graph automorphism different from the identity function. Conversely, given such a graph automorphism $f$, set $X_{u,v}$ true exactly when $v=f(u)$. Each of $A,B,C,D$ is then satisfied.

There are $n^2$ Boolean variables, $O(n^3)$ image and injectivity Boolean clauses, and at most $n^4$ adjacency Boolean clauses. With the graph stored by its adjacency matrix, testing a mismatch takes constant time. Thus the construction has polynomial time and output length $O(n^4\log (n+1))$ with binary-indexed variable names. For $n=0$, interpret the empty logical disjunction $D$ as false; for $n=1$, $A$ and $D$ conflict. These cases correctly have no nonidentity graph automorphism.

The propositional compactness theorem states that an arbitrary set $S$ of propositional formulas is satisfiable if and only if every finite subset of $S$ is satisfiable:The satisfying Boolean valuation may depend on $S_0$ on the right; the conclusion on the left provides one Boolean valuation satisfying all of $S$ simultaneously.

Let $S=\{F_i:i\ge 1\}$. Every finite subset of $S$ is satisfiable: if $F_N$ has the largest index occurring, the successive semantic entailments imply $F_N\models F_i$ for every earlier index, so any Boolean valuation satisfying $F_N$ satisfies that finite subset. The propositional compactness theorem therefore also shows that $S$ itself is satisfiable.

Suppose that $G$ had exactly the common models of $S$. Then $S\models G$, and hence $S\cup \{\neg G\}$ is unsatisfiable. By the propositional compactness theorem, finitely many $F_i$ together with $\neg G$ are already unsatisfiable. Enlarge the finite list if necessary so it is nonempty, and let $N$ be its greatest index. We obtainOn the other hand, the asserted equality of model classes gives $G\models F_{N+1}$. Transitivity of semantic entailment would yieldcontradicting the strictness assumption at index $N$. ThusThe obstruction is the finite character of propositional formulas: a single consequence of an infinite set already follows from finitely many premises, whereas this chain continues to impose strictly stronger requirements forever.

A first-order theory in a fixed first-order signature is a set of first-order sentences. Under the closed-theory convention used in the question, it contains all its semantic entailments: $T\models \theta$ implies $\theta \in T$. One can equivalently begin with a set of axioms and take its closure under consequence.

A complete theory is a consistent first-order theory that decides every first-order sentence $\theta$ in its first-order signature:Consistency ensures that exactly one of these alternatives holds.

A decidable theory is one for which an algorithm always terminates and determines whether a given first-order sentence is a consequence:If the first-order theory is already closed under consequence, this is its membership problem. It is a condition on the consequences, not merely on whether the chosen set of axioms has a decidable membership test.

A first-order theory $T$ admits quantifier elimination when every first-order formula $\phi (\bar{x})$ has a quantifier-free formula $\psi (\bar{x})$, in the same first-order signature and with no additional free variables, such thatThus all first-order models of $T$ agree that the two first-order formulas define the same tuples. This definition concerns first-order formulas with free variables, as well as first-order sentences; merely deciding closed assertions would be weaker. The existence of an effective procedure is an additional issue, supplied by the explicit construction in part (d).

Use the Rado graph on the natural numbers. Interpret the binary relation byThe relation is symmetric by its definition, and $E(i,i)$ is always false. Thus this first-order structure satisfies $F_1$ and $F_2$.

To verify an extension axiom, take distinct $x_1,\dots ,x_n$. Choose a natural number $k$ larger than every $x_i$ and putThe powers are distinct, so there are no carries in this binary representation. In particular $y>x_i$ for every $i$, and the bit in position $x_i$ is one exactly when $i<m$. Therefore $y$ is different from all the given vertices, is adjacent to $x_1,\dots ,x_{m-1}$, and is not adjacent to the others. If the $x_i$ are not distinct, the antecedent of the extension axiom is false, so it places no restriction. The case $n=0$, if included in the convention for natural numbers, simply asks for a nonempty domain, which this first-order structure has.

For example, prescribing adjacency to $1$ and $3$ and nonadjacency to $2$ permits $k=4$ and $y=16+2+8=26$, whose binary representation is $11010$. This explicitly realizes the required pattern. HenceReordering a tuple makes the extension axioms applicable to any two disjoint finite sets of vertices, with any desired adjacency and nonadjacency pattern. This is the extension property defining the theory of the random graph.

It suffices to eliminate one existential quantifier from a quantifier-free formula $\theta (y,\bar{x})$. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using $\forall y\alpha \equiv \neg \exists y\neg \alpha$. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert $\theta$ to disjunctive normal form. Since existential quantification distributes over a finite logical disjunction, consider a single logical conjunction of atomic first-order formulas and their negations. There are no function or constant symbols in this first-order signature, so its atoms are equalities between variables and instances of $E$ between variables.

For a tuple $\bar{x}=(x_1,\dots ,x_r)$, enumerate its possible complete atomic diagrams $\delta (\bar{x})$. Such a quantifier-free formula specifies which variables are equal and, between distinct equality classes, exactly which pairs are adjacent. Keep only the diagrams in which first-order equality is an equivalence relation and $E$ is symmetric and irreflexive. There are finitely many diagrams for each $r$, and every tuple in a first-order model of $T$ satisfies exactly one of them. Every retained diagram is realizable: insert one vertex for each equality class successively, using the extension axioms to prescribe its adjacency to earlier vertices.

Fix one diagram $\delta$. A potential existential witness for $y$ has one of two forms.

All first-order formulas involving only $\bar{x}$ are already decided by $\delta$. Therefore, for each diagram, the existence of a suitable $y$ has a definite answer, determined by a finite syntactic test. Let $\mathcal{D}$ be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. ThenThe right side is a quantifier-free formula. An empty logical disjunction means false, and for an empty tuple the empty atomic diagram means true. These logical truth constants also handle closed first-order sentences in this constant-free first-order signature.

For a concrete illustration of the fresh-witness case,If $x_1=x_2$, the edge requirements conflict. Otherwise the extension property supplies a vertex outside the finite set of parameters with the desired pattern; the extra avoidance of $x_3$ causes no obstruction. The general diagram construction handles all such equality coincidences systematically and proves quantifier elimination.

By part (c), $T$ has a first-order model, so it is consistent. By part (d), every first-order sentence is equivalent modulo $T$ to a quantifier-free sentence. In the first-order signature consisting only of $E$ and first-order equality, there are no constant symbols, no ground first-order terms, and no nullary predicates. Thus a closed quantifier-free formula reduces to true or false, using the logical truth constants. All first-order models of $T$ therefore agree on every first-order sentence:

The construction in part (d) is effective. Conversion to disjunctive normal form, enumeration of finite equality partitions and adjacency patterns, and testing the finitely many witness cases are all terminating operations. Apply them recursively to a given first-order sentence and evaluate the final truth constant. This decides whether the first-order sentence belongs to $T$, givingNo useful bound on the running time is needed for decidability; the potentially large enumeration still always terminates.

Use the back-and-forth method. Enumerate the two domains without repetitions as $a_0,a_1,\dots$ and $b_0,b_1,\dots$. We construct a sequence of finite maps, each a partial isomorphism of structures,starting with the empty function. Each $f_s$ is a bijection between finite subsets of the domains and preserves both adjacency and nonadjacency on its domain.

At a forth step, choose the first $a_i$ outside the current domain. List the finitely many domain vertices as $u_1,\dots ,u_r$. In $\mathcal{B}$, prescribe that the new image $b$ be adjacent to $f_s(u_j)$ exactly when $a_i$ is adjacent to $u_j$ in $\mathcal{A}$. Since the image vertices are distinct, an extension axiom in $\mathcal{B}$ supplies such a $b$ outside the entire current range. Extend $f_s$ by $a_i\mapsto b$. This preserves injectivity, adjacency and nonadjacency, including the absence of loops.

At a back step, choose the first $b_i$ outside the current range. Apply the same argument to the inverse partial isomorphism of structures in $\mathcal{A}$, finding a fresh preimage with the required adjacency pattern to the current domain. Extend $f_s$ by this new pair. Alternate forth and back steps indefinitely.

DefineBecause each finite function extends the preceding one, this is a well-defined injective function. The forth steps eventually include every $a_i$ in its domain, and the back steps eventually include every $b_i$ in its range, so $f$ is a bijection. Given any $u,v$, both lie in the domain of some finite $f_s$, where the edge equivalence already holds. It therefore also holds for $f$:Thus the two first-order structures are isomorphic. Alternating the steps is essential for surjectivity: repeatedly extending only the domain would merely construct an embedding into $\mathcal{B}$.

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.