In Enderton's logic [page $120$], he says:

Assume we wish to prove $\Gamma\vdash\phi.$ where $\phi$ is $\forall x\psi$. If $x$ does not occur free in $\Gamma$, then it will suffice to show $\Gamma\vdash \psi$. Even if $x$ should occur free in $\Gamma$, the difficulty can be circumvented. There will always be a variable $y$ such that $\Gamma\vdash\forall y\psi^x_y$ and $\forall y\psi^x_y\vdash\forall x\psi.$

Could anyone provide an example for the process? I face difficulites on seeing how could this be applied. I know how to show the part $\forall y\psi^x_y\vdash\forall x\psi$ given that $y$ does not occur in $\psi$ using re-placement lemma and group axiom $2$ in his system. But the first part is the one I can't see how it's done.

Any clarification, please?

  • $\begingroup$ I'm perplexed ... The only way to make sense of Enderon's statement, is to suppose that $x \notin FV(\phi)$, in which case I do not see any "benefit" from quantifying $\forall x \phi$. $\endgroup$ – Mauro ALLEGRANZA Feb 3 '15 at 16:31

Frankly speaking, I'm in trouble with Enderton's statement ...

The argument regards a derivation :

$\Gamma \vdash \psi$

where the fact that $x \in FV(\Gamma)$ prevents us from applying the Generalization Th.

Consider the following "trivial" proof in f-o arithmetic [based on Peano's axiom] :

1) $x=0$

2) $x+0=x$ --- from axiom $\forall x(x+0=x)$, with Ax.2 and modus ponens

3) $S(x+0)=S(x)$ --- from 2) and Ax.6 by modus ponens

4) $S(x+0)=x+S(0)$ --- from axiom $\forall x(S(x+y)=x+S(y))$, with Ax.2 and modus ponens

5) $S(x)=x+S(0)$ --- from 3) and 4) and equality.

The derivation of $\Gamma \vdash S(x)=x+S(0)$ is correct, and we are intuitively licensed to assert that : $\forall x[S(x)=x+S(0)]$, but we cannot derive it by generalization because $(x=0) \in \Gamma$ and thus : $x \in FV(\Gamma)$.

The only way I can imagine to "restore" it is to change all occurrences of $x$ with $y$ [or any new variable not occurring in the previous proof] in the applications of Ax.2. This does not affect the soundness of the axiom and we will end with :

5') $S(y)=y+S(0)$.

Now we have $y \notin FV(\Gamma)$, and we may use Gen Th to conclude with :

6) $\forall y[S(y)=y+S(0)]$.

Of course, in order to have the above result, we must not perform the substitution :


But, in general, we are not licensed to do so, because [review the semantical specifications, page 88] we want "sound" arguments, i.e. we expect that $\Gamma \vDash \varphi$, and :

$\Gamma$ logically implies $\varphi$, written $\Gamma \vDash \varphi$, iff for every structure $\mathfrak A$ for the language and every function $s : Var \to |\mathfrak A|$ such that $\mathfrak A$ satisfies every member of $\Gamma$ with $s$, $\mathfrak A$ also satisfies $\varphi$ with $s$.

In order to understand this "tricky point", consider instead this new "ultra-trivial" proof :

1) $x=0$

2) $S(x)=S(0)$

In this case, we do not want to assert : $\forall x [S(x)=S(0)]$ (nor : $\forall y [S(y)=S(0)]$) ! because the conclusion is licensed only for an (assignment) function $s$ such that $s(x)=0$. In this case, we cannot replace $x$ with $y$ in the conclusion only, because in this way we are nor more able to derive it from the assumptions $\Gamma$.

I hope it helps ...

Having derived :

$\Gamma \vdash \forall y \psi^{x}_{y}$ --- (a),

the second step in the proof is to show that :

$\forall y \psi^{x}_{y} \vdash \forall x \psi$.

To do this, we need Axiom 2 [see page 112] : $\forall y \alpha \rightarrow \alpha^{y}_{t}$.

With $\psi^{x}_{y}$ in place of $\alpha$ and $x$ in place of $t$, we have as $\alpha^{y}_{t}$ the result $(\psi^{x}_{y})^{y}_{x}$ , i.e. $\psi$.

The proof needs a formal verification through Re-replacement lemma.

Having verified this, we have that : $\vdash \forall y \psi^{x}_{y} \rightarrow \psi$.

