 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2017/digital-systems-linear-algebra-introduction-to-formal-proof/7/b/i/solution

Assume the two implications in turn, then derive a contradiction from

\neg P

123456789 \neg P \to Q \neg P \to \neg Q \neg P Q \neg Q ⊥ P (\neg P \to \neg Q) \to P (\neg P \to Q) \to ((\neg P \to \neg Q) \to P) assumption assumption assumption \to E 1, 3 \to E 2, 3 \neg E 4, 5 RAA 3 - 6 \to I 2 - 7 \to I 1 - 8

Here RAA is the derived proof by contradiction rule. The last two assumption discharge steps establish the requested right-associated implication as a theorem.

 New to topics? Read the docs here!