Free-for substitution commutes with satisfaction

Write $b=\mathrm{⟦}t{\mathrm{⟧}}_s$. The term substitution identity proves the assertion for both kinds of atoms. Negation and conjunction transport the inductive equivalences through their truth clauses.

At $\mathrm{\exists }y\psi$, if $y=x$, raw substitution leaves this quantified formula unchanged and updating its bound variable externally cannot affect its truth by coincidence. If $x\mathrm{\notin }\mathrm{FV}(\psi )$, substitution again changes nothing and coincidence gives the result.

Otherwise $y\mathrm{\ne }x$ and $x\in \mathrm{FV}(\psi )$. The free-for hypothesis gives $y\mathrm{\notin }\mathrm{FV}(t)$ and the free-for condition in $\psi$. For each $a\in M$, coincidence makes $\mathrm{⟦}t{\mathrm{⟧}}_{s[y:=a]}=b$. The two distinct-variable updates commute: $s[y:=a][x:=b]=s[x:=b][y:=a]$. Applying the induction hypothesis to $\psi$ at $s[y:=a]$ therefore gives the same truth at each witness $a$ on both sides.

Existential quantification over these pointwise equivalent assertions proves both directions for $\mathrm{\exists }y\psi$. The cases above exhaust its possibilities, so structural induction gives the result for every formula.