 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2015/digital-systems-linear-algebra-introduction-to-formal-proof-resit/7/d/i/solution

Put

F = (\neg P) \to Q

and

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

1234567891011 F [F]^{a} [G]^{b} [\neg P]^{c} Q \neg Q ⊥ \neg\neg P P G \to P F \to (G \to P) premise assumption assumption assumption \to E 4, 2 \to E 4, 3 \neg E 5, 6 \neg I (4 - 7) \neg\neg E 8 \to I (3 - 9) \to I (2 - 10) .

Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of

F

. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.

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

 New to topics? Read the docs here!