[proofplan] We first define the value of every term under an assignment by recursion on the construction of terms. Once term interpretation is available, each formula $\varphi$ determines a set of assignments $\llbracket \varphi\rrbracket_M\subseteq \operatorname{Ass}(M)$, again by recursion on the construction of formulas. Membership $s\in \llbracket \varphi\rrbracket_M$ is then exactly the satisfaction relation $M\models \varphi[s]$. Uniqueness follows by induction on formula complexity, since each clause determines the truth value of a formula from the truth values of its immediate subformulas. [/proofplan]

[step:Interpret all terms recursively from the structure $M$]Let $\operatorname{Ass}(M)$ be the set of all assignments $s:\operatorname{Var}_L\to |M|$. For each $L$-term $t$, define a function \begin{align*} t^M:\operatorname{Ass}(M)&\to |M|\\ s&\mapsto t^M[s] \end{align*} by recursion on the construction of $t$. If $t$ is a variable $x$, set $t^M[s]=s(x)$. If $t$ is a constant symbol $c$, set $t^M[s]=c^M$. If $t$ has the form $f(t_1,\dots,t_n)$, where $f$ is an $n$-ary function symbol of $L$ and $t_1,\dots,t_n$ are already interpreted terms, set \begin{align*} t^M[s]=f^M(t_1^M[s],\dots,t_n^M[s]). \end{align*} Since every term is obtained in finitely many applications of these three formation rules, induction on term complexity gives existence and uniqueness of the interpretation function $t^M$ for every term $t$.[/step]

[guided]Before defining truth of formulas, we need a precise meaning for the value of a term under an assignment. The relevant domain is the set \begin{align*} \operatorname{Ass}(M)=\{s:\operatorname{Var}_L\to |M|\}, \end{align*} whose elements assign to each variable an element of the universe of $M$. For every term $t$, we define a map \begin{align*} t^M:\operatorname{Ass}(M)&\to |M|\\ s&\mapsto t^M[s]. \end{align*} There are three cases, matching exactly the grammar of terms. If $t$ is a variable $x$, its value under $s$ is the element assigned to $x$, so $t^M[s]=s(x)$. If $t$ is a constant symbol $c$, its value is the interpretation of that constant in the structure, so $t^M[s]=c^M$. If $t=f(t_1,\dots,t_n)$ for an $n$-ary function symbol $f$ and already constructed terms $t_1,\dots,t_n$, then the values $t_i^M[s]\in |M|$ have already been defined, and the interpretation $f^M:|M|^n\to |M|$ gives \begin{align*} t^M[s]=f^M(t_1^M[s],\dots,t_n^M[s]). \end{align*} This recursion is well-founded because terms are finite syntactic objects. Induction on the number of formation steps in $t$ proves that the function $t^M$ exists and is unique for every term $t$.[/guided]

[step:Define each formula by the set of assignments satisfying it]For each $L$-formula $\varphi$, define a subset \begin{align*} \llbracket \varphi\rrbracket_M\subseteq \operatorname{Ass}(M) \end{align*} by recursion on the construction of $\varphi$. For atomic formulas, set \begin{align*} \llbracket t_1=t_2\rrbracket_M &=\{s\in \operatorname{Ass}(M):t_1^M[s]=t_2^M[s]\},\\ \llbracket R(t_1,\dots,t_n)\rrbracket_M &=\{s\in \operatorname{Ass}(M):(t_1^M[s],\dots,t_n^M[s])\in R^M\}. \end{align*} For Boolean connectives, set \begin{align*} \llbracket \neg\varphi\rrbracket_M &=\operatorname{Ass}(M)\setminus \llbracket \varphi\rrbracket_M,\\ \llbracket \varphi\wedge\psi\rrbracket_M &=\llbracket \varphi\rrbracket_M\cap \llbracket \psi\rrbracket_M,\\ \llbracket \varphi\vee\psi\rrbracket_M &=\llbracket \varphi\rrbracket_M\cup \llbracket \psi\rrbracket_M,\\ \llbracket \varphi\to\psi\rrbracket_M &=\bigl(\operatorname{Ass}(M)\setminus \llbracket \varphi\rrbracket_M\bigr)\cup \llbracket \psi\rrbracket_M. \end{align*} For quantifiers, set \begin{align*} \llbracket \exists x\,\varphi\rrbracket_M &=\{s\in \operatorname{Ass}(M):\text{there exists }a\in |M|\text{ such that }s[x\mapsto a]\in \llbracket \varphi\rrbracket_M\},\\ \llbracket \forall x\,\varphi\rrbracket_M &=\{s\in \operatorname{Ass}(M):\text{for every }a\in |M|,\ s[x\mapsto a]\in \llbracket \varphi\rrbracket_M\}. \end{align*} Since every formula is built in finitely many applications of the atomic, Boolean, and quantified formation rules, induction on formula complexity gives existence and uniqueness of the set $\llbracket \varphi\rrbracket_M$ for every formula $\varphi$.[/step]

