If a wff is simply atomic (e.g. $Pxy$) are $x$ and $y$ considered free in it?

Question

(Using First-Order Logic Hilbert System)

I found the following "solution" to $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$:

1. $\forall x \forall y Pxy \vdash \forall y Pzy$ (A2, MP)

2. $\forall y Pzy \vdash Pzx$ (A2, MP)

3. $\forall x \forall y Pxy \vdash Pzx$ (1,2)

4. $Pzx \vdash \forall x Pzx$ (GT)

5. $\forall x Pzx \vdash \forall z \forall x Pzx$ (GT)

6. $\forall x \forall y Pxy \vdash \forall z \forall x Pzx$ (3,4,5)

7. $\forall z \forall x Pzx \vdash \forall x Pyx$ (A2, MP)

8. $\forall x Pyx \vdash \forall y \forall x Pyx$ (GT)

9. $\forall x \forall y Pxy \vdash \forall y \forall x Pyx$ (6,7,8)

Where GT = Generalization Theorem, A2 = Substitution axiom, MP = Modus Ponens.

My problem is with line 4. How can you just throw a $\forall x$ in front of there? Doesn't the generalization theorem assume that $x$ is NOT free in the wff. Is $x$ not free in $Pzx$?

Here are all the axioms I can use:

• Tautologies

• $\forall x \alpha \rightarrow \alpha_t^x$, where $t$ is substitutable for $x$ in $\alpha$.

• $\forall x (\alpha \rightarrow \beta)\rightarrow(\forall x \alpha \rightarrow \forall x \beta)$

• $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$

And if the language includes equality,

• $x=x$
• $x=y \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is atomic and $\alpha'$ is obtained from $\alpha$ by replacing $x$ in zero or more places by $y$.

Answer 1

Of course, in an atomic formula $Pxy$, $x$ and $y$ are free.

As you says (correctly) you cannot do : $Pzx ⊢ ∀xPzx$; you have to apply it to Line 3 :

from $∀x∀yPxy ⊢ Pzx$, derive $∀x∀yPxy ⊢ \forall xPzx$.

The Generalization Theorem [see Enderton, page 117] says :

If $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

You can apply it to Line 3 because in it we have $\Gamma = \{ ∀x∀yPxy \}$ and $x$ is not free in it.

Thus, it works...

---

Note

In using : $\vdash$ in a derivation with annotations, it is a good practice to be consistent with the conventions :

• $\vdash \psi$ means that $\psi$ is theorem of the system, i.e. provable from the axioms

• $\varphi \vdash \psi$ means that $\psi$ is derivable from the assumption $\varphi$.

In your proof you are using it in an inconsistent way : in Line 4 you wrote to the left of $\vdash$ the formula from which you are deriving your conclusion (and written in this way, the step is illegal), while in other cases you correctly wrote to the left of $\vdash$ the assumptions from which the conclusion depends (see Line 3).

Your misunderstanding, I think, arise because you are "switching" from one way to the other.