I have a problem with two forms of the generalization rule in logic.
Shoenfield proves in his book that if $T\vdash\phi$ where $T$ is a set of formulas and $\phi$ is a formula, then $T\vdash\forall x\phi$.
His proof is, "from $T\vdash\phi$ and the tautology $\phi\to(\lnot\forall x\phi\to\phi)$, $T\vdash\lnot\forall x\phi\to\phi$. Then by the $\forall$-introduction rule, $T\vdash\lnot\forall x\phi\to\forall x\phi$ ; so $T\vdash\forall x\phi$ by the tautology $(\lnot\forall x\phi\to\forall x\phi) \to\forall x\phi$" ( The $\forall$-introduction rule can be deduced by the $\exists$-introduction rule which is considered as one of rules of inference in the book).
On the other hand, Enderton shows that if $T\vdash\phi$ and $x$ do not occur free in any formula in $T$, then $T\vdash\forall x\phi$, and says the restriction that $x$ not occur free in $T$ is essential, whereas Shoenfield does not restrict anything.
So $Px\vdash\forall x (Px)$ by Shoenfield and may not by Enderton. I wonder why it happens.
My opinion is that it happens because of the difference between their definition of '$\vDash$ for sets of formulas'. Enderton defines that $Px\vDash\forall x Px$ iff for every structure $\mathfrak A$ and every $a\in A$, the universe of $\mathfrak A$, such that $\mathfrak A\vDash Px[a]$, $\mathfrak A\vDash\forall x Px$. But Shoenfield writes $Px\vDash\forall x Px$ when for every structure $\mathfrak A$ such that $\forall a\in A(\mathfrak A\vDash Px[a])$, $\mathfrak A\vDash\forall x Px$. Obviously, $Px\not\vDash\forall x Px$ with Enderton's definition and $Px\vDash\forall x Px$ with Shoenfield's one.
Are there the others which expain why it happens? and Which definition is used in the modern mathematics?