Solution

ID: 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 . Negating its conjunction produces either or a witness for failure of the other conjunct. The implication fails precisely when holds but its consequent fails. Therefore a negation normal form is
All negations now apply directly to atomic formulas. In particular, the remains negative: failure of an implication requires its antecedent to be true.

New to topics? Read the docs here!