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

Keep the four given premises in context and assume $P$ under label $a$. The modus ponens rule applied to the first two premises gives $Q\vee R$ and $\neg S$. Apply the disjunction elimination rule to $Q\vee R$ as follows.

Under a case assumption $Q$, the premise $Q\to S$ gives $S$ by the modus ponens rule. Together with $\neg S$, the negation elimination rule gives $\perp$, and the supplied logical falsity elimination rule gives $R$. Under the other case assumption $R$, the required conclusion $R$ is already available. Discharge both case assumptions with the disjunction elimination rule to conclude $R$.

Finally discharge $a$ with the implication introduction rule, giving $P\to R$. The premise $S\to Q$ is not needed: a derivation is permitted to leave a premise unused.