I was looking at applying the ideas in the paper On Nonstandard Topology to Uniform spaces. Given a uniform space $(X,\Phi)$, we can define the relation $\approx$ on ${}^*X$ as follows $$\approx \, = \bigcap \{{}^*U:U \in \Phi \}$$
For example, if $(X,\Phi)$ is the real numbers with their ordinary uniform structure, then $x \approx y$ iff $x-y$ is an infinitesimal in the hyperreal numbers. If we use the metric $|x^3 - y^3|$ instead of the real numbers ordinary $|x - y|$ metric, then $H + \frac 1H \not \approx H$ for infinite $H$ (although $H + \frac 1{H^3} \approx H$).
In fact, it appears that we can prove that $\approx$ is an entourage (i.e. $\approx \, \in {}^*\Phi$). Take the following statements
- The statement "$V \in \Phi$"
- The statement "$V \subseteq U$" for each $U \in \Phi$.
By the third property of entourages, any finite number of these statements is satisfiable. Therefore, by the Saturation property, there is nonstandard $V$ that satisfies the transfer of all these statements. In particular, $V \in {}^* \Phi$. Additionally, $V \subseteq \, \approx$. By the second property of entourages, $\approx$ is therefore an entourage.
Is my proof correct though? The issue is that, going back to the real line with its usual uniform structure, we can assign each entourage a $V$ "diameter", defined as the supremum of the distances between points $x$ and $y$ such that $(x,y) \in V$. Therefore, we should be able to assign either a hyperreal number of $\infty$ to $\approx$ like this, but we can't really. It is less than every positive non-infinitesimal (so in particular is not $\infty$), but greater than every infinitesimal.
So, what's going on? Is $\approx$ actually an entourage?
Your proof would be correct if you knew that $\approx$ is an internal set. However, it usually won't be, and if it is not an internal set, it certainly can't be an element of ${}^*\Phi$. Indeed the contradiction you reached shows that for the usual uniformity on the real line, $\approx$ cannot be internal.
To be clear, ${}^*\Phi$ is not a uniformity in the most literal set-theoretic sense. Rather, it satisfies the version of the definition of a uniformity you get by applying Transfer to the usual definition. In particular, the usual definition involves quantification over all subsets of $X\times X$ (i.e., elements of $\mathcal{P}(X\times X)$), and this will turn into a quantification over all internal subsets of ${}^*X\times {}^*X$ (since those are the elements of ${}^*\mathcal{P}(X\times X)$).