 Solution

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

Put

H = \neg (P \to \neg Q)

. First derive

Q

, then

P

, using the derived proof by contradiction rule. Indentation records the subproofs:

123456789101112131415 H \neg Q P \neg Q P \to \neg Q ⊥ Q \neg P P ⊥ \neg Q P \to \neg Q ⊥ P Q \land P premise assumption assumption reiterate 2 \to I 3 - 4 \neg E 1, 5 RAA 2 - 6 assumption assumption \neg E 9, 8 ⊥ E 10 \to I 9 - 11 \neg E 1, 12 RAA 8 - 13 \land I 7, 14

Line 11 uses explosion; lines 5 and 12 discharge only their inner assumptions. Each RAA step can be expanded into negation introduction followed by double-negation elimination, as in part (ii).

 New to topics? Read the docs here!