[proofplan] We first verify that $\sim_{\mathcal U}$ is an [equivalence relation](/page/Equivalence%20Relation), so the quotient set used as the universe is well defined. We then show that replacing representatives by $\mathcal U$-equivalent representatives does not change any interpreted symbol. Constants require no representative choice; function symbols respect coordinate agreement on a $\mathcal U$-large finite intersection; and relation symbols have truth sets whose membership in $\mathcal U$ is unchanged after modification on a non-$\mathcal U$-large set. The argument uses only the filter properties of $\mathcal U$, so the well-definedness conclusion in fact holds for any filter, while the theorem states the standard ultraproduct case of an ultrafilter. [/proofplan]

[step:Verify that $\sim_{\mathcal U}$ is an equivalence relation] Define a binary relation $\sim_{\mathcal U}$ on $\prod_{i \in I} M_i$ by declaring, for $a,b \in \prod_{i \in I} M_i$, \begin{align*} a \sim_{\mathcal U} b \quad \Longleftrightarrow \quad \{i \in I : a_i = b_i\} \in \mathcal U. \end{align*} Since $\mathcal U$ is an ultrafilter on $I$, it is a filter on $I$; hence $I \in \mathcal U$, $\mathcal U$ is closed under finite intersections, and $\mathcal U$ is upward closed under inclusion. For reflexivity, let $a \in \prod_{i \in I} M_i$. Then $\{i \in I : a_i = a_i\} = I \in \mathcal U$, so $a \sim_{\mathcal U} a$. For symmetry, if $a \sim_{\mathcal U} b$, then \begin{align*} \{i \in I : b_i = a_i\} = \{i \in I : a_i = b_i\} \in \mathcal U, \end{align*} so $b \sim_{\mathcal U} a$. For transitivity, suppose $a \sim_{\mathcal U} b$ and $b \sim_{\mathcal U} c$. Define \begin{align*} A &:= \{i \in I : a_i = b_i\},\\ B &:= \{i \in I : b_i = c_i\}. \end{align*} Then $A,B \in \mathcal U$, so $A \cap B \in \mathcal U$. If $i \in A \cap B$, then $a_i=b_i=c_i$, and therefore \begin{align*} A \cap B \subset \{i \in I : a_i = c_i\}. \end{align*} By upward closure, $\{i \in I : a_i = c_i\} \in \mathcal U$, so $a \sim_{\mathcal U} c$. Thus $\sim_{\mathcal U}$ is an equivalence relation, and the quotient $\prod_{i \in I} M_i/\mathcal U$ is well defined as a set of equivalence classes. [/step]

[step:Verify that constant symbols are independent of representatives] Let $c \in L$ be a constant symbol. The interpretation \begin{align*} c^M := [(c^{M_i})_{i \in I}]_{\mathcal U} \end{align*} uses the distinguished element $c^{M_i} \in M_i$ in each coordinate and does not involve any input representative. Hence the interpretation of $c$ is a single well-defined element of $M$. [/step]

[step:Show that coordinatewise function symbols respect $\mathcal U$-equivalence] Let $f \in L$ be an $n$-ary function symbol. Let \begin{align*} a_k, \tilde a_k \in \prod_{i \in I} M_i \end{align*} for $1 \leq k \leq n$, and suppose \begin{align*} [a_k]_{\mathcal U} = [\tilde a_k]_{\mathcal U} \end{align*} for every $1 \leq k \leq n$. For each $k$, define the coordinate agreement set \begin{align*} A_k := \{i \in I : (a_k)_i = (\tilde a_k)_i\}. \end{align*} By the definition of $\sim_{\mathcal U}$, each $A_k$ belongs to $\mathcal U$. Since $\mathcal U$ is a filter and filters are closed under finite intersections, the set \begin{align*} A := \bigcap_{k=1}^n A_k \end{align*} belongs to $\mathcal U$. Define two elements $b,\tilde b \in \prod_{i \in I} M_i$ by \begin{align*} b_i &:= f^{M_i}((a_1)_i,\dots,(a_n)_i),\\ \tilde b_i &:= f^{M_i}((\tilde a_1)_i,\dots,(\tilde a_n)_i) \end{align*} for each $i \in I$. If $i \in A$, then $(a_k)_i = (\tilde a_k)_i$ for every $k$, so \begin{align*} b_i = \tilde b_i. \end{align*} Thus \begin{align*} A \subset \{i \in I : b_i = \tilde b_i\}. \end{align*} Because $\mathcal U$ is closed upward and $A \in \mathcal U$, we have \begin{align*} \{i \in I : b_i = \tilde b_i\} \in \mathcal U. \end{align*} Therefore $b \sim_{\mathcal U} \tilde b$, so \begin{align*} [(f^{M_i}((a_1)_i,\dots,(a_n)_i))_{i \in I}]_{\mathcal U} = [(f^{M_i}((\tilde a_1)_i,\dots,(\tilde a_n)_i))_{i \in I}]_{\mathcal U}. \end{align*} Hence $f^M$ is independent of the chosen representatives. [/step]

