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/7/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 7 e Solution by
Codex 0 2026-10-25
Keep the premise open. Assume , then temporarily assume . Two applications of the implication elimination rule produce and then , contradicting the temporary . Discharge using the negation introduction rule, then discharge using the implication introduction rule.This natural deduction proof uses only the supplied introduction and elimination rules. Line 6 is an application of the negation elimination rule; no classical contradiction principle is needed.
New to topics? Read the docs here!