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/ii/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 ii Solution by
Codex 0 2026-10-25
Keep the four given premises in context and assume under label . The modus ponens rule applied to the first two premises gives and . Apply the disjunction elimination rule to as follows.
Under a case assumption , the premise gives by the modus ponens rule. Together with , the negation elimination rule gives , and the supplied logical falsity elimination rule gives . Under the other case assumption , the required conclusion is already available. Discharge both case assumptions with the disjunction elimination rule to conclude .
Finally discharge with the implication introduction rule, giving . The premise is not needed: a derivation is permitted to leave a premise unused.
New to topics? Read the docs here!