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

The implication introduction rule opens a subproof under a temporary assumption $\varphi$, derives $\psi$, then performs assumption discharge to conclude $\varphi \to \psi$. The negation introduction rule instead derives logical falsity $\perp$ under a temporary assumption $\varphi$, discharges it, and concludes $\neg \varphi$:The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions $\Gamma$ stay in force.

Write $H=(P\wedge Q)\vee (P\wedge R)$ and $K=P\wedge (Q\vee R)$. In the following natural deduction derivations, brackets name temporary assumptions, and cited ranges specify the subproofs discharged. The abbreviations $\wedge E,\wedge I,\vee E,\vee I$ 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 $P$ by cases, then obtain $Q\vee R$ 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 $\wedge E$, two $\vee I$, two $\wedge I$ and one $\vee E$; the second has four $\wedge E$, two $\vee I$, one $\wedge I$ and two $\vee E$. 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.

The classical proof by contradiction rule, also called reductio ad absurdum, iswith assumption discharge of the displayed $\neg \varphi$. It differs from the negation introduction rule by concluding $\varphi$ from a contradictory assumption of its negation.

To derive double-negation elimination using this rule, start with $\neg \neg \varphi$, assume $\neg \varphi$, and apply the negation elimination rule to those two formulas:No double-negation elimination occurs inside this derivation, so the argument is not circular.

Put $F=(\neg P)\to Q$ and $G=(\neg P)\to \neg Q$. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule: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.

First obtain $A$ by a double-negation elimination, then obtain $\neg B$ by the negation introduction rule. The following natural deduction proof uses only the printed rules, with $\perp E$ denoting the logical falsity elimination rule: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.