= Solution
Let $u$ be fresh, not free in any of the three universal premises. <Universal quantifier elimination rule> gives $\neg P(u)\lor R(c,u)$, $Q(u)\to R(c,u)$ and $P(u)\lor Q(u)$. Apply <disjunction elimination rule> to the last formula.
In the $P(u)$ branch, apply <disjunction elimination rule> to $\neg P(u)\lor 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 \b[$\forall x\,R(c,x)$]. All case assumptions have been discharged, and the argument requires no classical <reductio ad absurdum>.
Back to article page
