Original question:
For compact metric spaces, plenty of subtly different definitions converge to the same concept. Overtness can be viewed as a property dual to compactness. So is there a similar story for overt metric spaces?


Edit: Since overtness is trivially true assuming the Law of the Excluded Middle, clearly the question is primarily interesting when we do not assume the LEM.


Edit 2: It looks like it is extremely difficult for a metric space to not be overt even in constructive settings. So editing the question to ask if there is ANY model where metric spaces are not overt.


Edit 3: For these reasons I changed the question again, from "Is there any model of mathematics where there exists a metric space that is not overt?". PT



What does overtness mean for metric spaces?
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 question 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, in any sensible logical setting.


Indeed, I am inclined to think that any *whole* space in topology is in practice overt and the interesting question is what **overt *sub*spaces** look like.


Andrej has already pointed out that the set $A\subset{\mathbb N}$ of programs that don't terminate (with the two-valued metric) is not overt.


We can do better than this. [Steve Vickers](https://www.cs.bham.ac.uk/%7Esjv/papersfull.php) 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.


This construction still gives an overt space, because the set (overt discrete space) of centres is dense.


(Since I mention Steve, in general he is interested in the *hyper*spaces 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 definition of overtness using 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](https://arxiv.org/pdf/math/0703561.pdf). Unfortunately, he only considered the case of *closed* overt/located subspaces, which 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$*](http://www.paultaylor.eu/ASD/overtrn).


The third condition above is the triangle law. Under suitable conditions, the **Newton--Raphson algorithm** yields a function $\Delta(x)\equiv |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*](https://mapcommunity.github.io/ictp/presentation_files/Bauer_P.pdf) 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.


