I am trying to get my head around logical implication. This is a very basic question but it seems so trivial that I think I must have misunderstood it. Prove
$$\{\forall x\ (\alpha\to\beta) ,\forall x\ \alpha\}\models \forall x \ \beta$$
Okay, so for any structure $A$ and any variable assignment $s:V\to|A|$ such that $$\models_A \forall x\ (\alpha\to\beta)[s] \ \& \models_A \forall x\ \alpha[s]$$ we must have $$\models_A \forall x\ \beta[s].$$
Now either this is trivially true or I am not getting something. Any help?
It is not so trivially true. The point of the exercise is to see whether you understand the distinction between syntax and semantics. Whether a formula is satisfied by a structure is recursively defined according to the syntax. To use a clearer notation:
If $A[s] \vDash \forall x\ ( α \to β )$ and $A[s] \vDash \forall x\ (α)$:
Given any element $c$ in $A$:
$A[s][x \mapsto c] \vDash ( α \to β )$ and $A[s][x \mapsto c] \vDash α$. [by definition of satisfaction for $\forall$]
If $A[s][x \mapsto c] \vDash α$ then $A[s][x \mapsto c] \vDash β$. [by definition of satisfaction for $\to$]
Thus $A[s][x \mapsto c] \vDash β$. [by modus ponens in the meta-system]
Therefore $A[s] \vDash \forall x\ ( β )$. [by definition of satisfaction for $\forall$]
Note what is happening. The syntax of the formal system was in fact designed to capture logical reasoning, so it is no surprise that the reasoning above looks very much like how it could be done inside the system, but this is the point; a semantic proof is not a priori the same as a syntactic proof. It turns out that $\vdash$ and $\vDash$ are the same for first-order logic, but that is a non-trivial result called the completeness theorem.