 Solution

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

Codex  0 2026-10-25

Write

H

for

(ϕ \to ψ) \to ϕ

. The following derives Peirce's law directly from the printed primitive rules, including double-negation elimination:

Line	Formula	Justification
1	$H$	Assume for the final implication
2	$\neg ϕ$	Assume locally
3	$ϕ$	Assume inside the scope of 2
4	$⊥$	Negation elimination rule, 2 and 3
5	$ψ$	Logical falsity elimination rule, 4
6	$ϕ \to ψ$	Implication introduction rule, discharging 3–5
7	$ϕ$	Implication elimination rule, 1 and 6
8	$⊥$	Negation elimination rule, 2 and 7
9	$\neg\neg ϕ$	Negation introduction rule, discharging 2–8
10	$ϕ$	Double-negation elimination, 9
11	$((ϕ \to ψ) \to ϕ) \to ϕ$	Implication introduction rule, discharging 1–10

Every assumption is discharged, so the last formula is a theorem. In particular, no unproved appeal to the derived RAA rule is hidden in the argument.

 Read the full article

 New to topics? Read the docs here!