David Roberts has rubbed the magic lamp and the genie appears!
Even though the notion of overtness does depend on the strength of the ambient logic, I believe the problem here is with the notion of metric space, rather than the choice of a model of mathematics.
The natural answer is that any metric space has enough points and is therefore necessarily overt.
I am inclined to think that any whole space in topology is in practice overt and the interesting question is what overt subspaces look like.
We have a monster (in the sense of Lakatos) that you could use as you please on either side of this argument: The set $A\subset{\mathbb N}$ of programs that don't terminate, with the discrete metric, is not overt.
We can do better than this. Steve Vickers has an alternative to the Cauchy completion in locale theory and formal topology. Like any metric topology, it has a basis of balls $B(x,r)$, where we may take the radii $r$ to be dyadic rationals and the centres $x$ to be (for example) points with dyadic rational coordinates.
(Since I mention Steve, in general he is interested in the hyperspaces of all overt or compact subspaces, which are called the lower and upper powerdomains. My interest, in constrast, is with individual overt subspaces.)
To the general mathematician, the idea of an operator $\lozenge$ that takes unions of open subspaces to the existential quantifier is not very familiar. However, it has a very natural equivalent form when we're working in a metric space constructed in the above way.
Define $d(x)< r \equiv \lozenge B(x,r)$. It is easy to show that this satisfies
$$ d(x)< r'< r \Longrightarrow d(x)< r $$ $$ d(x)< r \Longrightarrow \exists r'.d(x)< r'< r $$ $$ d(x,y)< r \;\land\; d(y)< s \Longrightarrow d(x)< r+s $$ $$ d(x)< r \;\land\; \epsilon\gt 0 \Longrightarrow \exists y.d(x,y)< r \;\land\; d(y)< \epsilon $$ for any $\epsilon>0$
What this means is that $d:X\to\overline{\mathbb R}$ is an upper semicontinuous function, or alternatively one that is valued in the upper real numbers.
This is the essence of the equivalence between overt and located subspaces (the latter are used in Bishop-style constructive analysis), which was stated by Bas Spitters. Unfortunately he only considered the case of closed overt/located subspaces; these are characterised by $d$ being valued in the ordinary (Euclidean, Dedekind, ...) real numbers.
The more general case is covered in my draft paper Overt Subspaces of ${\mathbb R}^n$.
The third condition above is the triangle law. Under suitable conditions, the Newton--Raphson algorithm yields a function $\Delta(x)\cong |f(x)/\dot f(x)|$ that satisfies all the other conditions and a $d$ obeying all of them can easily be derived from it.
My intuition is that an overt subspace is the solution-space of an algorithm. To justify this we need more examples from numerical analysis like Newton--Raphson, but that is very much not my subject.
On the other hand, Newton--Raphson actually yields more information than the $d$ function.
There are two possible responses to this:
- Maybe we should replace overtness with something more quantitative; or
- Maybe an algorithm could be derived from the formula for $\lozenge$ or $d$ together with the proof that it has the appropriate properties.
The second is not completely unreasonable: An overt subspace is a generalisation of a point defined by a Dedekind cut or a completely prime filter. Andrej Bauer pioneered some ideas for Efficient computation with Dedekind reals and had a prototype calculator called Marshall.
Given how widely used the notions of overt, located or recursively enumerable subspaces now are in the different constructive cults, really we ought to have a better story than "overtness is dual to compactness but classically invisible". There ought to be a way of explaining the idea to "ordinary" (classical) mathematicians, in particular numerical analysts.
I have been trying to do this for more than a decade, but I think I'm the wrong person to do it, and probably we can't do it from the constructive side: somehow we have to kidnap a numerical analyst and inculcate them with this idea.
I still have this draft paper (above). Probably I should just stop fussing and publish it. Comments towards that are welcome.