[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*}
[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]
[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.
[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]
[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]
