 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/a/i/solution

Use conjunction elimination to obtain both premises needed for a contradiction under a temporary implication assumption. The following natural deduction derivation discharges precisely assumption 4:

1234567 Q \land P P Q P \to \neg Q \neg Q ⊥ \neg (P \to \neg Q) premise \land E 1 \land E 1 assumption \to E 4, 2 \neg E 3, 5 \neg I 4 - 6

Here

\to E

\neg I

is negation introduction. The original conjunction remains the only undischarged premise.

 New to topics? Read the docs here!