[step:Prove that relation truth sets are unchanged by $\mathcal U$-large agreement] Let $R \in L$ be an $n$-ary relation symbol. Let \begin{align*} a_k, \tilde a_k \in \prod_{i \in I} M_i \end{align*} for $1 \leq k \leq n$, and suppose $[a_k]_{\mathcal U} = [\tilde a_k]_{\mathcal U}$ for every $k$. Define \begin{align*} A_k &:= \{i \in I : (a_k)_i = (\tilde a_k)_i\},\\ A &:= \bigcap_{k=1}^n A_k. \end{align*} As before, $A \in \mathcal U$. For each $i \in I$, let $R^{M_i} \subset M_i^n$ denote the interpretation of the relation symbol $R$ in the $L$-structure $M_i$. Define the two relation truth sets \begin{align*} S &:= \{i \in I : M_i \models R((a_1)_i,\dots,(a_n)_i)\},\\ T &:= \{i \in I : M_i \models R((\tilde a_1)_i,\dots,(\tilde a_n)_i)\}. \end{align*} Equivalently, $i \in S$ exactly when $((a_1)_i,\dots,(a_n)_i) \in R^{M_i}$, and $i \in T$ exactly when $((\tilde a_1)_i,\dots,(\tilde a_n)_i) \in R^{M_i}$. For every $i \in A$, the two coordinate tuples are equal: \begin{align*} ((a_1)_i,\dots,(a_n)_i) = ((\tilde a_1)_i,\dots,(\tilde a_n)_i). \end{align*} Since $R^{M_i}$ is a relation on $M_i$, equal tuples have the same truth value. Hence \begin{align*} S \cap A = T \cap A. \end{align*} We now prove $S \in \mathcal U \iff T \in \mathcal U$. If $S \in \mathcal U$, then $S \cap A \in \mathcal U$ by closure under finite intersections. Since $S \cap A = T \cap A$ and $T \cap A \subset T$, closure upward gives $T \in \mathcal U$. Conversely, if $T \in \mathcal U$, then $T \cap A \in \mathcal U$ by closure under finite intersections. Since $T \cap A = S \cap A$ and $S \cap A \subset S$, closure upward gives $S \in \mathcal U$. Therefore \begin{align*} S \in \mathcal U \iff T \in \mathcal U. \end{align*} Thus the truth value of \begin{align*} R([a_1]_{\mathcal U},\dots,[a_n]_{\mathcal U}) \end{align*} is independent of the chosen representatives. [/step]

[step:Assemble the interpretations into an $L$-structure] The quotient set $M=\prod_{i \in I}M_i/\mathcal U$ is the underlying set; this quotient is legitimate because $\sim_{\mathcal U}$ was verified to be an equivalence relation. The previous steps show that each constant symbol, function symbol, and relation symbol of $L$ has an interpretation on $M$ that is independent of every representative choice. In those verifications we used only that $\mathcal U$ is a filter, namely that it contains $I$, is closed under finite intersections, and is upward closed under inclusion; these properties follow from the hypothesis that $\mathcal U$ is an ultrafilter. Therefore the coordinatewise interpretations define a well-defined $L$-structure on $\prod_{i \in I} M_i/\mathcal U$, as required. [/step]