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

In natural deduction, conjunction introduction combines derivations of $\varphi$ and $\psi$ under the available assumptions into $\varphi \wedge \psi$. Disjunction elimination takes $\varphi \vee \psi$ and two subproofs of the same conclusion $\kappa$, one assuming $\varphi$ and the other assuming $\psi$, and concludes $\kappa$. Implication introduction takes a subproof deriving $\psi$ from a temporary assumption $\varphi$, and concludes $\varphi \to \psi$.

The rectangular boxes mark the scopes of temporary assumptions. The disjunction elimination rule discharges its two case assumptions, while the implication introduction rule discharges the antecedent assumption. Other surrounding assumptions remain in force; intermediate results depending on the boxed assumptions cannot be exported arbitrarily. Schematically,Here the square brackets designate the assumptions discharged by the corresponding inference rule.

A common-context sequent version of the disjunction elimination rule isThe second and third premises record exactly the two boxed subproofs of the natural deduction presentation. Their additional case assumptions do not occur in the conclusion: that is assumption discharge. The surrounding context $\Gamma$ remains throughout. A formulation with different surrounding contexts is equivalent after retaining their union by weakening.

Read chained logical implications as right-associative. Use the following natural deduction derivation; indentation bars mark nested subproofs and the last column records rules and discharged line ranges:Each application of the implication introduction rule discharges only its matching temporary assumption. Thus

Use conjunction elimination to extract the three inputs, then apply the implication elimination rule three times:The implication introduction rule closes the only subproof, giving

Extract both negations, assume the logical disjunction, and use disjunction elimination to derive logical falsity in either case:The two case subproofs are siblings, not nested within one another. Therefore

Use negation introduction separately for each component, introducing the forbidden logical disjunction in each subproof:Both temporary assumptions have been discharged before the final conjunction introduction, so

In proof by contradiction, assume the negation of the desired conclusion and derive logical falsity; discharge that assumption and infer the desired conclusion. Its sequent rule isThis is a rule of classical propositional logic. It follows from the paper's negation introduction rule, which first yields $\neg \neg \varphi$, and double-negation elimination, which yields $\varphi$. This is stronger than merely deriving $\neg \varphi$ by showing that $\varphi$ leads to logical falsity.

Use proof by contradiction, expanding the final classical step explicitly into negation introduction followed by double-negation elimination. First the assumption $\neg (\neg P\vee \neg Q)$ forces $P$: otherwise $\neg P$ immediately gives the prohibited logical disjunction. It similarly forces $Q$. The formal natural deduction derivation isHenceThis direction of De Morgan's laws uses the classical rule supplied on the source rule sheet; it has not been silently treated as an available inference rule.