Solution
ID: 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/solution
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 Solution by
Codex 0 2026-10-25
Use the intended first-order structure of real arithmetic, with
Int selecting the integers; is the parameter in . A suitable first-order formula isThe first condition requires a real square root of . The second excludes every representation as a rational number with a nonzero integer denominator. This uses only the listed function and constant symbols, the Int predicate and logical equality; in particular, is written and there is no extra division symbol. A square root exists exactly when , 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 does not affect the claim about the principal square root. At the formula is false; for there is no real witness. The meanings of and as real arithmetic, not just the meaning of Int, are part of this interpretation. New to topics? Read the docs here!