A 7-formula deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$. Enderton logic page 123.

Question

Enderton claims that it is not hard to show that a deduction for $\{\forall x (Px \to Qx), \forall z P z\} \vdash Qc$ exists, and furthermore that it consists of only seven formulas. I was able to find such a deduction but considering instead the set of hypotheses $\Gamma = \{\forall x (Px \rightarrow Qx), \forall x P x\}$. Otherwise, getting $\forall x P x$ from $\forall z P z$ takes me about 6 formulas by mimicking the proof of the Generalization Theorem. Here's a depiction of the 7-formula deduction I arrived at:

1. $\forall x(Px \to Qx) \to (\forall x Px \to \forall x Qx)$. In axiom group 3.
2. $\forall x (Px \to Qx)$. In $\Gamma$.
3. $\forall x Px \to \forall x Qx$. 1,2; Modus Ponens.
4. $\forall x Px$. In $\Gamma$.
5. $\forall x Qx$. 3, 4; Modus Ponens.
6. $\forall x Qx \to Qx_{c}^{x}$. In axiom group 2 (substitution).
7. $Qc$. 5,6; Modus Ponens.

Could anybody confirm that what Enderton claims cannot be done in 7 formulas/steps, or provide such a deduction?

Answer 1

A different derivation ...

1) $∀x(Px → Qx)$ --- premise

2) $∀zPz$ --- premise

3) $∀x(Px → Qx) \to (Pc → Qc)$ --- Axiom 2

4) $∀zPz \to Pc$ --- Axiom 2

5) $Pc → Qc$ --- 1) and 3) by MP

6) $Pc$ --- 2) and 4) by MP

7) $Qc$ --- 5) and 6) by MP.