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

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!