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

Choose arbitrary fresh variables $y,x,z$ and assume $H=((x=y\vee y=z)\wedge P(y))$ under label $a$. The conjunction elimination rule gives $x=y\vee y=z$ and $P(y)$. Apply the disjunction elimination rule to the equality disjunction.

In the case $x=y$, the supplied symmetry rule gives $y=x$, and the equality elimination rule applied to $P(y)$ gives $P(x)$. Disjunction introduction rule gives $P(x)\vee P(z)$. In the case $y=z$, equality elimination rule applied directly to $P(y)$ gives $P(z)$; the other disjunction introduction rule gives the same conclusion $P(x)\vee P(z)$. Discharge the two equality case assumptions by disjunction elimination rule.

Discharge $a$ with the implication introduction rule. There are now no undischarged assumptions. Use the universal quantifier introduction rule successively for $z$, then $x$, then $y$, yieldingFreshness holds at every generalization because the sole temporary assumption has already been discharged; the arbitrary variables are not tied to any premise.

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.