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

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]