The ultrapower construction is a general way of getting a new structure elementarily equivalent to a given one.
It is as explicit as one could hope – the non-constructiveness is, in effect, concentrated entirely in the ultrafilter that the construction takes as an input.
Let $X$ be a set.
This is supposed to be the set of elements of the structure we are interested in.
Let $I$ be a set.
An filter on $I$ is a set $\mathfrak{U}$ of subsets of $I$ that satisfies the following conditions:
- $I \in \mathfrak{U}$.
- If $I_0 \in \mathfrak{U}$ and $I_1 \in \mathfrak{U}$ then $I_0 \cap I_1 \in \mathfrak{U}$.
- If $I_0 \in \mathfrak{U}$ and $I_0 \subseteq I_1 \subseteq I$, then $I_1 \in \mathfrak{U}$.
For example, the set of cofinite subsets of $I$, i.e. $\{ I' \subseteq I : I \setminus I' \text{ is finite} \}$, is a filter on $I$.
Given $x_0$ and $x_1$ in $X^I$, define $x_0 = x_1 \pmod{\mathfrak{U}}$ to mean that $\{ i \in I : x_0 (i) = x_1 (i) \} \in \mathfrak{U}$.
It is straightforward to verify that this is an equivalence relation on $X^I$.
The filterpower $X^I / \mathfrak{U}$ is defined to be the set $X^I$ modulo this equivalence relation.
It is clear that given a map $f : X \to Y$, the induced map $f^I : X^I \to Y^I$ respects equality modulo $\mathfrak{U}$, so we get an induced map $f^I / \mathfrak{U} : X^I / \mathfrak{U} \to Y^I / \mathfrak{U}$.
So, by considering the projections $X \times Y \to X$ and $X \times Y \to Y$, we obtain a natural map $(X \times Y)^I / \mathfrak{U} \to (X^I / \mathfrak{U}) \times (Y^I / \mathfrak{U})$.
It is straightforward to verify that this is a bijection.
Thus, any binary operation on $X$, i.e. any map $X \times X \to X$, induces a binary operation on $X^I / \mathfrak{U}$ in a natural way.
Similarly for $n$-ary operations in general, for all finite $n$.
It is also clear that if $f : X \to Y$ is injective then $f^I / \mathfrak{U} : X^I / \mathfrak{U} \to Y^I / \mathfrak{U}$ is also injective.
Thus, any $n$-ary relation on $X$ induces an $n$-relation on $X^I / \mathfrak{U}$ in a natural way, for all finite $n$.
More concretely, given $x_0, \ldots, x_{n-1}$ in $X^I$ and some $n$-ary relation $R$ on $X$, the induced $n$-ary relation $R^I / \mathfrak{U}$ on $X^I / \mathfrak{U}$ relates the images of $x_0, \ldots, x_{n-1}$ in $X^I / \mathfrak{U}$ if and only if $\{ i \in I : (x_0 (i), \ldots, x_{n-1} (i)) \in R \} \in \mathfrak{U}$.
Hence, if $X$ carries a $\Sigma$-structure for some finitary signature $\Sigma$, then $X^I / \mathfrak{U}$ has a natural induced $\Sigma$-structure.
Moreover, this makes the diagonal embedding $X \to X^I / \mathfrak{U}$ into a homomorphism of $\Sigma$-structures.
The remarkable fact is this:
Theorem (Łoś).
If $\mathfrak{U}$ is an ultrafilter on $I$, i.e. $\mathfrak{U}$ is a filter on $I$ such that, for every $I' \subseteq I$, either $I' \in \mathfrak{U}$ or $I \setminus I' \in \mathfrak{U}$, then the diagonal embedding $X \to X^I / \mathfrak{U}$ is an elementary equivalence of $\Sigma$-structures.
Since the construction of $X^I / \mathfrak{U}$ as a set does not depend on $\Sigma$, we could just as well take $\Sigma$ to be the signature consisting of all $n$-ary operations on $X$ and $n$-ary relations on $X$.
This means it is possible to equip $X^I / \mathfrak{U}$ with any and all (finitary first order) structure that $X$ has, in a way that makes $X^I / \mathfrak{U}$ satisfy exactly the same (first order) properties as $X$.
In particular we could do so for $X = \mathbb{N}$ and obtain on $X^I / \mathfrak{U}$ not only the structure of a model of Peano arithmetic but also a linear order (with a least element and no greatest element), a rig structure, etc.
But could it be that $X \to X^I / \mathfrak{U}$ is actually an isomorphism?
Well, if $\mathfrak{U}$ is a principal ultrafilter, i.e. there is $i \in I$ such that $\mathfrak{U} = \{ I' \subseteq I : i \in I' \}$, then the diagonal embedding $X \to X^I / \mathfrak{U}$ is a bijection.
However, if $I$ is infinite, we can apply Zorn's lemma to deduce that a non-principal ultrafilter on $I$ exists: it is easy to check that any maximal proper filter on $I$ is an ultrafilter, and if $I$ is infinite then the cofinite filter is proper, hence contained in an ultrafilter; but an ultrafilter containing the cofinite filter cannot be principal.
If $\mathfrak{U}$ is an ultrafilter on $I$ containing the cofinite filter and $X$ has at least two distinct elements, then it is straightforward to see that $X \to X^I / \mathfrak{U}$ is not surjective.
We may think of those elements of $X^I / \mathfrak{U}$ that are in the image of the diagonal embedding as standard elements and those that are not are non-standard elements.
For example, let $X = I = \mathbb{N}$.
Then, $x (i) = i$ defines a non-standard element $x$ of $X^I / \mathfrak{U}$.
Abusing notation somewhat, we may identify elements of $X$ with the corresponding standard elements of $X^I / \mathfrak{U}$.
Clearly, for any $n \in \mathbb{N}$, $\{ i \in I : n < x (i) \} \in \mathfrak{U}$, so we have $n < x$ in $X^I / \mathfrak{U}$ for all $n \in \mathbb{N}$; in words, $x$ is greater than any standard element!
More generally, for a fixed finite $n$, given any set $\Phi$ of $n$-ary predicates on $X$ such that every finite subset is simultaneously satisfiable, by choosing $I$ and $\mathfrak{U}$ appropriately, we may find an explicit $n$-tuple of elements of $X^I / \mathfrak{U}$ satisfying all of $\Phi$ simultaneously.
The trick is to choose $I = X^n$.
Consider the set of all $I' \subseteq I$ such that there exists a finite subset $\Phi' \subseteq \Phi$ such that $I'$ contains the set of all $n$-tuples of elements of $X$ that simultaneously satisfy $\Phi'$.
This is a proper filter on $I$, so is contained in some ultrafilter $\mathfrak{U}$.
Let $x_j : I \to X$ be the $j$-th projection $X^n \to X$.
Then $(x_0, \ldots, x_{n-1})$, considered as an $n$-tuple of elements of $X^I / \mathfrak{U}$, simultaneously satisfies all of $\Phi$: indeed, for each $\phi \in \Phi$, the set of all $i \in I$ that satisfy $\phi (x_0 (i), \ldots, x_{n-1} (i))$ is in $\mathfrak{U}$, so we have $\phi (x_0, \ldots, x_{n-1})$ in $X^I / \mathfrak{U}$ as required.