Term substitution commutes with evaluation

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

For an $L$-structure $\mathcal{M}$ and assignment $s\in M^{\omega }$, define $\mathrm{⟦}{v}_i{\mathrm{⟧}}_s=s(i)$, $\mathrm{⟦}c{\mathrm{⟧}}_s=c^{\mathcal{M}}$ and $\mathrm{⟦}f(t_1,\dots ,t_n){\mathrm{⟧}}_s=f^{\mathcal{M}}(\mathrm{⟦}{t}_1{\mathrm{⟧}}_s,\dots ,\mathrm{⟦}{t}_n{\mathrm{⟧}}_s)\mathrm{.}$ This is a simultaneous definition for all assignments: recurse on terms into the set $M^{(M^{\omega })}$ of functions from assignments to $M$. Variable leaves are projections, constant leaves are constant maps, and each function operation acts pointwise. Structural recursion gives a unique evaluation. The operations are total because the interpreted functions are total. Superscripts $\mathcal{M}$ on brackets will distinguish structures when needed. Conventions and prerequisites: def-set-structures-and-variable-assignments, thm-structural-recursion-on-set-coded-syntax. (Term denotation)

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)