How to prove that $\Gamma\vdash\forall x\psi$ if $x$ occurs free in $\Gamma$, via generalization theorem?

Question

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?

Answer 1

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 :

$(x=0)^x_y$.

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

Answer 2

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.