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

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.