How to better understand " x occurs free in a wff " in first order logic?

Question

On page 121 of Herbert Enderton's A Mathematical Introduction to Logic, the author gives a proof of the following example :

If x does not occur free in $\alpha$, then $$ \vdash ( \alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha\rightarrow\beta) $$

To prove this, it suffices to show that $$ \vdash ( \alpha \rightarrow \forall x \beta) \rightarrow\forall x(\alpha\rightarrow\beta) $$ and $$ \vdash ( \alpha \rightarrow \forall x \beta) \leftarrow \forall x(\alpha\rightarrow\beta) $$

For the first case, it suffices to show that ( by the deduction and generalization theorem ) $$ \{(\alpha \rightarrow \beta),\alpha\}\vdash\beta $$ But this is easy, since $\forall x \beta \rightarrow \beta $ is an axiom.

I try to verify that.

Step 1, By Deduction Theorem, $$ ( \alpha \rightarrow \forall x \beta) \vdash \forall x(\alpha\rightarrow\beta) $$ Step 2, By Generalization Theorem, $$ ( \alpha \rightarrow \forall x \beta) \vdash \alpha\rightarrow\beta $$ Step 3, By Deduction Theorem, $$ \{(\alpha \rightarrow \beta),\alpha\}\vdash\beta $$

What baffle me :

1. Is Step 2 plausible? We don't know if $\beta$ is free or not...

2. Given an axiom of Enderton's system :

   $ \forall x \alpha \rightarrow \alpha_{x}^{t} $ , where $t$ is substitutable for $x$ in $\alpha$

   , how can I make sense of $\forall x \beta \rightarrow \beta $ ?

I ask this question mainly because I'm deeply baffled with the idea of " variable occurs free ". Can anyone translate $\vdash ( \alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha\rightarrow\beta)$ into Englsih ( or give an simple algebra example ) and compare the two cases where $\alpha $ occurs free and not occurs free? I believe it will help me understand why Enderton's proof is plausible.

Thank you ( :

Answer 1

For :

$\vdash (α→∀xβ)→∀x(α→β)$

the proof is :

1) $(α→∀xβ)$ --- assumed

2) $\alpha$ --- assumed

3) $∀xβ$ --- by modus ponens

4) $\beta$ --- from 3) by Ax.2 : $∀x \varphi→\varphi^x_t$, where $t$ is substitutable for $x$ in $\varphi$; we apply it with $\beta$ as $\varphi$ and $x$ as $t$.

5) $\alpha \rightarrow \beta$ --- from 2) and 4) by Deduction Th

6) $\forall x (\alpha \rightarrow \beta)$ --- from 5) by GENERALIZATION THEOREM [page 117] : If $\Gamma \vdash \varphi$ and $x$ do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.

In this step, $\Gamma = \{ α→∀xβ \}$; thus in order to apply Gen Th, we have to satisfy the proviso : $x$ not free in it. This requires that $x \notin FV(\alpha)$.

The theorem follows applying Deduction Th to 1)-6):

$\vdash (α→∀xβ)→∀x(α→β)$.

---

For :

$\vdash ∀x(α→β) \rightarrow (α→∀xβ)$

the proof is :

1) $∀x(α→β)$ --- assumed

2) $α→β$ from 1) by Ax.2, with $α→β$ as $\varphi$ and $x$ as $t$.

3) $\alpha$ --- assumed

4) $\beta$ --- by modus ponens

5) $\forall x \beta$ --- from 4) by GENERALIZATION THEOREM. In this step, $\Gamma = \{ ∀x(α→β), α \}$; thus, in order to apply it, we need : $x \notin FV(\alpha$)

6) $\alpha \rightarrow \forall x \beta$ --- from 3)-5) by Deduction Th.

The theorem follows applying Deduction Th to 1)-6):

$\vdash ∀x(α→β) \rightarrow (α→∀xβ)$.

---

---

Why we need the proviso ?

Consider :

$(x = 0) \rightarrow (x = 0)$

it is a (first-order) instance of the tautology $A \rightarrow A$; thus, by Ax.1, its generalization :

$\forall x((x = 0) \rightarrow (x = 0))$

is an axiom of first-order logic, and thus a valid formula.

Consider now :

$(x = 0) \rightarrow \forall x (x = 0)$;

if we "forget" the proviso, this formula is equivalent to previous one; thus it must be valid.

But it is not; to show it, we apply modus ponens to get :

$(x = 0) \vDash \forall x (x = 0)$.

Consider the definition [page 88] of Logical Implication :

Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\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$.

and consider the function $s$ such that $s(x)=0$.

With $|\mathfrak A| = \mathbb N$ and this $s$, we have that $(x = 0)$ is satisfied, while of course $\forall x (x = 0)$ is not (it is obviously false that all natural numbers are equal to $0$).

---

Consider now the example :

$(0=0) \rightarrow \forall x (x=0)$;

in this case the proviso is satisfied; thus, it must be equivalent to :

$\forall x ((0=0) \rightarrow (x=0))$.

This is verified in $\mathbb N$, where the two are both false.