 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-resit/8/e/solution

First negate the implication, then move the negation through the existential quantifier and the logical conjunction:

\neg φ \equiv (\forall x P (x)) \land \neg\exists y (Q (y) \land z < y) \equiv (\forall x P (x)) \land \forall y (\neg Q (y) \lor \neg (z < y)) .

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 \geq y

 New to topics? Read the docs here!