[proofplan]
We prove that the displayed clauses determine a unique relation by structural recursion on formulas. Atomic formulas are evaluated directly using the already-defined interpretation of terms in the structure $M$. Compound formulas are then evaluated from the satisfaction values of their immediate subformulas, and uniqueness follows by structural induction on formula complexity.
[/proofplan]
[step:Define satisfaction on atomic formulas by interpreting terms in $M$]
Let $\operatorname{Ass}(M)$ denote the set of all assignments $s: \operatorname{Var} \to |M|$.
For atomic equality formulas, define $M \models (t_1=t_2)[s]$ exactly when $t_1^M[s]=t_2^M[s]$ in $|M|$. For atomic relation formulas, if $R$ is an $n$-ary relation symbol of $L$, define $M \models R(t_1,\dots,t_n)[s]$ exactly when
\begin{align*}
(t_1^M[s],\dots,t_n^M[s]) \in R^M.
\end{align*}
The terms $t_i^M[s]$ are already defined by the recursive interpretation of terms in an $L$-structure, so these two clauses assign a definite truth value to every atomic formula and every assignment.
[/step]
[step:Extend satisfaction through the Boolean connectives]
Assume satisfaction has already been defined for the immediate subformulas of a formula.
For a negation $\neg\varphi$, define
\begin{align*}
M \models (\neg\varphi)[s]
\quad \Longleftrightarrow \quad
M \not\models \varphi[s].
\end{align*}
For a conjunction $\varphi \wedge \psi$, define
\begin{align*}
M \models (\varphi \wedge \psi)[s]
\quad \Longleftrightarrow \quad
M \models \varphi[s] \text{ and } M \models \psi[s].
\end{align*}
If other Boolean connectives are primitive in the syntax, define them by their classical truth clauses. Each definition refers only to immediate subformulas, which have strictly smaller formula complexity, so the recursive definition is well-founded.
[/step]
[step:Extend satisfaction through the quantifiers by varying one variable assignment]
Let $x \in \operatorname{Var}$, let $\varphi$ be an $L$-formula, and let $s \in \operatorname{Ass}(M)$. For each $a \in |M|$, the map $s[x \mapsto a]: \operatorname{Var} \to |M|$ is an assignment because it sends every variable either to $a \in |M|$ or to the already-defined value $s(y) \in |M|$.
Define
\begin{align*}
M \models (\exists x\,\varphi)[s]
\quad \Longleftrightarrow \quad
\text{there exists } a \in |M| \text{ such that } M \models \varphi[s[x \mapsto a]].
\end{align*}
Define
\begin{align*}
M \models (\forall x\,\varphi)[s]
\quad \Longleftrightarrow \quad
\text{for every } a \in |M|,\ M \models \varphi[s[x \mapsto a]].
\end{align*}
These clauses again refer only to the immediate subformula $\varphi$, so they extend the previously defined satisfaction relation to quantified formulas.
[/step]
[step:Prove existence by induction on formula complexity]
Define the complexity $c(\varphi) \in \mathbb{N}$ of an $L$-formula $\varphi$ as the number of logical constructors occurring in $\varphi$, where atomic formulas have complexity $0$.
We construct satisfaction for all formulas of complexity at most $k$ by induction on $k \in \mathbb{N}$. For $k=0$, the formula is atomic, and satisfaction is defined by the equality and relation clauses above. Suppose satisfaction has been defined for all formulas of complexity less than $k$, and let $\theta$ be a formula with $c(\theta)=k$. By the formation rules for first-order formulas, $\theta$ has one of the forms $\neg\varphi$, $\varphi \wedge \psi$, $\exists x\,\varphi$, or $\forall x\,\varphi$, with each immediate subformula having complexity less than $k$. The corresponding recursive clause therefore defines $M \models \theta[s]$ for every assignment $s \in \operatorname{Ass}(M)$.
By induction, satisfaction is defined for every $L$-formula and every assignment in $M$.
[/step]
[step:Prove uniqueness by structural induction on formulas]
Let $\models_1$ and $\models_2$ be two relations between $L$-formulas and assignments in $M$ satisfying all the displayed clauses. We prove by structural induction on $\varphi$ that, for every assignment $s \in \operatorname{Ass}(M)$,
\begin{align*}
M \models_1 \varphi[s]
\quad \Longleftrightarrow \quad
M \models_2 \varphi[s].
\end{align*}
For atomic equality and relation formulas, both relations are governed by the same interpretation of terms and relation symbols in $M$, so they agree.
For $\neg\varphi$, the induction hypothesis gives agreement on $\varphi$ for the assignment $s$, hence the negation clauses give agreement on $\neg\varphi$. For $\varphi \wedge \psi$, the induction hypothesis gives agreement on both $\varphi$ and $\psi$, hence the conjunction clauses give agreement on $\varphi \wedge \psi$.
For $\exists x\,\varphi$, the induction hypothesis applies to $\varphi$ for every modified assignment $s[x \mapsto a]$ with $a \in |M|$. Therefore the existence of an element $a \in |M|$ satisfying the subformula is the same for $\models_1$ and $\models_2$. Thus the two relations agree on $\exists x\,\varphi$. The universal quantifier is identical except that the existential condition is replaced by the condition that every $a \in |M|$ satisfies the subformula.
Hence the two relations agree on every formula and every assignment. The recursively defined satisfaction relation is therefore unique.
[/step]
[step:Conclude that the recursive clauses define Tarski satisfaction]
The previous steps establish existence of a relation $M \models \varphi[s]$ satisfying the atomic, Boolean, and quantifier clauses, and also establish that no other relation can satisfy those same clauses. Therefore the clauses define a unique satisfaction relation between $M$, $L$-formulas, and assignments in $M$. This unique relation is Tarski's satisfaction relation.
[/step]
