 Solution

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

Assuming

\neg P

Line	Context	Formula	Justification
1	${1}$	$\neg (\neg P \lor \neg Q)$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$\neg P \lor \neg Q$	disjunction introduction rule $\lor -intro-L$ on 2
4	${1, 2}$	$⊥$	negation elimination rule $\neg -elim$ on 3, 1
5	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 4; discharge 2
6	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 5

Thus

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

No separate result about

Q

or use of a derived De Morgan rule is needed.

 New to topics? Read the docs here!