I'm reading Gödel's famous paper “On Formally Undecidable Propositions of PM” and at one point he gives the following definition:
$c$ is defined to be the immediate consequence of $a$ and $b$ if $a$ is the formula $\neg b\lor c$ or alternatively if $c$ is the formula $\forall v. a$
The first case is derived from modus ponens and it is also explained in this answer.
My question is:
- What is the meaning of using "universal generalization" as a deduction rule? Is it something useful just from a formal standpoint, to make logical proofs easier, or is there a deeper reason for it?
Correct me if I'm wrong, but it seems to me that in conjunction with the other axiom $$\left(\forall v.a\right) \rightarrow \mathrm{sub}\; a\left( \begin{array}{c} v \\ c\end{array}\right)$$ where $c$ is "suitably chosen", the generalization rule implies that formulas with free variables are allowed to be true, and in fact they have the same truth value as their generalization.
As an example of this, the formula that can be synthesized in $$x_1=x_1$$ should be logically equivalent to $$\forall x_1 .\: x_1=x_1$$ in Gödel's system.
So my second complementary part of the question is:
- What would happen if we were to remove this deduction rule? Could everything work regardless without it with some adjustments? Or would it be much more complicated that it seems? And why are formulas with free variables allowed to be true in the first place?
Formulas with free variables would still exist but will not allowed to be true, I suppose. And I assume you would need other axioms to account for things like deriving $\forall v.\: a\rightarrow c$ from $\forall v.\: a\rightarrow b$ and $\forall v.\: b\rightarrow c$ . Is that really doable in some way or not?
Summing up, I'm asking why universal generalization is used as a deduction rule and whether it is possible to remove it or not in Gödel's system.