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

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.