How can universal quantifier manipulation rules be made redundant by the generalization rule (metatheorem)?

Question

On the Wikipedia page for Hilbert style axioms, in the "Logical axioms" section, it gives the axioms to manipulate universal quantifiers :

$Q5. \forall x(\phi)\rightarrow \phi[x:=t] $

$Q6. \forall x(\phi \rightarrow \psi)\rightarrow (\forall x(\phi) \rightarrow \forall x (\psi) )$

$Q7. \phi\rightarrow \forall x (\phi) $ where x is not free in $\phi$

and then says :

Universal quantification is often given an alternative axiomatisation using an extra rule of generalisation (see the section on Metatheorems), in which case the rules Q5 and Q6 are redundant.

As given in the Metatheorems section, this extra rule of generalisation seems to be :

Generalization : If $\Gamma \vdash \phi$ and $x$ does not occur free in any formula of $\Gamma$ then $\Gamma \vdash \forall x \phi$

But how are axioms Q5 and Q6 made redundant by this rule? I'm not sure I see how they follow from it and the other axioms?

Answer 1

I think that it must be a typo in your source ...

With $\forall$ as primitive, in presence of modus ponens, axiom $Q5$ licenses the derived rule $\forall$E (or UI) :

from $\forall x \varphi$, derive $\varphi(t/x)$,

with Generalization acting as $\forall$I.

Thus, I think that we cannot avoid $Q5$.

---

A well-known Hilbert-style proof system for classical quantification theory is in Elliott Mendelson, Introduction to mathematical logic (4th ed - 1997), with MP and Gen as rules of inference [see page 69].

The axioms are $Q5$ and $Q'6$ [named : $(A4)$ and $(A5)$ respectively] , where :

$Q'6.\ \ ∀x(\varphi → \psi) → (\varphi → ∀x\psi) \ \ $, provided that $x \notin FV(\varphi)$.

We can see Exercises 2.74 [page 102 - hint at page 392] :

Prove the independence of axioms $(A1)-(A7)$ in any predicate calculus with equality.

A proof (for a different set of quantifier axioms) of the independence of $Q5$ is in :

David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (2nd ed - 1937), page 90.

---

In Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 112, we can see an axiom system based on $Q5, Q6$ and $Q7$ [called axiom 2, axiom 3 and axiom 4, respectively], with Modus Ponens as only rule of inference.

The Generalization Th is proved [see page 117] using axioms 3 and 4.

Assuming Gen Th as a primitive Generalization rule we can prove (in presence of $Q5$) both $Q6$ and $Q7$.

For

$Q7 : \quad \varphi → ∀x(\varphi), \quad x \notin FV(\varphi)$

1) $\varphi \vdash \varphi$

2) $\varphi \vdash \forall x \varphi$ --- by Gen : $x$ not free in assumption $\varphi$

3) $\vdash \varphi \rightarrow \forall x \varphi$ --- by Deduction Th.

---

For

$Q6 : \quad ∀x(\varphi → \psi) → (∀x \varphi → ∀x \psi)$

1) $∀x(\varphi → \psi) \rightarrow (\varphi → \psi)$ --- $Q5$

2) $\forall x \varphi → \varphi$ --- $Q5$

3) $∀x(\varphi → \psi)$ --- assumed [a]

4) $∀x\varphi$ --- assumed [b]

5) $\varphi → \psi$ --- from 1) and 3) by MP

6) $\varphi$ --- from 2) and 4) by MP

7) $\psi$ --- from 5) and 6) by MP

8) $\forall x \psi$ --- from 7) by Gen : $x$ is not free in assumptions [a] and [b]

9) $∀x\varphi \rightarrow \forall x \psi$ --- from 4) and 8) by Deduction Th

10) $∀x(\varphi → \psi) \rightarrow (∀x\varphi \rightarrow \forall x \psi)$ --- from 3) and 9) by Deduction Th.