What does overtness mean for metric spaces?

Question

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

Answer 1

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 subspaces 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 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 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 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. 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$.

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 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.

Answer 2

The spectrum of a commutative ring, defined as the classifying locale of its prime filters, is overt if and only if any element is nilpotent or not nilpotent (Proposition 12.51 in these notes of mine).

Hence for almost any nontrivial base scheme $X$, inside the topos of sheaves over $X$, the spectrum of $\mathcal{O}_X$ will be an example for a locale which is not overt.

In impredicative (constructive or classical) mathematics, you will not find a topological space which would not be overt.

(Note to people familiar with algebraic geometry's relative spectrum construction who would expect $\operatorname{Spec}(\mathcal{O}_X)$ to be the one-point locale (so that it externalizes to $X$ again): The usual localic spectrum construction, when carried out internally in the topos of the base scheme, does not coincide with the relative spectrum construction. But a variant does. Details are in Section 12 of the linked notes.)

Answer 3

To conjure up a non-overt space we must change slightly the definition of topology, since even inuitionistically every space is overt, so long as every union of opens is open.

Let $\Sigma$ be the Sierpinski space, whose underlying set consists of the truth values $\{\bot, \top\}$ and the topology is generated by the basic open $\{\top\}$.

We topologize the topology $\mathcal{O}(X)$ of a space $X$ with the Scott topology.

Definition: A space $X$ is overt when the map $\exists_X : \mathcal{O}(X) \to \Sigma$, defined by $\exists_X(U) = (\exists x \in X . x \in U)$, is continuous.

In other words, $\exists_X(U) = \top$ if, and only if, the open set $U$ is inhabited.

Theorem: Using the traditional definition of topological spaces, every space $X$ is overt.

Proof. Let $X$ be a topological space. We only need to verify that $$\exists_X^{-1}(\{\top\}) = \{U \in \mathcal{O}(X) \mid \exists x \in X \,.\, x \in U\}$$ is Scott-open. But this is easy: it is obviously an upper set (a superset of an inhabited set is inhabited), so we just need to check the directed union condition: if $\bigcup_{i \in I} U_i$ is an inhabited directed union, then obviously there is $i \in I$ such that $U_i$ is inhabited. $\Box$

So far we have not used excluded middle, so simply passing to an intuitionistic setting is not going to help. We need to change the definition of topological spaces.

One possibility is to use locales instead of spaces, in which case overtness is related to the notion of open maps, see Ingo's answer.

Here we will do it a more pedestrian way, by changing the definition of topology so that the above definition of $\exists_X$ becomes invalid for a suitably chosen $X$, which will then be an example of a non-overt space. This can be accomplished in several ways, some of which are more direct than others. Let me just present the main idea, using the setup of computable mathematics, as described by Arno in his answer.

In (one kind of) computable mathematics we require "everything to be computable". In particular, open subsets are not closed under arbitrary unions, but only the computable ones. For example, the discrete topology on $\mathbb{N}$ is generated by taking unions of computable sequences of singletons $\{\{n\} \mid n \in \mathbb{N}\}$, which means that $\mathcal{O}(\mathbb{N})$ will consists of the computably enumerable subsets of $\mathbb{N}$, and not the powerset of $\mathbb{N}$.

As it turns out, in this setting we should think of $\Sigma = \{\bot, \top\}$ as the set of semidecidable truth values, i.e., the computable maps $\mathbb{N} \to \Sigma$ correspond to the computably enumerable subsets of $\mathbb{N}$ (not the computable ones, which we get as maps $\mathbb{N} \to \{0,1\}$ where $\{0,1\}$ has the discrete topology).

Now, consider a subset $X \subseteq \mathbb{N}$ which is not computably enumerable, such as the complement of the Halting set. We again equip it with the discrete topology generated by the singletons $\{\{n\} \mid n \in X\}$. Observe that $X$ is clearly a metric space, even discrete metric space whose (computable) metric is defined by $d(m, n) = \mathsf{if} \; m = n \; \mathsf{then} 1 \; \mathsf{else}\; 0$. The open subsets of $X$ are of the form $S \cap X$ where $S$ is a computably enumerable set. If there were a computable map $\exists_X : \mathcal{O}(X) \to \Sigma$ satisfying $\exists_X(U) = (\exists x \in X \,.\, x \in U)$, then $\{n \in \mathbb{N} \mid n \in X\}$ would be semidecidable, because $n \in X \iff \exists_X(X \cap \{n\}) = \top$. This would make $X$ computably enumerable, which it isn't. Therefore, $X$ is not overt.

Answer 4

In computable analysis, the typical approach to metric spaces is that of a computable metric space. If we assume that there already is some external concept of the metric space we want to handle, we will ask for a particular dense sequence such that we can compute the distance of any two points in that sequence from their indices. Without any prior understanding of the space, we should probably talk about complete spaces only (to avoid confusion over which points exist and which don't exist), so we again start with a sequence with computable distances, and then consider its completion to be the computably Polish space we are talking about.

Either approach means that our spaces by construction have a computable dense sequence, which renders them overt. However, this also means that we do not get that closed (or even $\Pi^0_2$-) subspaces of a computably Polish space are computably Polish themselves. The problem is precisely overtness, because an overt closed subset of a computably (Quasi)Polish space already contains a dense sequence. The metric itself obviously translates to subspaces. Thus, we should be looking at non-overt subspaces of a computable metric space to get the examples you are looking for.

The spaces $2^\omega$ and $\mathbb{N}^\omega$ are particularly illuminating examples of what is happening here. In either space, the usual way to think about a closed set is as the set of infinite paths through some given tree. The set will be overt, if we can choose the tree to be pruned, i.e. have no leaves/deadends. So, the set of infinite paths through Kleene's tree equipped with the distance inherited from $2^\omega$ would be a very much non-overt space in computable analysis.