Subtler than meets the eye: does x=y imply forall x forall y x=y? In Enderton's "Mathematical Introduction to Logic" (2ed p.88), $\Gamma\models\phi$ is defined to mean that for every model $M$ and every assignment $s$ such that $M\models\Gamma[s]$, $M\models \phi[s]$.
By contrast, in Bilaniuk's "Problem Course in Mathematical Logic" definition 6.6 on p.38, $\Gamma\models\phi$ is defined to mean that for every model $M$ such that $M\models\Gamma$, $M\models\phi$.  Here, $M\models \Gamma$ means $M\models \gamma[s]$ for every assignment $s$ and every $\gamma\in\Gamma$, similarly for $M\models \phi$.
$\Gamma\models\phi$ in symbols:


*

*Enderton: $\forall M \forall s
   (M\models \Gamma[s]\rightarrow
   M\models\phi[s])$

*Bilaniuk: $\forall    M ((\forall s
   M\models    \Gamma[s])\rightarrow
   (\forall s M\models\phi[s]))$


According to the former, $\lbrace x=y\rbrace\not\models\forall x\forall y (x=y)$.  According to the latter, $\lbrace x=y\rbrace\models\forall x\forall y(x=y)$.
What do the logicians here at Math Overflow think about this conundrum?
 A: I prefer Enderton's definition, but either definition will work if used consistently.  The only way to get a "conundrum" is to mix the two.  This is not the only place in mathematics where reasonable people have proposed different definitions for the same notation or terminology and where problems would arise if one were to try to use both definitions at the same time.  
A: In my experience, Enderton’s definition is far more prevalent.  Certainly in categorical logic and the areas of proof theory I’m familiar with, it’s almost always what’s intended.
On the other hand, $\Gamma \vDash \varphi$ is most often used when $\Gamma$ is some theory, i.e. a set of closed formulas, in which case they are equivalent.  The difference appears only when $\Gamma$ and $\varphi$ share free variables.
Bilaniuk’s definition (universally closing the two sides separately) is certainly coherent in itself.  But Enderton’s definition (universally closing over the whole relation) has various nice properties which Bilaniuk’s lacks:


*

*It corresponds more closely to the “provability” relation $\Gamma \vdash \varphi$.  (This is the biggest one!) 

*The deduction lemma: $\Gamma \vDash \varphi \Rightarrow \psi$ if and only if $\Gamma \cup \{\varphi\} \vDash \psi$.

*More general.  Any instance of Bilaniuk’s is trivially equivalent to one of Enderton’s (by renaming variables on the right to be disjoint from those on the left).

*More intuitive.  If I read $\varphi(x,y) \vDash \psi(x,y)$, then it seems natural to expect that the $x$ on the left corresponds somehow to the $x$ on the right, and likewise the $y$.  Under Bilaniuk’s reading, the shared variable names are just a red herring.


These are somewhat subjective, of course; I’m sure someone who prefers Bilaniuk’s definition could give some good counter-points.