[guided]The satisfaction relation is most cleanly constructed by assigning to each formula the set of all assignments that make it true. Thus, for each formula $\varphi$, we define a subset \begin{align*} \llbracket \varphi\rrbracket_M\subseteq \operatorname{Ass}(M). \end{align*} The notation means: $s\in \llbracket \varphi\rrbracket_M$ precisely when the assignment $s$ satisfies $\varphi$ in $M$. For equality, the formula $t_1=t_2$ should hold exactly when the two interpreted terms have the same value: \begin{align*} \llbracket t_1=t_2\rrbracket_M =\{s\in \operatorname{Ass}(M):t_1^M[s]=t_2^M[s]\}. \end{align*} For an atomic relation formula $R(t_1,\dots,t_n)$, the tuple of interpreted term values must lie in the interpreted relation $R^M\subseteq |M|^n$: \begin{align*} \llbracket R(t_1,\dots,t_n)\rrbracket_M =\{s\in \operatorname{Ass}(M):(t_1^M[s],\dots,t_n^M[s])\in R^M\}. \end{align*} The Boolean clauses are set-theoretic translations of the ordinary truth tables. Negation becomes complement in $\operatorname{Ass}(M)$, conjunction becomes intersection, disjunction becomes union, and implication becomes “not the antecedent or the consequent”: \begin{align*} \llbracket \neg\varphi\rrbracket_M &=\operatorname{Ass}(M)\setminus \llbracket \varphi\rrbracket_M,\\ \llbracket \varphi\wedge\psi\rrbracket_M &=\llbracket \varphi\rrbracket_M\cap \llbracket \psi\rrbracket_M,\\ \llbracket \varphi\vee\psi\rrbracket_M &=\llbracket \varphi\rrbracket_M\cup \llbracket \psi\rrbracket_M,\\ \llbracket \varphi\to\psi\rrbracket_M &=\bigl(\operatorname{Ass}(M)\setminus \llbracket \varphi\rrbracket_M\bigr)\cup \llbracket \psi\rrbracket_M. \end{align*} For quantifiers, the only new operation is changing the value of the quantified variable. The modified assignment $s[x\mapsto a]$ keeps all variable values fixed except that it sends $x$ to $a$. Therefore $\exists x\,\varphi$ holds under $s$ exactly when some possible value $a\in |M|$ for $x$ makes $\varphi$ true: \begin{align*} \llbracket \exists x\,\varphi\rrbracket_M =\{s\in \operatorname{Ass}(M):\text{there exists }a\in |M|\text{ such that }s[x\mapsto a]\in \llbracket \varphi\rrbracket_M\}. \end{align*} Likewise, $\forall x\,\varphi$ holds under $s$ exactly when every possible value $a\in |M|$ for $x$ makes $\varphi$ true: \begin{align*} \llbracket \forall x\,\varphi\rrbracket_M =\{s\in \operatorname{Ass}(M):\text{for every }a\in |M|,\ s[x\mapsto a]\in \llbracket \varphi\rrbracket_M\}. \end{align*} The recursion is well-founded because every formula has finite syntactic complexity, and every recursive clause refers only to immediate subformulas of smaller complexity. Hence induction on formula complexity gives a unique set $\llbracket \varphi\rrbracket_M$ for each formula $\varphi$.[/guided]

[step:Recover the satisfaction relation from the assignment sets] Define the relation \begin{align*} \models_M\ \subseteq \operatorname{Form}_L\times \operatorname{Ass}(M) \end{align*} by \begin{align*} M\models \varphi[s]\quad\Longleftrightarrow\quad s\in \llbracket \varphi\rrbracket_M. \end{align*} The defining equations for $\llbracket \varphi\rrbracket_M$ immediately give all stated clauses for equality, relation symbols, Boolean connectives, and quantifiers. Thus a satisfaction relation satisfying the displayed Tarski clauses exists. [/step]

[step:Prove uniqueness by induction on formula complexity] Let $\Vdash_M$ be any relation on $\operatorname{Form}_L\times \operatorname{Ass}(M)$ satisfying the same clauses. We prove by induction on the complexity of $\varphi$ that, for every assignment $s\in \operatorname{Ass}(M)$, \begin{align*} M\models \varphi[s]\quad\Longleftrightarrow\quad M\Vdash \varphi[s]. \end{align*} For atomic formulas, both relations are determined by the same term values and the same interpretations of equality and relation symbols in $M$. For Boolean formulas, the induction hypothesis applied to the immediate subformulas transfers the truth values through the same Boolean truth clauses. For quantified formulas, the induction hypothesis applied to $\varphi$ gives, for every $a\in |M|$, \begin{align*} M\models \varphi[s[x\mapsto a]] \quad\Longleftrightarrow\quad M\Vdash \varphi[s[x\mapsto a]]. \end{align*} Taking existence over $a\in |M|$ gives the equivalence for $\exists x\,\varphi$, and taking universality over $a\in |M|$ gives the equivalence for $\forall x\,\varphi$. Therefore $\Vdash_M$ agrees with $\models_M$ on every formula and every assignment, so the satisfaction relation satisfying the Tarski clauses is unique. This completes the proof. [/step]