Why can't we have generalization as an axiom in Hilbert style predicate logic?

Question

I am working through Raymond Smullyan's Gödel's incompleteness theorems. He works with a logical framework due to Kalish, Montague, given by the axioms

and, of course, the Peano axioms. The system has two inference rules:

Now, I am wondering why it is necessary to have Generalisation as an inference rule, and not possible to replace $L_5$ by "$F \supset \forall v_i F(v_i)$" without any restriction and just have Modus Ponens as the only inference rule.

I guess there is a good reason for that. Which?

Answer 1

Suppose you had an axiom schema such as you suggest:

$$\vdash F(v)\rightarrow (\forall v)\,F(v)$$

By change of free variable $v$ in the antecedent and applying the generalization inference rule, you can infer the following:

$$\vdash (\forall w)\,(F(w)\rightarrow (\forall v)\,F(v)),$$

and from that, the equivalent formula

$$\vdash (\exists w)\,F(w)\rightarrow (\forall v)\,F(v). $$

But this last formula is not valid (except in one-element models) — an instance of it is “if something equals $0$, then everything equals $0$”.

---

Note: The change of variable is just for clarity; it's not really necessary.

Answer 2

Let us see how Smullyan construes the notion of a proof (p. 30):

Hence, if a formula $F$ occurs as a line by itself in the derivation, it is necessarily a valid formula and it can be generalised by taking its universal closure (whether the variable $v_i$ occurs in $F$ or not, with no restriction on $v_i$):

$\vdots$

$F$

$\vdots$

$\forall v_{i}F(v_i)$

As for the case of modus ponens, assuming that $F$ occurs as a line by itself in the derivation again, a line in which $F\rightarrow\forall v_{i}F(v_i)$ stands by itself has to have been derived:

$\vdots$

$F$

$\vdots$

$F\rightarrow\forall v_{i}F(v_i)$

$\vdots$

$\forall v_{i}F(v_i)$

Consequently, we see not that the rule of modus ponens renders the rule of generalisation idle, on the contrary, for the case of universal closure, the rule of generalisation renders the rule of modens ponens idle.

Then, what if $F\rightarrow\forall v_{i}F(v_i)$ had no restriction? Consider a formula $F$ in which the variable $v_{i}$ occurs free (since the statement of the axiom is for any formula), then it would be illegitimately captured by the universal quantifier.