What is the purpose of universal quantifier?

Question

The universal generalization rule of predicate logic says that whenever formula M(x) is valid for its free variable x, we can prefix it with the universal quantifier,

M(x) ⊢ ∀x M(x).

But it seems then makes no sense. Why do you introduce a notion that does not mean anything new?

Answer 1

Basically, we need quantifiers not so much for making inferences but for having enough expressive "capability" in our language.

For simplicity, I assume the context of classical first-order logic, where the existential quantifier $\exists$ can be defined as an abbreviation for $\lnot \forall \lnot$.

If we are working into formalized arithmetic (e.g.first-order logic with Peano's Axioms), we may stay with the convention that free variables are implicitly universally quantified.

So, the Axiom about the successor function :

$x = y \rightarrow S(x) = S(y)$

can be interpreted as $\forall x \forall y ( ...)$, like in algebra when we write : $(x+y)^2 = x^2 + 2xy +y^2$.

The problem is that not all the relevant "facts" can be rightly expressed with universal quantifiers upfront.

Take the formula : $x = 0$; if we stay with the above convention, its meaning must be : "all numbers are equal to $0$", that is false.

If we negate it, we get $\lnot x = 0$, which, following the convention, must be read as : "all number are different from $0$". But this is false also !

We need a sign for "restricting" the context (the scope) of the quantifier (this wonderful discovery was made by Frege) in order to have :

$\forall x (x = 0)$

Now, its negation will be :

$\lnot \forall x (x = 0)$

and this time we have the intended meaning : "not all numbers are equal to $0$", that is true.

This example is taken form S.C.Kleene, Introduction to Metamathematics (1952).

Answer 2

$M(x)$ doesn't strictly have a truth value; $\forall x.M(x)$ does. So, different beasts. Not to mention "$T\vdash M(x)$" is not a sentence in the language, while again, "$\forall x.M(x)$" is.

The universal generalization rule connects a piece of metatheory ("for any variable '$x$', '$M(x)$' is provable", or some such), with a statement in the theory itself. The distinction is a subtle one, and won't often trip one up in everyday logic use, but when studying some truly abstract reaches of logic like model theory, you can end up in some tangled fallacies if you don't keep theory and metatheory apart.