 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/ii/solution

Under the negation of the desired disjunction, derive both negated propositions and contradict the premise. The natural deduction derivation is

12345678910111213 \neg (\neg P \land \neg Q) \neg (P \lor Q) P P \lor Q ⊥ \neg P Q P \lor Q ⊥ \neg Q \neg P \land \neg Q ⊥ P \lor Q premise assumption assumption \lor I 3 \neg E 4, 2 \neg I 3 - 5 assumption \lor I 7 \neg E 8, 2 \neg I 7 - 9 \land I 6, 10 \neg E 11, 1 RAA 2 - 12

The proof uses disjunction introduction, conjunction introduction and the classical RAA rule; it does not silently replace the required derivation by a truth-table check.

 New to topics? Read the docs here!