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 / 8

Express existence of a minimum using only the given strict-order relation:In the closed interval $[0,1]$, the witness is $m=0$. In the open interval $(0,1)$, every possible witness $m$ has the smaller member $m/2$, so the first-order sentence is false. These witnesses are explanations in the ambient real numbers, not additional symbols in the first-order signature.

Express that the order is a dense order:In either real interval, $(x+y)/2$ lies strictly between any two distinct ordered elements and remains in the domain. In the integers, $x=0,y=1$ have no intervening integer, so this first-order sentence is false. The endpoints of a closed interval do not prevent a dense order.

Combine a minimum with an adjacent pair in a linear order:In $[0,1]\cup [2,3]$, choose $m=0,u=1,v=2$. The minimum and the adjacent pair in a linear order both exist. In $[0,1]$, the dense order property rules out such an adjacent pair. In $\mathbb{Z}$, adjacent pairs exist, but no minimum exists: for any $m$, the integer $m-1$ is smaller. Thus this first-order sentence has precisely the required three truth values. Neither the endpoints nor the numerical witnesses occur as constant symbols in the first-order sentence.

Use the intended first-order structure of real arithmetic, with Int selecting the integers; $z$ is the parameter in ${\varphi }_z$. A suitable first-order formula isThe first condition requires a real square root of $2z$. The second excludes every representation as a rational number $p/q$ with a nonzero integer denominator. This uses only the listed function and constant symbols, the Int predicate and logical equality; in particular, $2$ is written $1+1$ and there is no extra division symbol. A square root exists exactly when $z\ge 0$, and either sign of a root is a rational number exactly when the other sign is a rational number, so the absence of a positivity condition on $r$ does not affect the claim about the principal square root. At $z=0$ the formula is false; for $z<0$ there is no real witness. The meanings of $+$ and $\ast$ as real arithmetic, not just the meaning of Int, are part of this interpretation.

Two unary predicates suffice. Require all four unary predicate types to be inhabited:There are no constants, no logical equality and no nonunary predicates. Any two of these conditions disagree on at least one predicate, so one domain element cannot witness both. Hence every satisfying first-order structure has at least four elements, by distinct witnesses from incompatible unary predicates. Conversely take domain $\{a,b,c,d\}$, $P=\{a,b\}$ and $Q=\{a,c\}$: the four elements realize the four displayed unary predicate types, respectively. These element names describe the example; they are not constants in the first-order sentence.

The term $x+z$ is not free for substitution for $y$. The occurrence of $y$ in $x<y$ is under $\exists x$, which would capture the inserted $x$. The other occurrence, in the outside disjunct $y<z$, has no enclosing quantifier. The inner $\forall z$ does not bind the occurrence of $y$ in its antecedent, so it creates no additional capture at that substitution site.

Rename the bound $x$ to a fresh $u$, then carry out capture-avoiding first-order substitution. The result isThe inserted $z$ in $u<x+z$ remains free because it lies outside the scope of $\forall z$. One may additionally rename that bound $z$ for readability, but it is not necessary for correctness.

The term $x+z$ is free for substitution for $z$. The only free occurrence of the target $z$ is in the outside disjunct $y<z$, beyond both quantifier scopes. The occurrences under $\forall z$ are bound variables and are not replaced. Therefore no renaming is required, andThe new $x$ and $z$ in the last disjunct are free. First-order substitution replaces the original free occurrences once; it does not recursively substitute into the inserted term.

The printed expression has one unmatched closing parenthesis. Remove that final surplus parenthesis and read the first disjunct as $\exists xP(x)$; the other disjunct has outer universal quantification over the displayed implication. To distinguish the two independent bound uses of $x$, rename the first to $u$.

Push the outer negation through the logical disjunction and through the quantifiers. Negating the implication preserves its existential antecedent and negates its consequent. Applying De Morgan's laws and the quantifier negation rules gives the negation normal formEach negation is now directly before an atomic formula. No bound variable has been captured, and no original existential quantification in the antecedent has accidentally been negated twice.