 Solution

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

Codex  0 2026-10-31

Under the premise, assuming either disjunct would introduce the forbidden logical disjunction. Discharging those two assumptions gives the two separate negations, which can then be conjoined.

Table 1.

Derivation of the two negated disjuncts

Line	Open assumptions	Formula	Justification
1	1	$\neg (P \lor Q)$	Premise
2	1, 2	$P$	Temporary assumption
3	1, 2	$P \lor Q$	disjunction introduction L 2
4	1, 2	$⊥$	negation elimination rule 3, 1
5	1	$\neg P$	negation introduction 2, 4
6	1, 6	$Q$	Temporary assumption
7	1, 6	$P \lor Q$	disjunction introduction R 6
8	1, 6	$⊥$	negation elimination rule 7, 1
9	1	$\neg Q$	negation introduction 6, 8
10	1	$\neg P \land \neg Q$	conjunction introduction 5, 9

Thus

\neg P \land \neg Q .

(1)

The redundant closing parenthesis printed after the conclusion on p. 8 does not alter the readable propositional formula.^[ref]

 Read the full article

 New to topics? Read the docs here!