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/b/solution

Write and . In the following natural deduction derivations, brackets name temporary assumptions, and cited ranges specify the subproofs discharged. The abbreviations denote the corresponding conjunction elimination rule, conjunction introduction rule, disjunction elimination rule and disjunction introduction rule.
First use the disjunction elimination rule backwards: split the premise into two cases and build the whole conclusion in each case.
Alternatively, use the conjunction introduction rule backwards on the conclusion. First obtain by cases, then obtain by a second case analysis, and finally combine the results:
The first proof goal transformation starts with case analysis; the second starts by splitting a conjunction goal. Counting only actual applications of the printed inference rules, both use nine steps: the first has four , two , two and one ; the second has four , two , one and two . The extra case analysis in the second exactly replaces one conjunction construction. If assumption lines are counted as well, the second display has two more lines because it opens four case subproofs rather than two. Thus the apparent difference in display length need not be a difference in inference count.

New to topics? Read the docs here!