[proofplan] Atomic formulas are built from terms by either applying a relation symbol or asserting equality between two terms. The main point is therefore to prove, by structural induction on terms, that evaluating a term in the reduced product gives the equivalence class of the coordinatewise evaluations. Once this term-evaluation fact is established, relation-symbol atoms follow directly from the definition of the relation interpretation in the reduced product, while equality atoms follow directly from the definition of the quotient [equivalence relation](/page/Equivalence%20Relation). [/proofplan]

[step:Evaluate terms in the reduced product coordinatewise]Fix $a_1,\dots,a_n \in \prod_{i \in I} M_i$. Let $\bigsqcup_{i \in I} M_i$ denote the disjoint union of the underlying sets of the structures $M_i$; we use it as a bookkeeping codomain for coordinatewise maps $b: I \to \bigsqcup_{i \in I} M_i$ satisfying $b(i) \in M_i$ for every $i \in I$. For each $L$-term $t(x_1,\dots,x_n)$, define the coordinatewise value \begin{align*} t_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto t^{M_i}((a_1)_i,\dots,(a_n)_i), \end{align*} so that $t_a \in \prod_{i \in I} M_i$. We prove by structural induction on $t$ that \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*} If $t$ is the variable $x_j$, then $t_a=a_j$, and hence \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [a_j]_{\mathcal F} = [t_a]_{\mathcal F}. \end{align*} If $t$ is a constant symbol $c$, then $c^M$ is, by definition of the reduced product structure, the class of the sequence \begin{align*} c_* : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto c^{M_i}. \end{align*} Since $t_a=c_*$, we get $t^M=[t_a]_{\mathcal F}$. Now suppose \begin{align*} t = f(s_1,\dots,s_m), \end{align*} where $f$ is an $m$-ary function symbol of $L$, and assume the induction hypothesis for each term $s_k$. For each $k \in \{1,\dots,m\}$, define \begin{align*} (s_k)_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto s_k^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} The induction hypothesis gives \begin{align*} s_k^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [(s_k)_a]_{\mathcal F}. \end{align*} By the definition of the interpretation of $f$ in the reduced product, \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) &= f^M([(s_1)_a]_{\mathcal F},\dots,[(s_m)_a]_{\mathcal F}) \\ &= [b]_{\mathcal F}, \end{align*} where \begin{align*} b : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto f^{M_i}((s_1)_a(i),\dots,(s_m)_a(i)). \end{align*} For every $i \in I$, \begin{align*} b_i = f^{M_i}\bigl(s_1^{M_i}((a_1)_i,\dots,(a_n)_i),\dots,s_m^{M_i}((a_1)_i,\dots,(a_n)_i)\bigr) = t^{M_i}((a_1)_i,\dots,(a_n)_i), \end{align*} so $b=t_a$. Therefore \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*}[/step]

