 Solution

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

12345678910 \neg P \land \neg Q \neg P \neg Q ∣ P \lor Q ∣ ∣ P ∣ ∣ ⊥ ∣ ∣ Q ∣ ∣ ⊥ ∣ ⊥ \neg (P \lor Q) premise \land -elim-L 1 \land -elim-R 1 assumption first case assumption \neg -elim 5, 2 second case assumption \neg -elim 7, 3 \lor -elim 4, 5 - 6, 7 - 8 \neg -intro 4 - 9

The two case subproofs are siblings, not nested within one another. Therefore

\neg P \land \neg Q ⊢ \neg (P \lor Q) .

 New to topics? Read the docs here!