 Solution

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

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 7 / b / Solution by

Codex  0 2026-10-31

Use disjunction introduction, negation introduction and conjunction introduction in the following natural deduction proof. Indentation marks the assumptions discharged at their closing lines.

1. ¬(φ ∨ ψ)             premise
2.   φ                  assumption [i]
3.   φ ∨ ψ              ∨I-left, 2
4.   ⊥                  ¬E, 1, 3
5. ¬φ                   ¬I, 2–4, discharging [i]
6.   ψ                  assumption [j]
7.   φ ∨ ψ              ∨I-right, 6
8.   ⊥                  ¬E, 1, 7
9. ¬ψ                   ¬I, 6–8, discharging [j]
10. ¬φ ∧ ¬ψ             ∧I, 5, 9

The two separate temporary assumptions establish the two required negations; neither is retained in the conclusion.

 Read the full article

 New to topics? Read the docs here!