In the PDF textbook "A Friendly Introduction to Mathematical Logic 2nd Edition" by Christopher C. Leary and Lars Kristiansen, page 53, the first quantifier inference rule (QR) is defined by the ordered pair $(\Gamma,\theta)$ such that $\Gamma=\{\psi\to\phi\}$ and $\theta=\psi\to(\forall x\phi)$ where $x$ is not free in the formula $\psi$ (note this is important). The book provides a proof of $\Gamma\vDash\theta$ on page 56, but I decided to give my own, very similar proof.
My proof goes as follows:
$$\Gamma\vDash\theta\iff(\psi\to\phi)\vDash[\psi\to(\forall x\phi)]$$
Let $\mathfrak{U}$ be some fixed, arbitrary interpretation. Thus, continuing forth,
$$(\psi\to\phi)\vDash[\psi\to(\forall x\phi)]\iff\mathfrak{U}\vDash(\psi\to\phi)\Rightarrow\mathfrak{U}\vDash[\psi\to(\forall x\phi)]$$
If $\mathfrak{U}\not\vDash(\psi\to\phi),$ then we're done, so let's assume $\mathfrak{U}\vDash(\psi\to\phi)$ which we'll donote (Assumption 1). This leaves us to prove $\mathfrak{U}\vDash[\psi\to(\forall x\phi)]$ under (Assumption 1).
$$\mathfrak{U}\vDash[\psi\to(\forall x\phi)]\iff\mathfrak{U}\vDash\psi\Rightarrow\mathfrak{U}\vDash(\forall x\phi)$$
Like previously, if $\mathfrak{U}\not\vDash\psi$, then we're done, so let's assume $\mathfrak{U}\vDash\psi$ which we'll denote (Assumption 2). This leaves us to prove $\mathfrak{U}\vDash(\forall x\phi)$ under (Assumption 2).
\begin{align} \mathfrak{U}\vDash(\forall x\phi)&\iff(\forall s)(\mathfrak{U}\vDash(\forall x\phi)[s]) \\ &\iff(\forall s)(\forall a)(\mathfrak{U}\vDash\phi[s[x|a]]) \\ \text{Let $s=t$ be some fixed, arbitrary} \\ \text{variable assignment function into $\mathfrak{U}$.} \\ &\iff(\forall a)(\mathfrak{U}\vDash\phi[t[x|a]]) &&(1) \end{align}
From (Assumption 1),
\begin{align} \mathfrak{U}\vDash(\psi\to\phi)&\iff\mathfrak{U}\vDash\psi\Rightarrow\mathfrak{U}\vDash\phi \\ &\iff(\forall s)(\mathfrak{U}\vDash\psi[s])\Rightarrow(\forall s)(\mathfrak{U}\vDash\phi[s]) \\ \text{Let $s=t[x|a]$ be the same x-modified} \\ \text{assignment function seen in (1).} \\ &\iff\mathfrak{U}\vDash\psi[t[x|a]]\Rightarrow\mathfrak{U}\vDash\phi[t[x|a]]) \\ &\iff(\forall a)(\mathfrak{U}\vDash\psi[t[x|a]])\Rightarrow(\forall a)(\mathfrak{U}\vDash\phi[t[x|a]]) && (2) \end{align}
From (Assumption 2),
\begin{align} \mathfrak{U}\vDash\psi&\iff(\forall s)(\mathfrak{U}\vDash\psi[s]) \\ \text{Let $s=t[x|a]$ be the same x-modified} \\ \text{assignment function seen in (1).} \\ &\iff\mathfrak{U}\vDash\psi[t[x|a]] \\ &\iff(\forall a)(\mathfrak{U}\vDash\psi[t[x|a]])&&(3) \end{align}
Frome (2) and (3), we can deduce (1) and thus we have proven $\mathfrak{U}\vDash(\forall x\phi)$ and we are done. (I have left out some of the final steps, but the remaining steps should be trivial to complete from here hopefully.) $\square$
I'm pretty sure this proof is correct, but the only thing I'm unsure about is the necessity that $x$ be not free in $\psi$. The proof shown in the book uses this fact to help prove $\Gamma\vDash\theta$, so it makes me uneasy about the validity of my proof. From my proof, it seems unnecessary that $x$ be not free in the $\psi$, but I'm might be missing something. Can someone show me where I'm mistaken within my proof and explain why $x$ must not be free in $\psi$.
Because with $x$ free the inference is not valid.
In order to see why the condition is necessary, we can consider the following counter-example : $\psi,\phi := (x=0)$ and consider the stucture $\mathbb N$.
We want to show that :
This means [see page 36] :
See page 37 :
Now we cam follow your proof considering $\mathbb N$ as $\mathfrak U$.
this assumption is clearly correct.
And we have to show that $(x=0) \to \forall x (x=0)$ is true in $\mathbb N$, i.e. that :
If $s(x) \ne 0$, we are done (the antecedent is False).
The issue is when $s(x)=0$, because we want that : $\mathbb N \vDash (\forall x(x=0))[s]$.
In order to have this, we need that :
And here we are stuck....
Clearly :