Not understanding universal generalisation, and proof that uses it

Question

From $\varphi$ follows $\forall x \varphi$.

E.g., universal generalizations of the formula $Rxy \wedge \exists z Sz$ can be $\forall x (Rxy \wedge \exists z Sz)$, $\forall x \forall y \forall u(Rxy \wedge \exists z Sz)$ etc.

I can't grasp why it is possible to do this, who says that in $\forall x (Rxy \wedge \exists z Sz)$ you just can say that it applies to all x's?

Then there is this proof:

Axiom schema's used in the proof:

1 $(\forall x (\varphi \rightarrow \psi))\rightarrow (\forall x \varphi \rightarrow \forall x \psi)$
2 $\varphi \rightarrow \forall x \varphi$
3 $\forall x \varphi \rightarrow [t/x]\varphi$

$\Sigma = \{Sa, \forall x (Sa \rightarrow Sx)\}$. Proof $\Sigma \vdash \forall x Sx$

1 $\Sigma \vdash Sa$
2 $\Sigma \vdash \forall x (Sa \rightarrow Sx)$
3 $\vdash \forall (Sa \rightarrow Sx) \rightarrow (Sa \rightarrow Sy)$ axiom 3, t = y
4 $\Sigma \vdash Sa \rightarrow Sy$
5 $\Sigma \vdash Sy$
6 $\Sigma \vdash \forall x Sx$

Why does $(Sa \rightarrow Sx)$ need to change to $(Sa \rightarrow Sy)$ in 3? And what and why is happening at step 5 and 6? From $Sy$ to $\forall x Sx$??

Thanks to Mauro and Berci; I wish I could upvote you both!

Answer 1

The point is that $x$ denotes a general indeterminant (and not a constant), so if you can derive a proof of a formula, using the indeterminant $x$ in it, then the same proof will work when $x$ is replaced by anything else throughout.

A) If we think about semantics, i.e. the meaning of these formulas, then we can assign values to the variables, and a formula is said to be valid in an interpretation context ('model') if it is satisfied with respect to all possible evaluation of the variables.

This leads to the rule of universal generalisation in formal logic: $\phi(x,y)$ is regarded valid iff $\forall x,y:\phi(x,y)$ holds.

B) In step 3 we applied axiom 3 for $\varphi=\ (Sa\to Sx)$ and $t=y$, i.e. we substitute $y$ in place of $x$ in $\varphi$ (that is $[y/x]\varphi$).

The meaning of axiom 3 is that if a formula $\varphi$ holds for all $x$, then it can be specialized to anything else: whatever we write in place of $x$, the formula will be true.

From step 5 to step 6 we simply apply the generalization rule, which is axiom 2, used with variable $y$.
Well, yes, we would obtain $\forall y Sy$ by that. If we want to strictly continue to get it with $x$, apply axioms 3 and 2 again:

$\,$7. $\Sigma\vdash Sx $ by axiom 3. for $\forall y\,Sy$.
$\,$8. $\Sigma\vdash \forall x\,Sx$ by axiom 2.

Answer 2

1) Quantifying variables not contained in the formula which is in the scope of the quantifier has no effect; see your example :

$∀x∀y∀u(Rxy∧∃zSz)$;

$u$ is not into $Rxy$ nor into $\exists z Sz$ : thus, it has no effect.

2) who says that in $∀x(Rxy∧∃zSz)$ you just can say that it applies to all $x$'s?

This question is not clear to me; the syntax of first-order logic "force us" to consider that the $x$ into the scope of a quantifier $\forall x$ must "range over" all the objects in the domain of the interpretation.

3) about your proof : in step 3, you apply Ax.3 : $∀xφ→[t/x]φ$. In the proof, we have that $\phi$ is $(Sa→Sx)$; thus $∀xφ$ is $∀x(Sa→Sx)$.

$(Sa→Sy)$ is $[y/x](Sa→Sx)$, where the variable $y$ is used as the term $t$.

Terms are : individual variables, like : $x,y,...$, individual constants, like $0$ in arithmetic), "complex terms", like $x+0$ in arithmetic.

In step 5, the proof uses modus ponens (or detachement : from $\phi$ and $\phi \rightarrow \psi$, infer $\psi$).

Thus, from 1) : $Sa$, and 4) : $Sa→Sy$, he deduces $Sy$.

Step 6 is derived form step 5 according to Ax.2 (called also Generalization rule : if $\vdash \phi$, then $\vdash \forall x \phi$).