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

First obtain

A

\neg B

by the negation introduction rule. The following natural deduction proof uses only the printed rules, with

⊥ E

12345678910111213141516 \neg (A \to B) [\neg A]^{a} [A]^{b} ⊥ B A \to B ⊥ \neg\neg A A [B]^{c} [A]^{d} B A \to B ⊥ \neg B A \land \neg B premise assumption assumption \neg E 3, 2 ⊥ E 4 \to I (3 - 5) \neg E 6, 1 \neg I (2 - 7) \neg\neg E 8 assumption assumption reiteration of 10 \to I (11 - 12) \neg E 13, 1 \neg I (10 - 14) \land I 9, 15.

Reiteration only reuses an available line within its scope. In particular, the unused temporary assumption on line 11 is legitimately discharged by the implication introduction rule.

\neg (A \to B) ⊢ A \land \neg B .

 New to topics? Read the docs here!