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 \b[$\exists x\,Q(x)$]. Substitution of a constant is capture-free here, so both quantifier side conditions hold.

Solution

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

 Solution (source code)