 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2022/digital-systems-linear-algebra-introduction-to-formal-proof-resit/7/e/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 / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 7 / e / Solution by

Codex  0 2026-10-25

Assume the logical conjunction temporarily, then eliminate the premise's logical disjunction by cases. A natural deduction proof, with each indented assumption delimiting its own subproof, is:

1.  not P or not Q                    premise
2.  | P and Q                        temporary assumption
3.  | P                              and-elim-L, 2
4.  | Q                              and-elim-R, 2
5.  | | not P                        first disjunction case
6.  | | false                        not-elim, 3,5
7.  | | not Q                        second disjunction case
8.  | | false                        not-elim, 4,7
9.  | false                          or-elim, 1, cases 5-6 and 7-8
10. not (P and Q)                     not-intro, discharge 2-9

Lines 5–6 and 7–8 are separate sibling subproofs, not one nested inside the other. Both derive the same contradiction under the common assumption on line 2. Logical disjunction elimination discharges the two case assumptions, and negation introduction then discharges the logical conjunction assumption. The sole undischarged premise is the required one. This proof uses only the supplied logical conjunction, logical disjunction and negation rules; no converse form of De Morgan's laws is being assumed as an extra rule.

 Read the full article

 New to topics? Read the docs here!