1

On p. 111 (section 2.4) of Enderton's A Mathematical Introduction to Logic, immediately after the proof of the Generalization Theorem the following example is given

$$\forall x \forall y \alpha \vdash \forall y \forall x \alpha$$ without any explanation.

I cannot see right away how the Generalization Theorem can help here since that theorem allows us to add new quantifiers but here it seems we need some way of taking apart already existing quantifiers.

I would appreciate any help in understanding how this result (which of course must be true) serves as an example at this point in the book.

Jyotirmoy Bhattacharya
  • 5,518

1 Answers1

2

We start with :

$∀x∀yα$

then apply Ax-2 [$\forall x \alpha \rightarrow \alpha[x/t]$, with proviso that $t$ is substitutable for $x$ in $\alpha$, using $x$ itself as $t$], to get :

$∀yα$

then apply the axiom again to get :

$\alpha$.

Having derivet this, we apply Gen Th, due to the fact that $x$ does not occur free in any formula in $\Gamma$, where $\Gamma$ is $∀x∀yα$, and we derive :

$∀xα$

and again with $y$ :

$∀y∀xα$

to conclude that :

$∀x∀yα \vdash ∀y∀xα$.

The result shows that we may "interchange" adiacent (equal) quantifiers.

Mauro ALLEGRANZA
  • 94,169
  • Thanks. But isn't $\alpha$ in the third step different from the original $\alpha$ due to the substitutions? – Jyotirmoy Bhattacharya Jun 12 '14 at 14:11
  • 1
    No. We have two cases : (i) the "trivial" one. $x$ is not free in $\alpha$; the substitution performed with Ax-2 is "void" and nothing change. (ii) if $x$ is free in $\alpha$, i.e. we start with $\forall x \forall y \alpha(x,y)$, we can apply Ax-2 with a term $t$ whatever, provided that it is not "captured" by the quantifier $\forall y$: this is the role of the proviso : $t$ substitutable. We have to choose as $t$ $x$ itself. Thus we get : $\forall y \alpha(x,y)$, and the same for the second step. Thus, applying twice Gen Th we get the result without "altering" $\alpha$. – Mauro ALLEGRANZA Jun 12 '14 at 14:15