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

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?

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.

• Gratitude. I should know better than to doubt an author so easily! – MuchToLearn Feb 9 at 21:47