[guided]The purpose of this step is to justify that terms may be evaluated before or after passing to the reduced product. Fix $a_1,\dots,a_n \in \prod_{i \in I} M_i$. Let $\bigsqcup_{i \in I} M_i$ denote the disjoint union of the underlying sets of the structures $M_i$; this gives a single codomain for coordinatewise maps $b: I \to \bigsqcup_{i \in I} M_i$ whose $i$-th value lies in $M_i$. For an $L$-term $t(x_1,\dots,x_n)$, define its coordinatewise evaluation \begin{align*} t_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto t^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} This is an element of $\prod_{i \in I} M_i$, because for each $i \in I$ the value $t^{M_i}((a_1)_i,\dots,(a_n)_i)$ lies in $M_i$. We prove by induction on the construction of the term $t$ that \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*} First suppose $t=x_j$ for some $j \in \{1,\dots,n\}$. The coordinatewise evaluation of $x_j$ is precisely the sequence $a_j$, since \begin{align*} t_a(i) = (a_j)_i \end{align*} for every $i \in I$. Therefore \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [a_j]_{\mathcal F} = [t_a]_{\mathcal F}. \end{align*} Next suppose $t$ is a constant symbol $c$. In the reduced product, the interpretation of $c$ is defined as the equivalence class of the sequence \begin{align*} c_* : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto c^{M_i}. \end{align*} The coordinatewise value $t_a$ is exactly this same sequence $c_*$. Hence \begin{align*} t^M = [c_*]_{\mathcal F} = [t_a]_{\mathcal F}. \end{align*} Finally suppose $t=f(s_1,\dots,s_m)$, where $f$ is an $m$-ary function symbol. The induction hypothesis applies to each smaller term $s_k$, so for every $k \in \{1,\dots,m\}$, \begin{align*} s_k^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [(s_k)_a]_{\mathcal F}, \end{align*} where \begin{align*} (s_k)_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto s_k^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} Now apply the definition of the reduced-product interpretation of the function symbol $f$. It says that $f^M$ acts on equivalence classes by applying $f^{M_i}$ at each coordinate. Thus \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) &= f^M([(s_1)_a]_{\mathcal F},\dots,[(s_m)_a]_{\mathcal F}) \\ &= [b]_{\mathcal F}, \end{align*} where \begin{align*} b : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto f^{M_i}((s_1)_a(i),\dots,(s_m)_a(i)). \end{align*} For each coordinate $i \in I$, substituting the definitions of the sequences $(s_k)_a$ gives \begin{align*} b_i = f^{M_i}\bigl(s_1^{M_i}((a_1)_i,\dots,(a_n)_i),\dots,s_m^{M_i}((a_1)_i,\dots,(a_n)_i)\bigr). \end{align*} This is exactly the recursive definition of the value of the term $f(s_1,\dots,s_m)$ in $M_i$, so \begin{align*} b_i = t^{M_i}((a_1)_i,\dots,(a_n)_i)=t_a(i) \end{align*} for every $i \in I$. Therefore $b=t_a$, and hence \begin{align*} t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*}[/guided]

