I am reading Enderton's A Mathematical Introduction to Logic (here a link to its second edition) and I am not sure I understand this proof, could anyone help please?
What I don't understand is what the structure of the proof is: specifically what the induction is being done on, and what the induction hypothesis is.
It seems to me that the induction is being done on the complexity of the formula, ie. count of logical operator. Atomic formula, which by def has no logical operator, naturally becomes the base case, with $\lnot$ and $\to$ being the inductive steps.
The $\forall$ case is the most confusing. By assumption $s_1(x|d)$ agrees with $s_2(x|d)$ - that I understand. But then Enderton cites the inductive hypothesis as the justification of $\psi$ being satisfied by $s_1(x|d)$ iff it is satisfied by $s_2(x|d)$ - this only seems possible if the induction is done on the complexity of the formula, otherwise I don't see how he can legitimately cite the hypothesis here.
Satisfaction as explained in the book:
As you said, the proof of theorem 22A is by induction on (the complexity of) the formula $\varphi$.
There are two subtleties in this proof.
In the base case, where $\varphi$ is an atomic formula, the proof uses the following lemma: given a term $t$, if $s_1$ and $s_2$ agree at all variables in $t$ then $\overline{s_1}(t) = \overline{s_2}(t)$. As mentioned in the text, this lemma should be proved separately, by induction on the (complexity of the) term $t$.
In the inductive step where $\varphi = \forall x \, \psi$, the induction hypothesis says that if $s'_1$ and $s'_2$ are two functions from $V$ to $|\mathfrak{A}|$ that agree at all free variables in $\psi$, then $\mathfrak{A}$ satisfies $\psi$ with $s_1'$ iff $\mathfrak{A}$ satisfies $\psi$ with $s_2'$. Unfortunately, you cannot apply the induction hypothesis to $\psi$ with $s_1$ and $s_2$ because $x$ is not a free variable of $\varphi = \forall x \, \psi$ but it might be a free variable in $\psi$ and we do not have any hypothesis about the behavior of $s_1$ and $s_2$ in $x$ (said differently, the formula $\psi$ is smaller than $\varphi$ but the hypothesis are not satisfied by $\psi$ with $s_1$ and $s_2$). But the functions $s_1(x \mid d)$ and $s_2(x \mid d)$ agree at all the free variables of $\psi$, hence we can apply the induction hypothesis to $\psi$ with $s_1(x \mid d)$ and $s_2(x \mid d)$: therefore, $\mathfrak{A}$ satisfies $\psi$ with $s_1(x \mid d)$ iff $\mathfrak{A}$ satisfies $\psi$ with $s_2(x \mid d)$. By definition of satisfaction, this means that $\mathfrak{A}$ satisfies $\varphi = \forall x \, \psi$ with $s_1$ iff $\mathfrak{A}$ satisfies $\varphi$ with $s_2$.