Struggling to prove $T \models_t \alpha \Rightarrow T \vdash \alpha$, $T$ being a theory $T \models_t \alpha$ is an abbreviation of $\forall\mathcal{A}(\forall w((\mathcal{A}, w) \models T) \Rightarrow \forall w((\mathcal{A}, w) \models \alpha))$, where $\mathcal{A}$ is a structure and $w$ is a variable assignment. $T \models \alpha$ is an abbreviation of $\forall \mathcal{M}(\mathcal{M} \models T \Rightarrow \mathcal{M} \models \alpha)$.
In my logic book (p. 102 of Wolfgang Rautenberg's A Concise Introduction to Mathematical Logic (Third Edition), if anyone wants to look up the precise wording), the author states that $T \models_t \alpha$ is equivalent to $T \vdash \alpha$. I've managed to prove $T \vdash\alpha \Rightarrow T \models_t \alpha$, but I struggle with the converse. Here is the proof.
\begin{align*}
T \vdash \alpha &\Leftrightarrow T \models \alpha  &\text{(soundness and completeness of FOL)} \\
&\Leftrightarrow \forall \mathcal{M}(\mathcal{M} \models T \Rightarrow \mathcal{M} \models \alpha) &\text{(definition)} \\
&\Leftrightarrow \forall \mathcal{A}\forall w((\mathcal{A}, w) \models T \Rightarrow (\mathcal{A}, w) \models \alpha) &\text{(definition)} \\
&\Rightarrow \forall\mathcal{A}(\forall w((\mathcal{A}, w) \models T) \Rightarrow \forall w((\mathcal{A}, w) \models \alpha)) &\text{(generally valid implication)} \\
&\Leftrightarrow T \models_t \alpha. &\text{(definition)}
\end{align*}
As we can see, the crucial part is the fourth line. I know that, generally, the converse implication is not always true. However, if the author's claim is true, it must be the case when structures and variable assignments are considered, i.e., $T \models_t \alpha \Rightarrow T \models \alpha$ must also hold. But I have no idea how to prove it and I even fear I could find a counterexample, in which case I'd be hopelessly confused! Any help is dearly appreciated. :)
P.S. Note that the author uses the notation $T \models \alpha$ for $T \models_t \alpha$, expecting that the reader will always presuppose the correct definition due to the consequence relation obtaining between a theory and a formula. I expanded the notation to avoid such ambiguity and confusion with the ordinary $\models$.
 A: The generally valid implication is $[\forall b (P(b) \implies Q(b))] \implies [\forall b P(b) \implies \forall b Q(b)]$.
Here, $P(b)$ is $(A, b) \models T$ and $Q(b)$ is $(A, b) \models \alpha$.
To show the above implication, suppose that $\forall b (P(b) \implies Q(b))$. And further suppose $\forall b P(b)$. Consider an arbitrary $b$. Then $P(b)$. And $P(b) \implies Q(b)$. So $Q(b)$.
Edit: the converse does not hold. For consider the statement $T :\equiv (a \neq b)$ and $\alpha :\equiv a = b$. Then clearly, it is not the case that $T \models \alpha$. But it is the case that $T \models_t \alpha$.
For suppose given some $A$. And suppose that for all $w$, $(A, w) \models T$. This is equivalent to saying $\forall x \in A \forall y \in A (x \neq y)$, which is in turn equivalent to saying $A$ is empty. If $A$ is empty, then $\forall w ((A, w) \models \alpha)$ holds trivially, since there is no variable assignment $w$ for the variables $a$ and $b$.
Edit: in fact, as suggested, this does hold when one restricts $T$ to have no free variables. This is because if $T$ has no free variables then $(A, w) \models T$ if and only if $A \models T$.
A: The author says $X\vdash_T\alpha$ stands for $X\cup T\vdash\alpha$. Of course you can generalize this to $\vDash$ and use $X\vDash_T\alpha$ to stand for $X\cup T\vDash\alpha$. If so, then
$$
\begin{array}{rcll}
T\vDash_T\alpha &\iff & T\cup T\vDash\alpha &\text{by convention}\\
&\iff & T\vDash\alpha &\text{by }T\cup T=T\\
&\iff & T\vdash\alpha &\text{by completeness and soundness}\\
&\iff & T\cup T\vdash\alpha &\text{by }T\cup T=T\\
&\iff & T\vdash_T\alpha &\text{by convention.}
\end{array}
$$
By the way, so far as I know, the shorthand $X\vdash_T\alpha$ is useful while $X\vDash_T\alpha$ is not.
Now return to your proof. It should be corrected as follows:
\begin{align*}
T \vdash \alpha &\Leftrightarrow T \models \alpha  &\text{(soundness and completeness of FOL)} \\
&\Leftrightarrow \forall \mathcal{M}(\mathcal{M} \models T \Rightarrow \mathcal{M} \models \alpha) &\text{(definition of $\vDash$)} \\
&\Leftrightarrow \color{red}{\forall \mathcal{A}\forall w((\mathcal{A}, w) \models T \Rightarrow (\mathcal{A}, w) \models \alpha) }&\text{(definition of $\vDash$)} \\
&\Leftrightarrow \forall \mathcal{A}\forall w((\mathcal{A}, w) \models T\cup T \Rightarrow (\mathcal{A}, w) \models \alpha) &\text{($T\cup T=T$)} \\
&\Leftrightarrow \forall \mathcal{A}(\mathcal{A} \models T\cup T \Rightarrow \mathcal{A} \models \alpha) &\text{(definition  of $\vDash$)} \\
&\Leftrightarrow T\cup T\models \alpha. &\text{(definition  of $\vDash$)}\\
&\Leftrightarrow T \models_T \alpha. &\text{(convention)}
\end{align*}
A: I would like to thank Mauro ALLEGRANZA for the crucial insight which proves the converse implication: $T$ is (by definition, because it's a theory) a set of sentences.
Let $\mathcal{A}_0$ be some structure and $w_0$ some variable assignment. Let
$$
\forall\mathcal{A}(\forall w((\mathcal{A}, w) \models T) \Rightarrow \forall w((\mathcal{A}, w) \models \alpha))
$$
be true. Then we have
\begin{align*}
(\mathcal{A}_0,w_0) \models T &\Rightarrow \forall w ((\mathcal{A}_0,w) \models T) &\text{(because $T$ is a set of sentences)} \\
&\Rightarrow \forall w ((\mathcal{A}_0,w) \models \alpha) &\text{(premise)} \\
&\Rightarrow (\mathcal{A}_0,w_0) \models \alpha. &\text{(valid implication)}
\end{align*}
This proves
$$
\forall\mathcal{A}(\forall w((\mathcal{A}, w) \models T) \Rightarrow \forall w((\mathcal{A}, w) \models \alpha)) \Rightarrow \forall \mathcal{A}\forall w((\mathcal{A}, w) \models T \Rightarrow (\mathcal{A}, w) \models \alpha),
$$
which, by the proof in the original post, proves $T \models_t \alpha \Rightarrow T \vdash \alpha$.
