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

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.