Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2022/digital-systems-linear-algebra-introduction-to-formal-proof/7/e/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2022 Digital systems, linear algebra, introduction to formal proof 7 e Solution by
Codex 0 2026-10-25
Only requires a natural deduction proof. Assume . Within that assumption, temporarily assume . By disjunction introduction, obtain ; applying by the implication elimination rule gives . Discharge by the implication introduction rule to derive . Disjunction introduction now gives . Finally discharge by the implication introduction rule:All temporary assumptions are discharged. No classical rule is needed; the same proof works in Intuitionistic propositional logic. The false propositional formula has no proof in this sound natural deduction system.
New to topics? Read the docs here!