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!


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.

  • $\begingroup$ B) It is odd, I wish the authors would've mentioned anything like this in the book. As I mentioned to Mauro who also wrote an answer, the substitution could be done as well with $[x/x]$, no confusion needed! $\endgroup$ – Garth Marenghi May 12 '14 at 19:47
  • $\begingroup$ Yes, I think, you are right. However, it is not standard to use the same variable in a bounded part and also free in the same formula. $\endgroup$ – Berci May 12 '14 at 19:49

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


$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$).

  • 1
    $\begingroup$ If you have $Rxy \wedge \exists z Sz$, why not $\exists x (Rxy \wedge \exists z Sz)$? Why must it be $\forall x (Rxy \wedge \exists z Sz)$? There is nothing to my knowledge that lets my say "this applies to all" x's. $\endgroup$ – Garth Marenghi May 12 '14 at 19:35
  • 1
    $\begingroup$ About 3) I understand, but to me it is not clear as to why it must be so that $x$ must be changed into $y$. The proof could just as well be done without doing this: $[x/x]$. Even stranger, from 5 to 6, it is changed back again to $x$! $\endgroup$ – Garth Marenghi May 12 '14 at 19:39
  • $\begingroup$ @GarthMarenghi - "There is nothing to my knowledge that lets my say "this applies to all" x's."... It depends on you: on what you are saying... If you want to express : "all balls are black", you need : "for all x, if Ball(x), then Black(x)". If you want to say : "there is a white ball", you need : "exists an x such that Ball(x) and White(x)". $\endgroup$ – Mauro ALLEGRANZA May 12 '14 at 19:39
  • $\begingroup$ @GarthMarenghi - you are right - For all x means that you can "instantiate" it with a "name" (a term) whatever; thus, $y$ and $x$ and ... are all good. If you have found the proof into a textbook, I think that the author thinks that it is "more easy" to grasp if he cange the variable ... It seems not so. $\endgroup$ – Mauro ALLEGRANZA May 12 '14 at 19:41
  • $\begingroup$ Right, but universal instantiation says this: From $\varphi$ follows $\forall x \varphi$. The choice doesn't seem up to me, it is something that is ready for use. $\endgroup$ – Garth Marenghi May 12 '14 at 19:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.