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?
Best Answer
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.