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

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!