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/8/b/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 8 b ii Solution by
Codex 0 2026-10-25
Let be fresh, not free in any of the three universal premises. Universal quantifier elimination rule gives , and . Apply disjunction elimination rule to the last formula.
In the branch, apply disjunction elimination rule to . Its case contradicts by negation elimination rule, and logical falsity elimination rule then gives . Its case already gives that conclusion. Discharge those two inner case assumptions to obtain under the outer assumption. In the outer branch, the modus ponens rule applied to gives directly.
Discharge the two outer case assumptions by disjunction elimination rule. The conclusion now depends only on the universal premises, in which is not free. Universal quantifier introduction rule therefore gives . All case assumptions have been discharged, and the argument requires no classical reductio ad absurdum.
New to topics? Read the docs here!