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 / a / ii / Solution

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.