Łoś's Theorem

== Theorem ==
Let $\LL$ be a language.
Let $I$ be an infinite set.
Let $\UU$ be an ultrafilter on $I$.
Let $\map \phi {v_1, \ldots, v_n}$ be an $\LL$-formula.
Let $\MM$ be the ultraproduct:
:$\ds \paren {\prod_{i \mathop \in I} \MM_i} / \UU$
where each $\MM_i$ is an $\LL$-structure.
Then, for all $m_1 = \paren {m_{1, i} }_\UU, \dots, m_n = \paren {m_{n, i} }_\UU$ in $\MM$:
:$\MM \models \map \phi {m_1, \ldots, m_n}$
:
:the set $\set {i \in I: \MM_i \models \map \phi {m_{1, i}, \ldots, m_{n, i} } }$ is in $\UU$.
In particular, for all $\LL$-sentences $\phi$, we have that:
:$\MM \models \phi$ $\set {i \in I: \MM_i \models \phi}$ is in $\UU$.
== Proof ==
We prove the $\LL$-sentences case by induction on the complexity of formulas. The general case trivially follows this proof. 
We appeal to the interpretations of language symbols in the ultraproduct when viewed as an $\LL$-structure, the properties of ultrafilters, and make use of the Axiom of Choice.
The theorem holds trivially for statements of equality of terms and for relations, by definition of how to interpret language symbols for the ultraproduct.
Suppose the theorem holds for $\psi_0$ and $\psi_1$.
If $\phi$ is $\neg \psi_0$:
We are assuming that $\MM \models \psi_0$ :
:$\set {i: \MM_i \models \psi_0} \in \UU$.
Thus:
:$\MM \models \phi$ $\set {i: \MM_i \models \psi_0} \notin \UU$
follows by negating both sides of this statement.
Since $\UU$ is an ultrafilter, a set is absent from $\UU$ the set's complement is present in $\UU$.
So, we may again rewrite the above statement equivalently as:
:$\MM \models \phi \iff I \setminus \set {i: \MM_i \models \psi_0} \in \UU$
Finally, we can further rewrite this set difference to see that:
:$\MM \models \phi \iff \set {i: \MM_i \models \phi} \in \UU$
which is the statement that the theorem holds for $\phi$.
Let $\phi$ be $\psi_0 \wedge \psi_1$:
For both $k \in \set {0, 1}$, we are assuming that:
:$\MM \models \psi_k \iff \set {i: \MM_i \models \psi_k} \in \UU$
By choice of $\phi$, we have $\MM \models \phi$ $\MM \models \psi_0 \wedge \psi_1$.
The right side of this statement can be rewritten as $\MM \models \psi_0$ and $\MM \models \psi_1$.
Thus, using the inductive hypothesis stated above for each $\psi_k$:
:$\MM \models \phi \iff \set {i: \MM_i \models \psi_0} \in \UU$ and $\set {i: \MM_i \models \psi_1} \in \UU$
Since $\UU$ is a filter, it is closed under intersections, and hence the right side of this statement can be written as:
:$\set {i: \MM_i \models \psi_0 \text{ and } \MM_i \models \psi_1} \in \UU$
Thus:
:$\MM \models \phi \iff \set {i: \MM_i \models \phi} \in \UU$
which is the statement that the theorem holds for $\phi$.
Let $\phi$ be $\exists x \map {\psi_0} x$:
If $x$ is not free in $\psi_0$ then earlier cases cover this, so we may assume $x$ is free in $\psi_0$.
We are assuming then that for all $m = \sequence {m_i}_\UU$ in $\MM$:
:$\MM \models \map {\psi_0} m \iff \set {i \in I: \MM_i \models \map {\psi_0} {m_i} } \in \UU$
Thus:
:$\MM \models \phi \iff \exists m = \sequence {m_i}_\UU \in \MM$
for which:
:$\set {i \in I: \MM_i \models \map {\psi_0} {m_i} } \in \UU$
One direction of the theorem follows easily, since this above statement gives us the witnesses $m_i$:
:$\MM \models \phi \implies \set {i \in I: \MM_i \models \map {\psi_0} {m_i} } \in \UU$
And this above set is included in the set we're looking for, so that is an element of the ultrafilter as well:
:$\set {i \in I: \MM_i \models \map {\psi_0} {m_i} } \subseteq \set {i \in I: \MM_i \models \exists x \map {\psi_0} x} \in \UU$
For the converse, we need to find some appropriate $\sequence {m_i}_\UU$ in order to apply the above biconditional statement.
To this end, let $\set {i \in I: \MM_i \models \exists x \map {\psi_0} x} \in \UU$, and apply the Axiom of Choice as follows:
Select for each $i \in \set {i \in I: \MM_i \models \exists x \map {\psi_0} x}$ a witness $m_i \in \MM_i$ such that $\MM_i \models \map {\psi_0} {m_i}$
Select for each $i$ not in this set an arbitrary element $m_i$ of $\MM_i$.
Taking $\sequence {m_i}_\UU$ as our element of $\MM$ then allows us to apply the above biconditional statement and complete the proof.
Category:Model Theory for Predicate Logic