[proofplan] We prove a stronger assignment-level statement: for every $L$-formula $\psi$ and every assignment $s$ of variables into $|M|$, truth of $\psi$ in $M$ under $s$ is equivalent to truth of $\psi$ in $N$ under the transported assignment $h \circ s$. The proof is by structural induction on formulas. The term case supplies the base computation needed for atomic formulas, atomic formulas use preservation of equality and relation symbols by the isomorphism, Boolean connectives use the induction hypothesis directly, and quantifiers use the bijectivity of $h$ to transfer witnesses in both directions. [/proofplan] [step:Transport assignments and show that every term commutes with the isomorphism] Let $\mathrm{Var}$ denote the set of variables of the language $L$. For an assignment \begin{align*} s: \mathrm{Var} \to |M|, \end{align*} define the transported assignment \begin{align*} h_*s: \mathrm{Var} &\to |N| \\ y &\mapsto h(s(y)). \end{align*} For an $L$-term $t$, write $t^M[s] \in |M|$ and $t^N[h_*s] \in |N|$ for its interpretation in $M$ and $N$ under the indicated assignments. We prove by structural induction on $t$ that \begin{align*} h(t^M[s]) = t^N[h_*s]. \end{align*} If $t$ is a variable $y$, then $t^M[s]=s(y)$ and $t^N[h_*s]=(h_*s)(y)=h(s(y))$, so the identity holds. If $t$ is a constant symbol $c$, then $t^M[s]=c^M$ and $t^N[h_*s]=c^N$, and preservation of constants by the isomorphism gives $h(c^M)=c^N$. Now suppose \begin{align*} t = F(t_1,\dots,t_k), \end{align*} where $F$ is a $k$-ary function symbol of $L$, and assume the assertion holds for $t_1,\dots,t_k$. Since $h$ preserves the interpretation of $F$, \begin{align*} h(F^M(t_1^M[s],\dots,t_k^M[s])) = F^N(h(t_1^M[s]),\dots,h(t_k^M[s])). \end{align*} Using the induction hypotheses for the terms $t_1,\dots,t_k$, this becomes \begin{align*} h(t^M[s]) = F^N(t_1^N[h_*s],\dots,t_k^N[h_*s]) = t^N[h_*s]. \end{align*} Thus term interpretation commutes with $h$ for every $L$-term. [guided] The reason we begin with terms is that atomic formulas are built out of terms. Let $\mathrm{Var}$ be the set of variables of $L$, and let \begin{align*} s: \mathrm{Var} \to |M| \end{align*} be an assignment. Transporting $s$ through the isomorphism gives the assignment \begin{align*} h_*s: \mathrm{Var} &\to |N| \\ y &\mapsto h(s(y)). \end{align*} For each $L$-term $t$, we claim that interpreting $t$ first in $M$ and then applying $h$ gives the same element as transporting the assignment first and then interpreting $t$ in $N$: \begin{align*} h(t^M[s]) = t^N[h_*s]. \end{align*} We prove this by structural induction on the term $t$. If $t$ is a variable $y$, then its interpretation in $M$ is $s(y)$, while its interpretation in $N$ under $h_*s$ is $(h_*s)(y)=h(s(y))$. Hence \begin{align*} h(t^M[s]) = h(s(y)) = t^N[h_*s]. \end{align*} If $t$ is a constant symbol $c$, then $t^M[s]=c^M$ and $t^N[h_*s]=c^N$. Because $h$ is an isomorphism of $L$-structures, it preserves constant symbols, so \begin{align*} h(c^M)=c^N. \end{align*} For the inductive step, suppose \begin{align*} t = F(t_1,\dots,t_k), \end{align*} where $F$ is a $k$-ary function symbol of $L$. The induction hypothesis says that each argument term already commutes with $h$: \begin{align*} h(t_i^M[s]) = t_i^N[h_*s] \end{align*} for every $i \in \{1,\dots,k\}$. Since $h$ is an isomorphism, it preserves the function symbol $F$, meaning \begin{align*} h(F^M(b_1,\dots,b_k)) = F^N(h(b_1),\dots,h(b_k)) \end{align*} for all $b_1,\dots,b_k \in |M|$. Applying this with $b_i=t_i^M[s]$ gives \begin{align*} h(t^M[s]) &= h(F^M(t_1^M[s],\dots,t_k^M[s])) \\ &= F^N(h(t_1^M[s]),\dots,h(t_k^M[s])) \\ &= F^N(t_1^N[h_*s],\dots,t_k^N[h_*s]) \\ &= t^N[h_*s]. \end{align*} This completes the term induction. [/guided] [/step] [step:Prove the assignment-level invariance for atomic formulas] We prove that for every atomic $L$-formula $\psi$ and every assignment $s:\mathrm{Var}\to |M|$, \begin{align*} M \models \psi[s] \iff N \models \psi[h_*s]. \end{align*} First let $\psi$ be $t_1=t_2$, where $t_1$ and $t_2$ are $L$-terms. Then \begin{align*} M \models t_1=t_2[s] &\iff t_1^M[s]=t_2^M[s] \\ &\iff h(t_1^M[s])=h(t_2^M[s]) \\ &\iff t_1^N[h_*s]=t_2^N[h_*s] \\ &\iff N \models t_1=t_2[h_*s]. \end{align*} The second equivalence uses injectivity of $h$, and the third equivalence uses the term computation from the previous step. Now let \begin{align*} \psi = R(t_1,\dots,t_k), \end{align*} where $R$ is a $k$-ary relation symbol of $L$. Since $h$ is an isomorphism, for all $b_1,\dots,b_k \in |M|$, \begin{align*} M \models R(b_1,\dots,b_k) \iff N \models R(h(b_1),\dots,h(b_k)). \end{align*} Applying this with $b_i=t_i^M[s]$ and using the term computation gives \begin{align*} M \models R(t_1,\dots,t_k)[s] &\iff N \models R(h(t_1^M[s]),\dots,h(t_k^M[s])) \\ &\iff N \models R(t_1^N[h_*s],\dots,t_k^N[h_*s]) \\ &\iff N \models R(t_1,\dots,t_k)[h_*s]. \end{align*} [/step] [step:Extend the invariance through Boolean connectives] Assume inductively that the assignment-level equivalence holds for formulas $\alpha$ and $\beta$. For negation, \begin{align*} M \models \neg \alpha[s] &\iff \text{not }(M \models \alpha[s]) \\ &\iff \text{not }(N \models \alpha[h_*s]) \\ &\iff N \models \neg \alpha[h_*s]. \end{align*} For conjunction, \begin{align*} M \models (\alpha \land \beta)[s] &\iff M \models \alpha[s]\text{ and }M \models \beta[s] \\ &\iff N \models \alpha[h_*s]\text{ and }N \models \beta[h_*s] \\ &\iff N \models (\alpha \land \beta)[h_*s]. \end{align*} The same argument applies to $\lor$, $\to$, and $\leftrightarrow$ when these connectives are taken as primitive; if they are defined abbreviations, their invariance follows from the displayed cases. [/step] [step:Transfer existential and universal witnesses using bijectivity of the isomorphism] Assume inductively that the assignment-level equivalence holds for a formula $\theta$. Let $y$ be a variable, and for $b\in |M|$ define \begin{align*} s[y \mapsto b]: \mathrm{Var} &\to |M| \end{align*} to be the assignment agreeing with $s$ except that it sends $y$ to $b$. For $c\in |N|$, define $(h_*s)[y\mapsto c]:\mathrm{Var}\to |N|$ analogously. For the existential quantifier, first suppose \begin{align*} M \models \exists y\,\theta[s]. \end{align*} Then there exists $b\in |M|$ such that \begin{align*} M \models \theta[s[y\mapsto b]]. \end{align*} The transported assignment satisfies \begin{align*} h_*(s[y\mapsto b]) = (h_*s)[y\mapsto h(b)]. \end{align*} By the induction hypothesis, \begin{align*} N \models \theta[(h_*s)[y\mapsto h(b)]], \end{align*} so \begin{align*} N \models \exists y\,\theta[h_*s]. \end{align*} Conversely, suppose \begin{align*} N \models \exists y\,\theta[h_*s]. \end{align*} Then there exists $c\in |N|$ such that \begin{align*} N \models \theta[(h_*s)[y\mapsto c]]. \end{align*} Since $h$ is surjective, there exists $b\in |M|$ with $h(b)=c$. Hence \begin{align*} (h_*s)[y\mapsto c]=h_*(s[y\mapsto b]). \end{align*} By the induction hypothesis applied in the reverse direction, \begin{align*} M \models \theta[s[y\mapsto b]], \end{align*} and therefore \begin{align*} M \models \exists y\,\theta[s]. \end{align*} Thus existential quantification is invariant. For the universal quantifier, if it is primitive, the argument is analogous. We have \begin{align*} M \models \forall y\,\theta[s] &\iff \text{for every } b\in |M|,\ M \models \theta[s[y\mapsto b]] \\ &\iff \text{for every } b\in |M|,\ N \models \theta[(h_*s)[y\mapsto h(b)]] \\ &\iff \text{for every } c\in |N|,\ N \models \theta[(h_*s)[y\mapsto c]] \\ &\iff N \models \forall y\,\theta[h_*s]. \end{align*} The third equivalence uses that $h:|M|\to |N|$ is bijective. If $\forall$ is defined by $\forall y\,\theta := \neg \exists y\,\neg\theta$, then its invariance follows instead from the already proved cases for negation and existential quantification. [guided] This is the only step where we need the full bijectivity of the isomorphism, rather than merely preservation of symbols. Let $y$ be a variable. For $b\in |M|$, define \begin{align*} s[y \mapsto b]: \mathrm{Var} &\to |M| \end{align*} to be the assignment that sends $y$ to $b$ and agrees with $s$ on every variable other than $y$. For $c\in |N|$, define $(h_*s)[y\mapsto c]:\mathrm{Var}\to |N|$ in the same way. Consider $\exists y\,\theta$. Suppose first that \begin{align*} M \models \exists y\,\theta[s]. \end{align*} By the semantics of the existential quantifier, there is some witness $b\in |M|$ such that \begin{align*} M \models \theta[s[y\mapsto b]]. \end{align*} Transporting the modified assignment gives exactly the modified transported assignment: \begin{align*} h_*(s[y\mapsto b]) = (h_*s)[y\mapsto h(b)]. \end{align*} This equality holds because both assignments send $y$ to $h(b)$ and send every other variable $z$ to $h(s(z))$. The induction hypothesis applied to $\theta$ now gives \begin{align*} N \models \theta[(h_*s)[y\mapsto h(b)]]. \end{align*} Thus $h(b)$ is a witness in $N$, and so \begin{align*} N \models \exists y\,\theta[h_*s]. \end{align*} Conversely, suppose \begin{align*} N \models \exists y\,\theta[h_*s]. \end{align*} Then there is a witness $c\in |N|$ such that \begin{align*} N \models \theta[(h_*s)[y\mapsto c]]. \end{align*} To pull this witness back to $M$, we use surjectivity of $h$. There exists $b\in |M|$ with $h(b)=c$. For this $b$, \begin{align*} (h_*s)[y\mapsto c]=h_*(s[y\mapsto b]). \end{align*} Applying the induction hypothesis in the reverse direction gives \begin{align*} M \models \theta[s[y\mapsto b]]. \end{align*} Therefore $b$ is a witness in $M$, and \begin{align*} M \models \exists y\,\theta[s]. \end{align*} For the universal quantifier, the same mechanism is used for all elements at once. If $\forall$ is primitive, then \begin{align*} M \models \forall y\,\theta[s] &\iff \text{for every } b\in |M|,\ M \models \theta[s[y\mapsto b]] \\ &\iff \text{for every } b\in |M|,\ N \models \theta[(h_*s)[y\mapsto h(b)]]. \end{align*} Because $h$ is bijective, the elements $h(b)$ with $b\in |M|$ are exactly all elements of $|N|$. Hence the last condition is equivalent to \begin{align*} \text{for every } c\in |N|,\ N \models \theta[(h_*s)[y\mapsto c]], \end{align*} which is precisely \begin{align*} N \models \forall y\,\theta[h_*s]. \end{align*} If $\forall y\,\theta$ is instead treated as an abbreviation for $\neg\exists y\,\neg\theta$, then its invariance follows from the already proved invariance of negation and existential quantification. [/guided] [/step] [step:Specialize the assignment-level theorem to the displayed tuple] By structural induction on formulas, the previous steps prove that for every $L$-formula $\psi$ and every assignment $s:\mathrm{Var}\to |M|$, \begin{align*} M \models \psi[s] \iff N \models \psi[h_*s]. \end{align*} Choose an assignment \begin{align*} s: \mathrm{Var} \to |M| \end{align*} such that $s(x_i)=a_i$ for every $i\in\{1,\dots,n\}$. Since all free variables of $\varphi$ are among $x_1,\dots,x_n$, the satisfaction relation for $\varphi$ depends only on the values assigned to these variables. Therefore \begin{align*} M \models \varphi(a_1,\dots,a_n) &\iff M \models \varphi[s] \\ &\iff N \models \varphi[h_*s] \\ &\iff N \models \varphi(h(a_1),\dots,h(a_n)). \end{align*} This is the desired equivalence. [/step]