 Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/logic-and-proof/2/d/solution

 Top articles  Latest articles New article in topic

Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 2 / d / Solution by

Codex  0 2026-10-31

It suffices to eliminate one existential quantifier from a quantifier-free formula

θ (y, \overset{x}{ˉ})

. Indeed, logical connectives preserve equivalence, and a universal quantifier can be rewritten using

\forall y α \equiv \neg\exists y \neg α

. An induction on the construction of a first-order formula then eliminates all its quantifiers from the inside out.

Convert

θ

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

\overset{x}{ˉ} = (x_{1}, \dots, x_{r})

, enumerate its possible complete atomic diagrams

δ (\overset{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

δ

. A potential existential witness for

y

has one of two forms.

An existing vertex. If $y = x_{i}$ , substitute $x_{i}$ for $y$ in the logical conjunction. The diagram $δ$ decides the truth value of every resulting atom, and so decides whether this choice works.
A new vertex. Require $y \neq = x_{i}$ for every $i$ . Simplify $y = y$ to true and $E (y, y)$ to false. Use symmetry to rewrite every remaining edge requirement involving $y$ in the form $E (x_{i}, y)$ or $\neg E (x_{i}, y)$ . An equality $y = x_{i}$ , a positive loop requirement, or opposite edge requirements on the same equality class makes this case impossible. Otherwise the requirements give a consistent adjacency pattern on finitely many distinct vertices. Any equality classes without a specified edge requirement can be assigned either pattern. Reorder representatives with the desired neighbours first; the appropriate extension axiom supplies a fresh vertex with precisely this pattern.

All first-order formulas involving only

\overset{x}{ˉ}

are already decided by

δ

. Therefore, for each diagram, the existence of a suitable

y

has a definite answer, determined by a finite syntactic test. Let

D

be the set of diagrams for which at least one disjunct and at least one of the two witness cases succeeds. Then

T ⊨ \forall \overset{x}{ˉ} [\exists y θ (y, \overset{x}{ˉ}) \leftrightarrow δ \in D ⋁ δ (\overset{x}{ˉ})] .

(1)

The 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,

T ⊨ \forall x_{1} \forall x_{2} \forall x_{3} [\exists y (E (y, x_{1}) \land \neg E (y, x_{2}) \land y \neq = x_{3}) \leftrightarrow x_{1} \neq = x_{2}] .

(2)

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.

 Read the full article

 New to topics? Read the docs here!