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

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


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.


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.