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

Use the disjunction elimination rule on the outer disjunction. In its left branch, assume $P\vee Q$ and apply the disjunction elimination rule again: from a case assumption $P$, the disjunction introduction rule gives $P\vee R$; from a case assumption $Q$, the premise $Q\to R$ and the modus ponens rule give $R$, then the disjunction introduction rule gives $P\vee R$. Discharging those two inner case assumptions yields $P\vee R$ under the left outer branch.

In the right outer branch, assume $R\vee S$. A case assumption $R$ gives $P\vee R$ by the disjunction introduction rule. A case assumption $S$, together with the premise $\neg S$, gives $\perp$ by the negation elimination rule, and then $P\vee R$ by logical falsity elimination rule. Discharge these inner case assumptions with the disjunction elimination rule.

Both outer branches now have the same conclusion. Discharge the two outer case assumptions with the disjunction elimination rule to obtain $P\vee R$ under exactly the stated premises.