Then the following generalization is also an axiom [see page 112] :

$\vdash \forall x (\forall y \psi^{x}_{y} \rightarrow \psi )$.

By Axiom 4 ($x$ is not free in $\forall y \psi^{x}_{y}$), we have :

$\vdash \forall y \psi^{x}_{y} \rightarrow \forall x \psi$.

Thus, from (a) above, we conclude with :

$\Gamma \vdash \forall x \psi$.

Last edition

I think that a similar approach can be derived from the Example in Enderton, page 123.

Consider the following proof of $∀x(Pz → Qz), ∀zPz \vdash \forall yQy$ :

1) $∀x(Pz → Qz)$ --- premise

2) $∀zPz$ --- premise

3) $Py → Qy$ --- from 1) and Ax.1 by mp

4) $Py$ --- from 2) and Ax.1 by mp

5) $Qy$ --- from 3) and 4) by mp

6) $\forall y Qy$ --- from 5) by Gen Th.

If in the above proof we add to the set $\Gamma$ of premises, the new formula $Ry$, let $\Gamma' = \Gamma \cup \{ Ry \}$, we are no longer licensed to assert : $\Gamma' \vdash \forall yQy$.

I think that we can take benefit of Enderton's consideration in the said Example in the following way.

Modify the above proof of $\Gamma \vdash Qy$ into a proof of $\Gamma \vdash Qc$; now we can "add" the extra-premise $Ry$ and we have $\Gamma' \vdash Qc$.

Then we choose a new variable $z$ not occurring into $\Gamma', Qc$ and we can modify the proof to get a new one :

$\Gamma^c_z, Ry \vdash Q^c_z$.

Now we can apply Gen Th to get :

$\Gamma^c_z, Ry \vdash \forall zQz$.

  • $\begingroup$ We start with $\Gamma\vdash \psi$ and choose a constant symbol $c$ that does not occur in $\Gamma$ and substitute it for $x$ in $\psi$ to get $\psi^x_c$, Now, how do we know that $\Gamma\vdash\psi^x_c$ "we need to know this to apply generalization theorem on constants"? $\endgroup$ – Fawzy Hegab Feb 3 '15 at 6:52
  • $\begingroup$ I've already read it some time ago. But as I wasn't thinking about this question, I didn't relate the proof to the question directly. Thank you for pointing this out (and of course, for your detailed answer) $\endgroup$ – Fawzy Hegab Feb 3 '15 at 7:51
  • $\begingroup$ I've posted a concrete example for the idea "with variables instead of constants", Could you please check if the logic is correct? $\endgroup$ – Fawzy Hegab Feb 3 '15 at 8:06

For example, To show that $\forall x\forall yPxy\vdash\forall y\forall xPyx$:

We can't use generalization theorem directly so we employ another variable $s$ as follows:

1- $\forall x\forall yPxy\vdash\forall yPsy$ "Ax$2$"

2- $\forall yPsy\vdash Psx$ "Ax$2$"

3- $\forall x\forall yPxy\vdash Psx$ "from 1,2 usingtransitivity of modes ponens"

4- $\forall x\forall yPxy\vdash \forall xPsx$ "from 3 using Generalization theorem"

5- $\forall x\forall yPxy\vdash \forall s \forall xPsx$ "from 4 using Genenralization theorem"

6- $\forall s \forall xPsx\vdash \forall y\forall xPyx$

7- $\forall x\forall yPxy\vdash\forall y\forall xPyx$ "from 5,6".

Here, We've used another varialbe $s$ to use generalization theorem.

  • $\begingroup$ This example does not fit, because the only assumption is $∀x∀yPxy$ with no free vars; you can prove it as : $∀x∀yPxy \vdash ∀yPzy \vdash Pzw \vdash ∀xPzx \vdash ∀y∀xPyx$. $\endgroup$ – Mauro ALLEGRANZA Feb 3 '15 at 8:34
  • $\begingroup$ @MauroALLEGRANZA, Ok, could you provide an example which fits? I will try to go through the process through an example. $\endgroup$ – Fawzy Hegab Feb 3 '15 at 10:31
  • $\begingroup$ Sorry ... I've drived you on the wrong track with my wrong application of the generalization on constant theorem. I've tried to revise my answer. $\endgroup$ – Mauro ALLEGRANZA Feb 4 '15 at 9:30

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.