logic
On page 99, A Mathematical Introduction to Logic, Herbert B. Enderton（2ed),
Show that if $x$ does not occur free in $α$, then $α \vDash ∀ x α$.
Added:This could be seen as a follow-up problem of this one. Frankly speaking, I'm totally confused between this problem and the answer to that problem.
Having the OP's question already received answers, I submit this "long" comment aimed at providing a proof using Enderton's axioms and modus ponens, which is the only rule of inference (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).
We have to prove (Q3A) [see Exercise 8, page 130] :
$\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.
First part : $\leftarrow$
(1) $\forall x \beta$ --- assumed
(2) $\beta_c^x$ --- from (1) by Ax.2 and mp, where the constant symbol $c$ does not occur in $\alpha, \beta$
(3) $\beta_c^x \rightarrow \alpha$ --- assumed
(4) $\alpha$ --- from (2) and (3) by mp
By COROLLARY 24H (RULE EI) [page 124], having proved $\forall x \beta, \beta_c^x \rightarrow \alpha \vdash \alpha$, where $c$ does not occur in $\beta$ nor in $\alpha$ (because $x \notin FV(\alpha)$), we have :
(5) $\forall x \beta, \exists (\beta \rightarrow \alpha) \vdash \alpha$
(6) $\exists (\beta \rightarrow \alpha) \vdash (\forall x \beta \rightarrow \alpha)$ --- from (5) by DT.
Second part : $\rightarrow$
(1) $\lnot \beta \vdash \beta \rightarrow \alpha$ --- by $\vDash_{TAUT} \lnot \phi \rightarrow (\phi \rightarrow \psi)$, assuming $\lnot \beta$
(2) $\forall x \beta \rightarrow \alpha$ --- assumed
(3) $\lnot \exists x (\beta \rightarrow \alpha)$ --- assumed
(4) $\exists x (\beta \rightarrow \alpha)$ --- from (1) by the "derived rule" : $\varphi_t^x \rightarrow \exists x \varphi$ [provable from Ax.2] and mp
Thus we have : $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$, from (1) and (4) and $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \lnot \exists x (\beta \rightarrow \alpha)$, from (1) and (3); we apply : COROLLARY 24E (REDUCTIO AD ABSURDUM) [page 119] and $\vDash_{TAUT} \lnot \lnot \phi \rightarrow \phi$ and mp to conclude with :
(5) $\lnot \exists x (\beta \rightarrow \alpha) \vdash \beta$
(6) $\forall x \beta$ --- from (5) by GENERALIZATION THEOREM [page 117] ($x$ is not free in assumptions (2), because $x \notin FV(\alpha$), and (3) and assumption (1) has been "discharged" in (5))
(7) $\alpha$ --- from (2) and (6) by mp
(8) $\beta \rightarrow \alpha$ --- From (7) and $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$ and mp
(9) $\exists x(\beta \rightarrow \alpha)$ --- from (8) by the "derived rule" in (4) above
We apply again COROLLARY 24E (REDUCTIO AD ABSURDUM) with : $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \lnot \exists x (\beta \rightarrow \alpha)$, and $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \exists x (\beta \rightarrow \alpha)$, from (2)-(9), and Double Negation to conclude with :
(10) $(\forall x \beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$.
Addendum
We add as an exercise the proof in Enderton's system of (Q2B) [see Exercise 8, page 130] :
$\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$.
First part : $\rightarrow$
(I've "streamlined" a little bit the "tautological" steps)
(1) $\alpha \rightarrow \exists x \beta$ --- assumed
(2) $\forall x \lnot (\alpha \rightarrow \beta)$ --- assumed
(3) $\alpha \land \lnot \beta$ --- from (2) by Taut
(4) $\lnot \beta$ --- from (3) by Taut
(5) $\forall x \lnot \beta$ --- by the Generalization Theorem [page 117], because $x$ is not free in assumptions (1) and (2)
(6) $\lnot \exists x \beta$ --- abbreviation
(7) $\alpha$ --- from (3) by Taut
(8) $\exists x \beta$ --- from (1) by mp.
Having derived the contradiction [with (6) and (8)], we apply Corollary 24E (Reductio ad Absurdum) [page 119] : if $\Gamma \cup \{ \varphi \}$ is inconsistent, then $\Gamma \vdash \lnot \varphi$, with $\Gamma = \{ \alpha \rightarrow \exists x \beta \}$, and $\varphi := \forall x \lnot (\alpha \rightarrow \beta)$.
Thus we may conclude :
(9) $\lnot \forall x \lnot (\alpha \rightarrow \beta)$
that is : $\alpha \rightarrow \exists x \beta \vdash \exists x (\alpha \rightarrow \beta)$.
Finally :
(A) $\vdash (\alpha \rightarrow \exists x \beta) \rightarrow \exists x (\alpha \rightarrow \beta)$ --- by Deduction Theorem.
Second part : $\leftarrow$
(1) $\alpha \rightarrow \beta[x/c]$ --- assumed, where $c$ is an individual constant
(2) $\lnot \beta[x/c] \rightarrow \lnot \alpha$ --- by Taut
(3) $\forall x \lnot \beta$ --- assumed
(4) $\lnot \beta[x/c]$ --- from Ax.2 and (3) by mp
(5) $\lnot \alpha$ --- form (2) and (4) by mp
(6) $\forall x \lnot \beta \rightarrow \lnot \alpha$ --- form (3) and (5) by Deduction Theorem
(7) $\alpha \rightarrow \lnot \forall x \lnot \beta$ --- by Taut
(8) $\alpha \rightarrow \exists x \beta$ --- abbreviation.
Now we apply Corollary 24H (Rule EI) : assume that the constant symbol $c$ does not occur in $\varphi, \psi$ or $\Gamma$, and that $\Gamma \cup \{ \varphi[x/c] \} \vdash \psi$; then $\Gamma, \exists x \varphi \vdash \psi$, where $\Gamma = \emptyset$, $\varphi[x/c] := \alpha \rightarrow \beta[x/c]$ and $\psi := \alpha \rightarrow \exists x \beta$.
Thus we may conclude with :
$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.
Finally :
(B) $\vdash \exists x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \exists x \beta)$.
The theorem follows from (A) and (B).
2nd Addendum
For the second part : $\leftarrow$, we can prove it without Corollary 24H (Rule EI).
(1) $\exists x(\alpha \rightarrow \beta)$ --- assumed
(2) $\alpha$ --- assumed
(3) $\lnot \exists x \beta$ --- assumed
(4) $\lnot \lnot \forall x \lnot \beta$ --- abreviation for $\exists$
(5) $\forall x \lnot \beta$ --- by Taut
(6) $\lnot \beta$ --- Ax.2
(7) $\vDash_{TAUT} \alpha \rightarrow (\lnot \beta \rightarrow \lnot (\alpha \rightarrow \beta))$
(8) $\lnot (\alpha \rightarrow \beta)$ --- from (2), (6) and (7) by mp
(9) $\forall x \lnot (\alpha \rightarrow \beta)$ --- by Gen Th ($x \notin FV(\alpha)$)
(10) $\lnot \exists x (\alpha \rightarrow \beta)$ --- abbreviation
(11) $\lnot \lnot \exists x \beta$ --- we apply Corollary 24E (Reductio ad Absurdum) [page 119] to (3), with (1) and (10)
(12) $\exists x \beta$ --- by Taut
(13) $\alpha \rightarrow \exists x \beta$ --- from (2) by Deduction Theorem.
So again :
$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.
Assume your proof ends with $D \cdots \forall v_1 \phi(v_1) \vdash \phi(t)$.
[EDIT: The following paragraph is a correction following a comment from Albert.]
If $v_1=v$, first rename all bound occurences of $v_1$ in the derivation $D \cdots \forall v_1 \phi(v_1)$ to a variable $v_1'\neq v$ which does not yet occur in the proof. All rules remain sound, and $D$ is not affected since it contains no occurences of $v$ (bound or free) by assumption. In this way you obtain a derivation $D \cdots \forall v_1' \phi(v_1')$ where $v_1'\neq v$.
Hence we can now assume $v_1\neq v$. By induction hypothesis we get a proof ending with $\forall v_1 (\varphi[v/c])(v_1)$. As you noted, what we ultimately want to get is a proof of $\varphi(t)[v/c]$. The trick is to apply $\forall E$ instantiating $v_1$ with $t[v/c]$ (instead of $t$). In this way you obtain the formula $\varphi[v/c](t[v/c])$, and this is indeed identical to $\varphi(t)[v/c]$.
The intuition is that $t$ might contain occurences of $c$, and so if you first replace all $c$'s by $v$'s and then all $v_1$'s by $t$'s, then the latter step reintroduces some $c$'s into your formula that you don't want to have. Consider for example the case that $\varphi=P(v_1)$, $t=c$ and your initial proof is $\forall v_1 P(v_1)\vdash P(c)$. The proposition says that you should be able to obtain a proof of $\forall v_1 P(v_1)\vdash P(v)$. Clearly you should not instantiate $v_1$ with $t=c$, but rather with $v=t[v/c]$.
Best Answer
"$\vDash$" means that RHS is true in every model of LHS. If $x$ does not occur free in $\alpha$, a model of $\alpha$ need not assign a value to $x$ - that is, in a model of $\alpha$, $\alpha$ is true for all assignments of $x$, so $\alpha \vDash \forall x \alpha$.
I'm not really sure if this is how formally you are expected to answer something like this (assuming this is attached to some kind of course in logic), but this is the reason it's true.