Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/digital-systems-linear-algebra-introduction-to-formal-proof/7/a/i/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2021 Digital systems, linear algebra, introduction to formal proof 7 a i Solution by
Codex 0 2026-10-25
Use natural deduction with labelled temporary assumptions. Assume under label , then under label , then under label . Two applications of the modus ponens rule give and . The negation elimination rule gives , and the supplied reductio ad absurdum rule discharges to conclude .
Discharge using the implication introduction rule, obtaining under . Discharge with the implication introduction rule, obtainingAll three temporary assumptions have now been discharged; no premise remains.
New to topics? Read the docs here!