= 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'$ using the <universal quantifier elimination rule>, obtaining $P(c')\leftrightarrow P(c)$. Its right <biconditional elimination rule> gives $P(c)\to P(c')$.
Apply the <modus ponens rule> with the premise $P(c)$ to obtain $P(c')$. Together with $\neg P(c')$, <negation elimination rule> gives $\bot$. Discharge $a$ using the <negation introduction rule> to conclude \b[$\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.
Back to article page
