0

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

According to Enderton p.121, it suffices to show that:

$\{\forall x(\alpha\rightarrow\beta),\alpha\}\vdash\beta$

For then, Enderton suggests, we can derive the former via generalization and deduction theorems.

But I don't understand this. For one the one hand, from the deduction theorem we can derive:

$\{\forall x(\alpha\rightarrow\beta)\}\vdash\alpha\rightarrow\beta$

But an application of the generalization theorem to the RHS of this won't yield our target theorem.

On the other hand, we cannot apply the generalization theorem to $\{\forall x(\alpha\rightarrow\beta),\alpha\}\vdash\beta$ to get:

$\{\forall x(\alpha\rightarrow\beta),\alpha\}\vdash\forall x\beta$

Because we don't know if $x$ occurs free in $\alpha$.

Any and all help is much appreciated!

beachtrees
  • 209

1 Answers1

2

On my 2nd edition version page.121 of Enderton for this EXAMPLE (Q2A), the author explicitly assumes x does not occur free in α:

EXAMPLE (Q2A). If x does not occur free in α, then $$\vdash (α → ∀ x β) ↔ ∀ x(α → β)$$

So for your concerned actual backward direction, you're right that it suffices (by the deduction and generalization theorems) to show that $\{∀ x(α → β), α\} \vdash β$ which is easy to prove by 2 rules (UI+MP). Then you can invoke its generalization theorem on page.117 to finish this backward direction.

cinch
  • 1,648
  • 1
  • 4
  • 12