My question is about the concept of nonstandard metric space that would arise from a use of the nonstandard reals R* in place of the usual R-valued metric.
That is, let us define that a topological space X is a nonstandard metric space, if there is a distance function, not into the reals R, but into some nonstandard R* in the sense of nonstandard analysis. That is, there should be a distance function d from X2 into R*, such that d(x,y)=0 iff x=y, d(x,y)=d(y,x) and d(x,z) <= d(x,y)+d(y,z). Such a nonstandard metric would give rise to the nonstandard open balls, which would generate a metric-like topology on X.
There are numerous examples of such spaces, beginning with R* itself. Indeed, every metric space Y has a nonstandard analogue Y*, which is a nonstandard metric space. In addition, there are nonstandard metric spaces that do not arise as Y* for any metric space Y. Most of these examples will not be metrizable, since we may assume that R* has uncountable cofinality (every countable set is bounded), and this will usually prevent the existence of a countable local basis. That is, the nested sequence of balls around a given point will include the balls of infinitesimal radius, and the intersection of any countably many will still be bounded away from 0. For example, R* itself will not be metrizable. The space R* is not connected, since it is the union of the infinitesimal neighborhoods of each point. In fact, one can show it is totally disconnected.
Nevertheless, it appears to me that these nonstandard metric spaces are as useful in many ways as their standard counterparts. After all, one can still reason about open balls, with the triangle inequality and whatnot. It's just that the distances might be nonstandard. What's more, the nonstandard reals offer some opportunities for new topological constructions: in a nonstandard metric space, one has the standard-part operation, which would be a kind of open-closure of a set---For any set Y, let Y+ be all points infinitesimally close to a point in Y. This is something like the closure of Y, except that Y+ is open! But we have Y subset Y+, and Y++=Y+, and + respects unions, etc.
In classical topology, we have various metrization theorems, such as Urysohn's theorem that any second-countable regular Hausdorff space is metrizable.
Question. Which toplogical spaces admit a nonstandard metric? Do any of the classical metrization theorems admit an analogue for nonstandard metrizability? How can we tell if a given topological space admits a nonstandard metric?
I would also be keen to learn of other interesting aspects of nonstandard metrizability, or to hear of interesting applications.
I have many related questions, such as when is a nonstandard metric space actually metrizable? Is there any version of R* itself which is metrizable? (e.g. dropping the uncountable cofinality hypothesis)