Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 8

Using first-order logic with equality, one suitable sentence isThe distinct witnesses give at least two solutions, and the universal clause excludes every third solution. All variables are bound, and the same equation variable $e$ is used in every solution predicate. This is an instance of a first-order definition of exactly finitely many witnesses.

On the universe $\mathbb{Z}$, interpret the first-order signature byThis assigns both constants, a total binary function, a unary relation and a binary relation, so it specifies a complete first-order structure. If $R_2(x)$ and $R_2(y)$ both hold, then $x,y\ge 0$, and hence $f(c_1,c_2)=0\le x+y=f(x,y)$, proving the consequent. If either premise fails, the implication is true. Thus the universally quantified implication holds for every pair of integers, nonvacuously for every pair of nonnegative integers. Distinct constant symbols need not denote distinct objects unless a separate axiom requires it.

Describe a branching vertex by the first-order logic sentenceand the existence of a sink by $\delta =\exists x\forall y\neg E(x,y)$. The directed path has sinks but no branching vertex; the directed cycle has neither sinks nor branching vertices; the directed arborescence has a branching vertex. Thus the following three sentences distinguish the named structures in order:Here $\beta ,\delta$ are abbreviations for the displayed formulas; replacing them gives sentences in the single-relation first-order signature $\{E\}$. Explicitly, ${\phi }_1$ says that some vertex has no successor and that no vertex has two distinct successors. The truth table across the three structures is:

The conditions distinguish these three finite structures; they are not claimed to characterize all directed paths, cycles or trees among arbitrary directed graphs. Only local out-degrees and the presence of a sink are needed, without quantifying over paths of unbounded length.

The occurrence of $y$ in $P(x,y)$ lies under the quantifier $\exists x$. Directly inserting the term $x+z$ would capture its free $x$: the result $\exists xP(x,x+z)$ would make the inserted $x$ bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.

Perform capture-avoiding first-order substitution by first renaming bound variables to fresh names. Renaming the first binder to $u$ is necessary; renaming the second to $v$ is optional but makes the result especially clear. These renamings give the equivalent formula $(\exists uP(u,y))\vee (\exists vQ(v))$. Substituting only the free occurrences of $y$ now givesBoth $x$ and $z$ in the inserted term remain free variables. The original $\exists z$ has scope only over its own disjunct and would not capture the inserted $z$ in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.

First negate the implication, then move the negation through the existential quantifier and the logical conjunction:This is negation normal form, because each negation is immediately in front of an atomic predicate. The occurrence of $z$ remains free. Keeping $\neg (z<y)$ also avoids assuming any additional order axioms for the relation symbol $<$; if it has its usual linear-order interpretation, that atom can instead be expressed as $z\ge y$.