I am familiar with the construction of the hyperreal numbers $^*\mathbb{R}$ as an extension of $\mathbb{R}$ built of equivalence classes of real sequences up to equivalence with respect to some fixed non-principal ultrafilter, but it's never felt satisfying to me given its inherent noncomputability.
A "real-world" context in which I see everyday objects behaving like elements of $^*\mathbb{R}$ comes up when I think about Big-O (technically I mean Big-$\Theta$ but let's run with the standard abuse of notation). For instance the set of functions $\{n^\alpha \mid \alpha \in \mathbb{R}_{\geq 0}\}$ up to Big-O equivalence can be identified with $\mathbb{R}_{\geq 0}$ via $\alpha \leftrightarrow n^\alpha$. From this view the function $\log(n)$ behaves like an infinitesimal since it grows more slowly than $n^\alpha$ for any $\alpha>0$, but faster than $n^0$.
Of course, ignoring Big-O equivalence, these functions themselves, and in fact any functions which come up when studying computational complexity, are nothing more than sequences of real numbers and so may in fact be thought of as hyperreal numbers under the ultrapower construction. Moreover, one may play around further by restricting $\alpha$ to, say, the set of computable real numbers. This idea has been a starting point for me in pursuit of a countable dense and hopefully computable subset of hyperreal numbers. A necessary condition for this to work is that $^*\mathbb{R}$ be separable, and this is one of my questions.
Sidenote: I guess I could be wrong but I would assume that the way to topologize $^*\mathbb{R}$ in the ultrapower construction is to take the natural product topology on sequences $\mathbb{N}\to\mathbb{R}$, and then quotient by the ultrafilter equivalence. So two sequences are close iff their first $N$ terms are pairwise within $\epsilon$ of each other, for some $N\in\mathbb{N}$ and $\epsilon\in\mathbb{R}$.
Question 1
Anyway, I haven't been able to prove but wonder if and hope the bold claim below is true. It would imply that $\mathbb{R}$ is not only separable but contains a computable dense subset.
Bold claim: Let $A$ be the set of computable real numbers (so $A$ is in particular a countable dense subset of $\mathbb{R}$). Let $B$ be the set of computable functions from $\mathbb{N}\to A$ (i.e., computable sequences of elements of $A$). Note that $B$ is countable. Fix a nonprincipal ultrafilter and construct $^*\mathbb{R}$ as usual. Then $^*B$, the image of $B$ in $^*\mathbb{R}$, is dense.
Question 2
Failing that, is $^*\mathbb{R}$ separable or not separable by some other (ideally constructive but potentially nonconstructive) argument?
Best Answer
The non-computability of the number system in infinitesimal analysis is a bit of a mirage (as is the philosophical interpretation of Tennenbaum's theorem; see this publication, Section 5.10.5). In axiomatic approaches to infinitesimal analysis, we work in $\mathbb R$ and infinitesimals (and unlimited numbers) are found there. In fact, recently it turned out that infinitesimal analysis is as effective as classical non-infinitesimal approaches to analysis; see this introduction.
To elaborate, philosophical interpretations of Tennenbaum's theorem tend to assume that the ZF foundations are the correct starting point for interpreting computability. This is an assumption that can be challenged. The cardinal point here is that Tennenbaum's theorem is just as true in ZF as it is in SPOT, where $\mathbb N$ includes unlimited (nonstandard) integers. The addition and multiplication operations in this $\mathbb N$ are computable in the usual sense; by Tennenbaum's theorem, if one constructs nonstandard extensions $\mathbb N^\ast$ of $\mathbb N$, the operations there will not be computable. But one doesn't need to extend, since one can do analysis with infinitesimals and unlimited numbers already in $\mathbb N$ and $\mathbb R$, and, furthermore, effectively, as mentioned above.
Since some users seem to be having difficulty accessing my homepage, I provide the information for the relevant papers:
Hrbacek, K.; Katz, M. "Infinitesimal analysis without the Axiom of Choice." Annals of Pure and Applied Logic 172 (2021), no. 6, 102959. https://doi.org/10.1016/j.apal.2021.102959, https://arxiv.org/abs/2009.04980, https://mathscinet.ams.org/mathscinet-getitem?mr=4224071
Hrbacek, K.; Katz, M. "Effective infinitesimals in ℝ." Real Analysis Exchange 48 (2023), no. 2, 365-380. https://arxiv.org/abs/2305.09672, https://doi.org/10.14321/realanalexch.48.2.1671048854
The easiest way to see that the hyperreals are not separable is because there are uncountably many galaxies.