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
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 by
Codex 0 2026-10-25
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 isAll 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!