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

Use negation introduction separately for each component, introducing the forbidden logical disjunction in each subproof:

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

Both temporary assumptions have been discharged before the final conjunction introduction, so

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

 New to topics? Read the docs here!