[step:Verify atomic formulas defined by relation symbols] Assume \begin{align*} \varphi(x_1,\dots,x_n) = R(t_1(x_1,\dots,x_n),\dots,t_m(x_1,\dots,x_n)), \end{align*} where $R$ is an $m$-ary relation symbol of $L$. Recall that the reduced-product interpretation of $R$ is well-defined on equivalence classes: if representatives are changed on sets belonging to the dual equivalence relation, then the set of coordinates on which all representatives agree lies in $\mathcal F$ by finite-intersection closure, and upward closure of $\mathcal F$ preserves membership of the truth set. For each $k \in \{1,\dots,m\}$, define \begin{align*} (t_k)_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto t_k^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} By the term-evaluation result from the previous step, \begin{align*} t_k^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [(t_k)_a]_{\mathcal F}. \end{align*} Therefore, using the definition of the interpretation of $R$ in the reduced product, \begin{align*} M \models \varphi([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) \end{align*} holds if and only if \begin{align*} \{i \in I : M_i \models R((t_1)_a(i),\dots,(t_m)_a(i))\} \in \mathcal F. \end{align*} Since $(t_k)_a(i)=t_k^{M_i}((a_1)_i,\dots,(a_n)_i)$ for every $i \in I$ and every $k$, this set is exactly \begin{align*} \{i \in I : M_i \models \varphi((a_1)_i,\dots,(a_n)_i)\}. \end{align*} Thus the desired equivalence holds for relation-symbol atomic formulas. [/step]

[step:Verify atomic formulas defined by equality]Assume \begin{align*} \varphi(x_1,\dots,x_n) = (s(x_1,\dots,x_n)=t(x_1,\dots,x_n)), \end{align*} where $s$ and $t$ are $L$-terms. Define \begin{align*} s_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto s^{M_i}((a_1)_i,\dots,(a_n)_i), \end{align*} and \begin{align*} t_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto t^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} By the term-evaluation result, \begin{align*} s^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [s_a]_{\mathcal F}, \qquad t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*} Hence \begin{align*} M \models s([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = t([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) \end{align*} if and only if \begin{align*} [s_a]_{\mathcal F} = [t_a]_{\mathcal F}. \end{align*} By the definition of equality in the quotient, \begin{align*} [s_a]_{\mathcal F} = [t_a]_{\mathcal F} \end{align*} if and only if \begin{align*} \{i \in I : s_a(i)=t_a(i)\} \in \mathcal F. \end{align*} Substituting the definitions of $s_a$ and $t_a$, this is equivalent to \begin{align*} \{i \in I : M_i \models s((a_1)_i,\dots,(a_n)_i)=t((a_1)_i,\dots,(a_n)_i)\} \in \mathcal F, \end{align*} which is precisely \begin{align*} \{i \in I : M_i \models \varphi((a_1)_i,\dots,(a_n)_i)\} \in \mathcal F. \end{align*} Thus the desired equivalence holds for equality atomic formulas.[/step]

[guided]For equality atoms, the reduced-product relation is not given by a relation symbol; it is the actual equality relation in the quotient structure. Let \begin{align*} \varphi(x_1,\dots,x_n) = (s(x_1,\dots,x_n)=t(x_1,\dots,x_n)). \end{align*} Define the two coordinatewise term-value sequences \begin{align*} s_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto s^{M_i}((a_1)_i,\dots,(a_n)_i), \end{align*} and \begin{align*} t_a : I &\to \bigsqcup_{i \in I} M_i \\ i &\mapsto t^{M_i}((a_1)_i,\dots,(a_n)_i). \end{align*} The term-evaluation result proved above gives \begin{align*} s^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [s_a]_{\mathcal F}, \qquad t^M([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = [t_a]_{\mathcal F}. \end{align*} Therefore the equality atom is true in $M$ exactly when these two equivalence classes are equal: \begin{align*} M \models s([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) = t([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) \end{align*} if and only if \begin{align*} [s_a]_{\mathcal F} = [t_a]_{\mathcal F}. \end{align*} Now use the definition of the quotient by the filter. Two sequences represent the same element of the reduced product exactly when they agree on a set belonging to $\mathcal F$. Thus \begin{align*} [s_a]_{\mathcal F} = [t_a]_{\mathcal F} \end{align*} if and only if \begin{align*} \{i \in I : s_a(i)=t_a(i)\} \in \mathcal F. \end{align*} Replacing $s_a(i)$ and $t_a(i)$ by their definitions gives \begin{align*} \{i \in I : M_i \models s((a_1)_i,\dots,(a_n)_i)=t((a_1)_i,\dots,(a_n)_i)\} \in \mathcal F. \end{align*} This is exactly the set of indices at which $M_i$ satisfies the atomic formula $\varphi$ with parameters $((a_1)_i,\dots,(a_n)_i)$. Hence \begin{align*} M \models \varphi([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) \end{align*} if and only if \begin{align*} \{i \in I : M_i \models \varphi((a_1)_i,\dots,(a_n)_i)\} \in \mathcal F. \end{align*}[/guided]

[step:Conclude the equivalence for every atomic formula] Every atomic $L$-formula is either a relation-symbol formula \begin{align*} R(t_1,\dots,t_m) \end{align*} or an equality formula \begin{align*} s=t. \end{align*} The preceding two steps prove the asserted equivalence in each of these two cases. Therefore, for every atomic $L$-formula $\varphi(x_1,\dots,x_n)$ and all $a_1,\dots,a_n \in \prod_{i \in I} M_i$, \begin{align*} M \models \varphi([a_1]_{\mathcal F},\dots,[a_n]_{\mathcal F}) \end{align*} if and only if \begin{align*} \{i \in I : M_i \models \varphi((a_1)_i,\dots,(a_n)_i)\} \in \mathcal F. \end{align*} This proves the Atomic Łoś Lemma for reduced products. [/step]