[proofplan] We first prove, by induction on $L$-terms, that every term has the same value in the substructure $A$ as in the ambient structure $M$ when evaluated at parameters from $|A|$. This reduces preservation of atomic formulas to the defining clauses of substructure: equality is preserved because term values agree, and relation symbols are interpreted in $A$ by restriction from $M$. We then prove the theorem by structural induction on quantifier-free formulas, using the atomic case as the base case and the induction hypothesis for Boolean connectives. [/proofplan] [step:Show that terms evaluate identically in $A$ and in $M$] Fix $a = (a_1,\dots,a_n) \in |A|^n$. For every $L$-term $t(x_1,\dots,x_n)$, let $t^A(a) \in |A|$ denote the value of $t$ in $A$ at $a$, and let $t^M(a) \in |M|$ denote the value of $t$ in $M$ at the same tuple. We prove by induction on the construction of $t$ that \begin{align*} t^A(a) = t^M(a). \end{align*} If $t$ is the variable $x_i$ for some $i \in \{1,\dots,n\}$, then $t^A(a) = a_i = t^M(a)$. If $t$ is a constant symbol $c$ of $L$, then $c^A = c^M$ because $A$ is an $L$-substructure of $M$. Now suppose $t$ has the form $f(t_1,\dots,t_m)$, where $f$ is an $m$-ary function symbol of $L$ and $t_1,\dots,t_m$ are $L$-terms. By the induction hypothesis, \begin{align*} t_j^A(a) = t_j^M(a) \end{align*} for each $j \in \{1,\dots,m\}$. Since $A$ is closed under the interpretations of function symbols and $f^A$ is the restriction of $f^M$ to $|A|^m$, we obtain \begin{align*} t^A(a) &= f^A(t_1^A(a),\dots,t_m^A(a)) \\ &= f^M(t_1^A(a),\dots,t_m^A(a)) \\ &= f^M(t_1^M(a),\dots,t_m^M(a)) \\ &= t^M(a). \end{align*} This completes the induction on terms. [guided] Fix the parameter tuple $a = (a_1,\dots,a_n) \in |A|^n$. For an $L$-term $t(x_1,\dots,x_n)$, the notation $t^A(a)$ denotes the element of $|A|$ obtained by interpreting all symbols of $t$ inside $A$, while $t^M(a)$ denotes the element of $|M|$ obtained by interpreting the same term inside $M$. We prove that these two evaluations always agree: \begin{align*} t^A(a) = t^M(a). \end{align*} The proof is by induction on the construction of the term $t$. First suppose $t$ is a variable, say $t = x_i$ with $i \in \{1,\dots,n\}$. Then both structures evaluate $x_i$ at the same assigned element $a_i$, so \begin{align*} t^A(a) = a_i = t^M(a). \end{align*} Next suppose $t$ is a constant symbol $c$ of $L$. Since $A \subset M$ is an $L$-substructure, the interpretation of $c$ in $A$ is the same element as its interpretation in $M$. Hence \begin{align*} t^A(a) = c^A = c^M = t^M(a). \end{align*} Finally suppose $t$ is built using an $m$-ary function symbol $f$ of $L$: \begin{align*} t = f(t_1,\dots,t_m), \end{align*} where $t_1,\dots,t_m$ are smaller $L$-terms. The induction hypothesis says that each smaller term has the same value in $A$ and in $M$: \begin{align*} t_j^A(a) = t_j^M(a) \end{align*} for every $j \in \{1,\dots,m\}$. Because $A$ is a substructure, the function $f^A: |A|^m \to |A|$ is exactly the restriction of $f^M: |M|^m \to |M|$ to tuples from $|A|^m$. Therefore \begin{align*} t^A(a) &= f^A(t_1^A(a),\dots,t_m^A(a)) \\ &= f^M(t_1^A(a),\dots,t_m^A(a)) \\ &= f^M(t_1^M(a),\dots,t_m^M(a)) \\ &= t^M(a). \end{align*} This proves the term-evaluation lemma. [/guided] [/step] [step:Verify preservation for atomic formulas] Let $\psi(x_1,\dots,x_n)$ be an atomic $L$-formula. There are two cases. First suppose $\psi$ has the form $s = t$, where $s$ and $t$ are $L$-terms. By the previous step, \begin{align*} s^A(a) = s^M(a) \quad\text{and}\quad t^A(a) = t^M(a). \end{align*} Hence \begin{align*} A \models s(a) = t(a) &\iff s^A(a) = t^A(a) \\ &\iff s^M(a) = t^M(a) \\ &\iff M \models s(a) = t(a). \end{align*} Second suppose $\psi$ has the form $R(t_1,\dots,t_m)$, where $R$ is an $m$-ary relation symbol of $L$ and $t_1,\dots,t_m$ are $L$-terms. By the previous step, \begin{align*} t_j^A(a) = t_j^M(a) \end{align*} for each $j \in \{1,\dots,m\}$. Since $R^A = R^M \cap |A|^m$, we have \begin{align*} A \models R(t_1(a),\dots,t_m(a)) &\iff (t_1^A(a),\dots,t_m^A(a)) \in R^A \\ &\iff (t_1^M(a),\dots,t_m^M(a)) \in R^M \\ &\iff M \models R(t_1(a),\dots,t_m(a)). \end{align*} Thus every atomic $L$-formula is preserved between $A$ and $M$ on tuples from $|A|$. [guided] Let $\psi(x_1,\dots,x_n)$ be an atomic $L$-formula. Atomic formulas are the base cases for the later induction on quantifier-free formulas, so we verify both possible forms. First consider an atomic equality \begin{align*} \psi = (s = t), \end{align*} where $s$ and $t$ are $L$-terms. The previous step gives equality of term evaluations in the two structures: \begin{align*} s^A(a) = s^M(a) \quad\text{and}\quad t^A(a) = t^M(a). \end{align*} Therefore the equality holds in $A$ exactly when the corresponding equality holds in $M$: \begin{align*} A \models s(a) = t(a) &\iff s^A(a) = t^A(a) \\ &\iff s^M(a) = t^M(a) \\ &\iff M \models s(a) = t(a). \end{align*} Now consider an atomic relation formula \begin{align*} \psi = R(t_1,\dots,t_m), \end{align*} where $R$ is an $m$-ary relation symbol of $L$ and $t_1,\dots,t_m$ are $L$-terms. Again the previous step gives \begin{align*} t_j^A(a) = t_j^M(a) \end{align*} for every $j \in \{1,\dots,m\}$. The defining relation-substructure condition says that $R^A$ is the restriction of $R^M$ to tuples from $|A|^m$, equivalently \begin{align*} R^A = R^M \cap |A|^m. \end{align*} Since each $t_j^A(a)$ lies in $|A|$, membership in $R^A$ is the same as membership in $R^M$ for this tuple. Thus \begin{align*} A \models R(t_1(a),\dots,t_m(a)) &\iff (t_1^A(a),\dots,t_m^A(a)) \in R^A \\ &\iff (t_1^M(a),\dots,t_m^M(a)) \in R^M \\ &\iff M \models R(t_1(a),\dots,t_m(a)). \end{align*} This proves preservation for all atomic formulas. [/guided] [/step] [step:Extend the equivalence through Boolean connectives] We prove the theorem by structural induction on the quantifier-free formula $\varphi(x_1,\dots,x_n)$. The atomic case was proved in the previous step. For negation, suppose $\varphi$ has the form $\neg \theta$, where $\theta$ is quantifier-free and the equivalence has already been proved for $\theta$. Then \begin{align*} A \models \neg \theta(a) &\iff A \not\models \theta(a) \\ &\iff M \not\models \theta(a) \\ &\iff M \models \neg \theta(a). \end{align*} For conjunction, suppose $\varphi$ has the form $\theta \wedge \rho$, where $\theta$ and $\rho$ are quantifier-free and the equivalence has already been proved for both. Then \begin{align*} A \models (\theta \wedge \rho)(a) &\iff A \models \theta(a)\ \text{and}\ A \models \rho(a) \\ &\iff M \models \theta(a)\ \text{and}\ M \models \rho(a) \\ &\iff M \models (\theta \wedge \rho)(a). \end{align*} The cases of disjunction, implication, biconditional, and any other Boolean connective included as primitive in the chosen syntax are handled by the same truth-table argument using the induction hypothesis for the immediate subformulas. Therefore, for every quantifier-free $L$-formula $\varphi(x_1,\dots,x_n)$ and every tuple $a \in |A|^n$, \begin{align*} A \models \varphi(a) \iff M \models \varphi(a). \end{align*} This is the desired equivalence. [guided] We now pass from atomic formulas to all quantifier-free formulas. The method is structural induction on $\varphi$. Since quantifier-free formulas are built from atomic formulas using Boolean connectives, there is no quantifier case to consider. The base case is exactly the atomic preservation result proved in the previous step. Thus, if $\varphi$ is atomic, then \begin{align*} A \models \varphi(a) \iff M \models \varphi(a). \end{align*} Now suppose $\varphi$ is formed by negation: \begin{align*} \varphi = \neg \theta, \end{align*} where $\theta$ is quantifier-free. The induction hypothesis gives \begin{align*} A \models \theta(a) \iff M \models \theta(a). \end{align*} Taking the logical negation of both sides gives \begin{align*} A \models \neg \theta(a) &\iff A \not\models \theta(a) \\ &\iff M \not\models \theta(a) \\ &\iff M \models \neg \theta(a). \end{align*} Next suppose $\varphi$ is formed by conjunction: \begin{align*} \varphi = \theta \wedge \rho, \end{align*} where $\theta$ and $\rho$ are quantifier-free. The induction hypothesis applies separately to $\theta$ and to $\rho$: \begin{align*} A \models \theta(a) \iff M \models \theta(a), \qquad A \models \rho(a) \iff M \models \rho(a). \end{align*} Using the truth definition for conjunction, \begin{align*} A \models (\theta \wedge \rho)(a) &\iff A \models \theta(a)\ \text{and}\ A \models \rho(a) \\ &\iff M \models \theta(a)\ \text{and}\ M \models \rho(a) \\ &\iff M \models (\theta \wedge \rho)(a). \end{align*} If the syntax treats disjunction, implication, biconditional, or other Boolean connectives as primitive, their cases follow in the same way: evaluate the immediate subformulas in $A$ and $M$, use the induction hypothesis to identify their truth values, and then apply the truth table for the connective. Hence the truth value of every quantifier-free formula is the same in $A$ and in $M$ on every tuple from $|A|^n$: \begin{align*} A \models \varphi(a) \iff M \models \varphi(a). \end{align*} This proves the theorem. [/guided] [/step]