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

Let $u$ be fresh, not free in any of the three universal premises. Universal quantifier elimination rule gives $\neg P(u)\vee R(c,u)$, $Q(u)\to R(c,u)$ and $P(u)\vee Q(u)$. Apply disjunction elimination rule to the last formula.

In the $P(u)$ branch, apply disjunction elimination rule to $\neg P(u)\vee R(c,u)$. Its $\neg P(u)$ case contradicts $P(u)$ by negation elimination rule, and logical falsity elimination rule then gives $R(c,u)$. Its $R(c,u)$ case already gives that conclusion. Discharge those two inner case assumptions to obtain $R(c,u)$ under the outer $P(u)$ assumption. In the outer $Q(u)$ branch, the modus ponens rule applied to $Q(u)\to R(c,u)$ gives $R(c,u)$ directly.

Discharge the two outer case assumptions by disjunction elimination rule. The conclusion $R(c,u)$ now depends only on the universal premises, in which $u$ is not free. Universal quantifier introduction rule therefore gives $\forall xR(c,x)$. All case assumptions have been discharged, and the argument requires no classical reductio ad absurdum.