Past exam of the year 1 of the computer science course of the University of Oxford / 2013 / Digital systems, linear algebra, introduction to formal proof / 7

The conjunction introduction rule combines derivations of $\varphi$ and $\psi$ into a derivation of $\varphi \wedge \psi$. Both conclusions must be available under the current assumptions.

The disjunction elimination rule is reasoning by cases: from $\varphi \vee \psi$, a subproof deriving the same conclusion $\kappa$ under $\varphi$, and another subproof deriving $\kappa$ under $\psi$, conclude $\kappa$. It discharges the two case assumptions, not any surrounding premises.

The implication introduction rule derives $\varphi \to \psi$ by temporarily assuming $\varphi$ and deriving $\psi$; it then discharges that occurrence of the assumption $\varphi$.

ThusA conclusion inside a box cannot simply be reused outside it without an appropriate inference rule. Any other undischarged assumptions continue to constrain the result. These are exactly the rules printed in Figure 1.^[ref]

The following natural deduction tables record the active assumption lines explicitly. A rule may use an earlier line only while all of that line's assumptions remain available; assumption discharge closes the indicated case or hypothesis. The first proof makes the case split first, constructs the whole required logical conjunction in each case, and then closes the cases.

The second proof instead splits the goal first. It proves each required logical disjunction by a separate use of disjunction elimination, then applies conjunction introduction at the end.

The essential difference is the order of proof construction: the first shares one case split between both goals, whereas the second duplicates that split and combines the results outside the cases. Both use only the stated natural deduction rules, and both conclude

In proof by contradiction, assume the negation of a desired conclusion $A$, derive logical falsity, and discharge the assumption to infer $A$. A rule expressing this isHere the label $i$ identifies the assumption being discharged; any other open assumptions remain.

To derive this rule using the supplied rules, apply negation introduction to the subproof from $\neg A$ to $\perp$. This discharges $\neg A$ and yields $\neg \neg A$. Apply double-negation elimination to obtain $A$. Thus the extra rule is admissible because Figure 1 explicitly includes double-negation elimination.^[ref]

This is the classical form of proof by contradiction; simply deriving $\neg A$ from an assumption $A$ leading to logical falsity uses negation introduction alone.

Under the premise, assuming either disjunct would introduce the forbidden logical disjunction. Discharging those two assumptions gives the two separate negations, which can then be conjoined.

ThusThe redundant closing parenthesis printed after the conclusion on p. 8 does not alter the readable propositional formula.^[ref]

Temporarily deny the desired logical disjunction. If $\neg P$ held, it would introduce that very logical disjunction, producing logical falsity; double-negation elimination therefore gives $P$. The same argument gives $Q$, contradicting the premise. The complete natural deduction derivation is:

ConsequentlyThe uses of double-negation elimination are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of De Morgan's laws.