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

Apply the universal quantifier elimination rule to the universal premise with term $c$, obtaining $P(c)\leftrightarrow Q(c)$. The left biconditional elimination rule gives $P(c)\to Q(c)$. Use the premise $P(c)$ and the modus ponens rule to derive $Q(c)$. The existential quantifier introduction rule with witness $c$ yields $\exists xQ(x)$. Substitution of a constant is capture-free here, so both quantifier side conditions hold.

Temporarily assume $Q(c)$ under label $a$. The implication premise and the modus ponens rule yield $\forall x(P(x)\leftrightarrow P(c))$. Instantiate it at $c^{\prime }$ using the universal quantifier elimination rule, obtaining $P(c^{\prime })\leftrightarrow P(c)$. Its right biconditional elimination rule gives $P(c)\to P(c^{\prime })$.

Apply the modus ponens rule with the premise $P(c)$ to obtain $P(c^{\prime })$. Together with $\neg P(c^{\prime })$, negation elimination rule gives $\perp$. Discharge $a$ using the negation introduction rule to conclude $\neg Q(c)$. Nothing assumes that the two constant symbols denote different objects; if they denoted the same object, the stated premises would themselves already be inconsistent.

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.