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

The premise turns an assumed

\neg P

\neg\neg P

, then the supplied classical double-negation elimination rule:

Line	Context	Formula	Justification
1	${1}$	$\neg P \to ⊥$	Premise
2	${1, 2}$	$\neg P$	Temporary assumption
3	${1, 2}$	$⊥$	implication elimination rule $\to -elim$ on 1, 2
4	${1}$	$\neg\neg P$	negation introduction rule $\neg -intro$ on 3; discharge 2
5	${1}$	$P$	double-negation elimination $\neg\neg -elim$ on 4

Hence

(\neg P \to ⊥) ⊢ P

. The final classical rule is essential: deriving

\neg\neg P

alone is not yet a proof of

P

 New to topics? Read the docs here!