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 / i

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.