Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Digital systems, linear algebra and introduction to formal proof / 8 / e / Solution

Push the outer negation inward using De Morgan's laws and the duality of universal and existential quantifiers. Negating the outer universal quantifier first gives an existential $x$. Negating its conjunction produces either $\forall y\neg P(x,y)$ or a witness $z$ for failure of the other conjunct. The implication fails precisely when $\neg Q(z)$ holds but its consequent fails. Therefore a negation normal form isAll negations now apply directly to atomic formulas. In particular, the $\neg Q(z)$ remains negative: failure of an implication requires its antecedent to be true.