Coincidence for term values and satisfaction

Given: Work in ZF unless the statement explicitly weakens or supplements it; fix the objects and hypotheses of the statement.

For every set signature $L$ and $L$-structure $\mathcal{M}$ there is a unique set ${\mathrm{Sat}}_{\mathcal{M}}\subseteq {\mathrm{Form}}_L\times M^{\omega }$. Writing $\mathcal{M},s\models \varphi$ for membership, its clauses are $\mathcal{M},s\models u=v⟺\mathrm{⟦}u{\mathrm{⟧}}_s=\mathrm{⟦}v{\mathrm{⟧}}_s,$ $\mathcal{M},s\models R(t_1,\dots ,t_n)⟺(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\in R^{\mathcal{M}},$ $\mathcal{M},s\models \mathrm{\neg }\varphi ⟺\text{not }\mathcal{M},s\models \varphi ,$ $\mathcal{M},s\models \varphi \wedge \psi ⟺(\mathcal{M},s\models \varphi \text{ and }\mathcal{M},s\models \psi ),$ $\mathcal{M},s\models \mathrm{\exists }x\varphi ⟺\mathrm{\exists }b\in M(\mathcal{M},s[x:=b]\models \varphi )\mathrm{.}$ The set is uniformly first-order definable from $L$ and the structure data. (Existence and uniqueness of set satisfaction)

An occurrence is a token position in the parsed finite word. A variable occurrence is free when it is in a term field and no ancestor quantifier binds that variable. The variable field of a quantifier is a binder, not a free occurrence. Write $\mathrm{FV}(e)$ for the finite set of variables with free occurrences in $e$, and $\mathrm{Var}(e)$ for all variables appearing anywhere. A sentence is a formula with empty $\mathrm{FV}$. The recursive rules are $\mathrm{FV}(v)=\{v\}$, $\mathrm{FV}(c)=\mathrm{\varnothing }$, union over the arguments for function and atomic relation/equality expressions, unchanged under negation, union for conjunction, and $\mathrm{FV}(\mathrm{\exists }y\psi )=\mathrm{FV}(\psi )\setminus \{y\}$. Structural recursion justifies these set-valued definitions, with targets $\mathcal{P}(\omega )$ after identifying variables with their indices. Raw substitution $e[t\mathrm{/}x]$ replaces just the free occurrences of variable $x$ by term $t$. On terms it replaces $x$ by $t$, keeps other variables and constants, and acts on each argument. It commutes with atoms and Boolean constructors. At $\mathrm{\exists }y\psi$ it leaves the whole expression unchanged if $y=x$; otherwise it gives $\mathrm{\exists }y(\psi [t\mathrm{/}x])$. The term $t$ is free for $x$ in $e$ if, at every replaced occurrence, the path to the root crosses no binder for a member of $\mathrm{FV}(t)$. Thus at $\mathrm{\exists }y\psi$ with $y\mathrm{\ne }x$ and $x\in \mathrm{FV}(\psi )$ it requires both $y\mathrm{\notin }\mathrm{FV}(t)$ and that $t$ be free for $x$ in $\psi$. If no free $x$ occurs, the condition is vacuous. Simultaneous substitution replaces the original free occurrences once; it does not perform substitutions inside inserted terms. It need not equal sequential substitution. Conventions and prerequisites: thm-structural-recursion-on-set-coded-syntax. (Free variables and free-for substitution)