Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-22T09:07:25.206Z Has data issue: false hasContentIssue false

COMPUTABLY COMPACT METRIC SPACES

Published online by Cambridge University Press:  11 May 2023

RODNEY G. DOWNEY
Affiliation:
SCHOOL OF MATHEMATICS AND STATISTICS VICTORIA UNIVERSITY OF WELLINGTON WELLINGTON, NEW ZEALAND E-mail: [email protected] E-mail: [email protected] E-mail: [email protected]
ALEXANDER G. MELNIKOV
Affiliation:
SCHOOL OF MATHEMATICS AND STATISTICS VICTORIA UNIVERSITY OF WELLINGTON WELLINGTON, NEW ZEALAND E-mail: [email protected] E-mail: [email protected] E-mail: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

We give a systematic technical exposition of the foundations of the theory of computably compact metric spaces. We discover several new characterizations of computable compactness and apply these characterizations to prove new results in computable analysis and effective topology. We also apply the technique of computable compactness to give new and less combinatorially involved proofs of known results from the literature. Some of these results do not have computable compactness or compact spaces in their statements, and thus these applications are not necessarily direct or expected.

Type
Articles
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2023. Published by Cambridge University Press on behalf of The Association for Symbolic Logic

1. Introduction

1.1. Compactness

Compactness plays a central role in classical analysis. We don’t have space to talk about all the applications of compactness in analysis, but refer the reader to the survey [Reference Hewitt60] for a detailed discussion. Compactness allows us to have an intrinsic connection between the infinite and the discrete finite instances of problems. In the words of Hewitt [Reference Hewitt60],

“A great many propositions of analysis are:

  • trivial for finite sets;

  • true and reasonably simple for infinite compact sets;

  • either false of extremely difficult to prove for noncompact sets.”

If the reader thinks about any basic course in analysis, they will be struck about how many elementary theorems about real analysis rely on compactness in some form or another. When we turn to analysis on more general spaces, again compactness plays a central role. Classically, compact metric spaces are perhaps the most well-understood separable spaces after the discrete ones. Metrizable compact manifolds and compact topological groups have been studied extensively.

1.2. Goals

The concern of this paper is computable analysis; specifically computability aspects of Polish spaces (complete separable metric spaces). In this paper we will hope to achieve three goals.

  • We will give a unified and smooth account of uses of compactness in computable analysis. This will involve the unification of a number of disparate approaches offered by many authors down through the years. We will describe and improve the fundamental techniques associated with computable compactness that are scattered throughout the literature.

  • We will apply this machinery to prove several new results. This includes a characterization of recursive profinite groups in terms of computable compactness and a new computation of Čech cohomology. We will also give new simplified proofs of some known results (more details below).

  • We will offer an answer to the following question:

    “What is the ‘correct’ notion of computability for a compact Polish(able) topological space?”

    In contrast with the situation for computable discrete algebra, the situation for Polish spaces is not clear especially if we are willing to view them up to homeomorphism.

1.3. Historical context

The roots of computable analysis go back to the early twentieth century (see, e.g., [Reference Borel12]). In his seminal papers [Reference Turing143, Reference Turing144], Turing clarified this early intuition. He gave the first universally accepted formal definition of a computable function. Turing used this definition to solve the Hilbert’s Entscheidungsproblem. But Turing also introduced computable analysis on $[0,1]$ . He analysed computable functions on the field of computable real numbers. He defined a real $\xi $ to be computable if there is a Turing machine that, on input i, outputs a rational $r=\frac {m}{n}$ such that $|\xi -r| < 2^{-i}$ . This approach was pursued especially in Russia by Markov and his school, culminating in Aberth’s book [Reference Aberth1]. Strangely, Turing’s definition of a computable function (i.e., on the computable reals) is now usually referred to as Markov computability. Our paper lies in the tradition of what has become known as “type 2” computable analysis. This tradition goes back to the work of Grzegorczyk [Reference Grzegorczyk55Reference Grzegorczyk57] and Kleene [Reference Kleene79]. In this approach, we view effective functions as computable operators that are not restricted to computable reals and work for arbitrary reals. Avigad and Brattka [Reference Avigad and Brattka4] give an excellent overview of the development of computable analysis from the work of Turing.

The majority of early research was restricted to computability on the real line and in $\mathbb {R}^n$ . In these spaces, the rationals and the tuples of rationals can be used to define computable points. This idea can be extended to more general spaces, as follows. For an abstract Polish space, we fix a dense sequence and require that we have a distance function which is a computable on the dense set. For example, as above, we could use polynomials with rational coefficients in $C[0,1]$ . (Precise definitions will be found in Section 2.) Within this setting, computability-theoretic aspects of metric and normed spaces have also been studied for many decades; some of the earlier references include [Reference Myhill109, Reference Pour-El and Caldwell122, Reference Pour-El and Richards123].

Computability-theoretic aspects in the Euclidean and the totally disconnected ultrametric cases, particularly Cantor space $2^\omega $ , have been of central importance. The Euclidean case—in the sense that the space is actually a subset of $\mathbb {R}^n$ for some n—is treated in [Reference Braverman and Yampolsky22, Reference Ko81, Reference Pour-El and Richards124, Reference Weihrauch146]. The ultrametric case—and more specifically the study of effectively closed subsets of Cantor space—is a well-developed classical subject of computability theory with surveys such as [Reference Cenzer29, Reference Cenzer and Remmel30]. This subdivision is of course a bit artificial since Cantor space can be viewed as a subset of $[0,1]$ , but the metric will no longer be an ultrametric.

In the past decade or two there has been an increasing interest in the computability-theoretic aspects of abstract metric spaces. The central questions in such investigations include:

  • When does a space admit a computable presentation, and in what sense is it computable?

  • Can we compute certain invariants or objects associated with this space (e.g., the space of probability measures on the space), and if “yes” then in what sense?

  • Can we establish computable analogues of the classical topological results?

  • Can we classify computable points in computable topological spaces?

  • Can we classify computably presentable spaces in a given class? etc.

The computability-theoretic study of abstract metric and topological spaces is developing hand in hand with work on reverse mathematics [Reference Mummert107], algorithmic randomness [Reference Hoyrup and Rojas63], enumeration degree theory [Reference Pauly118], and (to some extent) effective descriptive set theory [Reference Moschovakis106]. The notion of a computable presentation of a space is central in such investigations. Many classical spaces such as $2^{\omega }$ and $L^2[0,1]$ are equipped with a “natural” computability structure which is usually fixed; the theory is then developed for the fixed computability structure. The two classical texts [Reference Pour-El and Richards124, Reference Weihrauch146] essentially take this approach. Even though both books talk about ways to compare different computability structures on a fixed space, the space under consideration is usually equipped with a few “natural” computability structures that can be compared. For example, in $C[0,1]$ one could use polynomials with rational coefficients or, alternatively, piecewise linear functions with rational parameters; these turn out to be equivalent (in a rather strong sense). But of course, not every space has a computable presentation simply from cardinality-theoretic observations. Can we describe those spaces that do admit computable presentations, at least from some common classes? For instance, for which compact Polish K does the Banach space $C(K)$ have a computable presentation? What about the space of probability measures on K? etc.

To attack these and similar questions we will often have to depart from classical computable analysis (that deals with fixed “natural” computable presentations) and use methods of computable topology. Although we can point at earlier initiatives such as, e.g., [Reference Kalantari and Weitkamp73Reference Kalantari and Weitkamp75, Reference Nogina114, Reference Nogina115, Reference Spreen139Reference Spreen and Young141], most of the related work in computable topology is more recent and includes [Reference Čelar and Iljazović28, Reference Gavruskin and Nies48, Reference Hoyrup, Kihara and Selivanov62, Reference Kalantari and Welch76, Reference Korovina and Kudinov85, Reference Kudinov and Selivanov87, Reference Weihrauch and Grubba148]. Computable topology is notorious for its zoo of various notions of computability for a topological space. In contrast with effective algebra [Reference Ash and Knight3, Reference Ershov and Goncharov41] where all standard notions of computable presentability had been separated more than half-a-century ago (e.g., [Reference Feiner42]), some of the key notions of computable presentability in topology have been separated only very recently [Reference Bazhenov, Harrison-Trainor and Melnikov8, Reference Harrison-Trainor, Melnikov and Ng59, Reference Hoyrup, Kihara and Selivanov62, Reference Lupini, Melnikov and Nies91]; these results will be discussed in detail later in the paper.

In the recent years there has been a tendency to focus on the three main notions of computable presentability of a (compact) Polish space: a computable Polish space, a computable topological space, and a computably compact space. Our paper is focused on one of these three important notions of computable presentability, namely computable compactness that is defined and discussed below. Computable compactness is clearly restricted to compact Polish spaces. Nonetheless, we will see that the notion and the techniques associated with it have far-reaching applications in computable analysis that are not restricted to compact spaces.

1.4. Computable compactness

Recall that we mentioned that the notion of a computable Polish space, or a computably metrized space, seems to be the most well-established notion of computable presentability for a Polish(able) space. The early classical works on computable metric spaces include [Reference Ceitin27, Reference Lacombe88, Reference Moschovakis105]. A Polish space is computable or computably completely metrized if there is a complete, compatible metric d and a dense subset of special or ideal points $(x_i)_{i \in \omega }$ of the space such that $d(x_i, x_j)$ are computable reals uniformly in i and j. If we view spaces up to isometry, we fix the metric; if we study them up to homeomorphism then we assume d is compatible. In the present article, we assume the metric to be complete, since in all examples that we care about it will indeed be such. For instance, compact metric spaces are complete and separable.Footnote 1 However, the issue is that in a computably metrized compact space, we do not necessarily have computable access to its finite covers.

Classical uses of compactness do not need an understanding of how finite covers are obtained. For classical purposes, it is sufficient that the finite covers exist. Thus, when we consider computability aspects of compact spaces, it is natural to quantify what we mean by this. There are many definitions of a space being computably compact throughout the literature. Remarkably, as we prove below, they—as well as some new useful ones—are all equivalent. For instance, Mori, Tsujii, and Yasugi [Reference Mori, Tsujii and Yasugi104] say that a computably metrized space is computably compact (or effectively compact) if there is a computable function which takes n and produces a finite $2^{-n}$ -cover of the space by open balls centred in special points and having rational radii. (Such balls are called basic.)

The notion has proven to be extremely useful, and the techniques associated with computable compactness tend to be elegant. Indeed, it is not uncommon that a tedious and technical proof in computable analysis becomes transparent and compact (pun intended) after a thoughtful application of computable compactness.

In spite of the usefulness of computable compactness and its numerous applications in the literature, it seems there is not many “standard” references that would contain a systematic exposition of the most fundamental results and techniques associated with computable compactness. Even though these are some excellent papers and Ph.D. theses written on related subjects (e.g., [Reference Brattka and Presser19, Reference Iljazović and Kihara67, Reference Miller103, Reference Pauly117]), many results and proofs are scattered throughout the literature. As a result, it seems that some fundamental facts about computably compact spaces keep being rediscovered over and over again. Proofs of some results in the literature (including some recent ones) can be significantly simplified via choosing a more careful set-up in which computable compactness can be used to simplify combinatorics. It seems that some of the standard techniques associated with computable compactness are not necessarily uniformly known, and perhaps even that the theory itself is a bit under-appreciated.

Thus, as mentioned above, our first main goal of this article is to fill this apparent gap in the literature, at least partially. Once we accumulate enough techniques and develop new ones, we will apply this machinery to prove new results and improve known proofs; this is our second main goal. Recall that our third goal is to try to suggest a correct notion of computable compact Polish space. The potential candidates for the “correct” computability notion include a computable topological space, a computably metrized space, and computably compact space, and some other perhaps more exotic notions—such as a right-c.e. (upper-semicomputable) metric spaces—that can be found in the literature and some of which will be mentioned later. We suggest that the following might be true:

Computable compactness is the right notion of computability for compact Polish spaces.

Even if the reader will disagree with this thesis after looking at the results that we present here, the definition of computable compactness is certainly robust. More formally, Theorem 1.1 contains eight equivalent formulations of computable compactness some of which are new. Many of the applications that we discuss in this article—perhaps most notably the recently discovered effective Stone and Pontryagin dualities—strongly suggest that our thesis should not be dismissed even if we view spaces up to homeomorphism. We will also explain why all three standard definitions of computable presentability for a compact Polish space—computably compact, computably metrized, computable topological—differ up to homeomorphism.

The study of computably compact spaces is very closely related to the investigation of effectively closed subsets of computably metrized Polish spaces, especially when the set happens to be computable closed. As we will see in Proposition 3.29, under some mild restrictions computable closed sets can be viewed as computably compact spaces, and vice versa by $(vi)$ of the theorem below. We cite [Reference Iljazović and Kihara67] for an excellent recent survey. The cited survey, however, does not really have many proofs or proof sketches, so we felt that including proofs should be a good idea; this is done in Section 3.5, which includes the necessary facts that we will need in the present paper.

Another classical and closely related subject in computability theory is the area of $\Pi ^0_1$ classes. This area can be viewed as a special case of the theory of effectively closed sets but restricted to $2^{\omega }$ . Of course, more can be said about $2^{\omega }$ than about an arbitrary space. Unlike the theories of computably compact spaces and computable closed sets, there is no shortage of excellent surveys and papers about $\Pi ^0_1$ -classes (e.g., [Reference Cenzer29, Reference Cenzer and Remmel30, Reference Diamondstone, Dzhafarov and Soare34]), and the draft of a book “Effectively Closed Sets $\Pi ^0_1$ Classes” by Cenzer and Remmel that is available online (as of early 2022). Thus, we will not include many proofs, we just state a few results in Section 2.6 that we will need, and will give references.

These three topics—computably compact spaces, computable closed sets, and $\Pi ^0_1$ -classes—are closely related, and no firm line can be drawn between them.

Before we proceed, we should admit that giving a complete and comprehensive survey of the existing literature and results on the subject is not among the main goals of this article, but nonetheless we will provide many useful references. This is not a survey paper in the usual sense, it is mainly a technical semi-survey paper with many new results, and it should be treated as such. We also chose to spread further discussion and references to the literature throughout the paper (where it is relevant) rather than to write a giant introduction.

1.5. The Main Theorem

The following theorem will be proven over the subsequent sections. The fundamentals of computable compactness theory will be developed simultaneously with the proof. We will discuss each clause of the theorem in detail shortly; for now we note that $\mathrm{(iii)},\mathrm{(iv)}$ , and $\mathrm{(viii)}$ are new.

Theorem 1.1. For a computably, completely metrized Polish space M, the following are equivalent:

  1. (i) Given n, we can effectively compute (the finite set of parameters describing) a finite $2^{-n}$ -cover $K_n$ of M by basic open balls.

  2. (ii) We can effectively enumerate all finite basic open covers (each given at once as a finite set of parameters) of the space.

  3. (iii) The same as $\mathrm{(i)}$ , but additionally in each finite cover n we can uniformly decide whether any finite collection of basic open balls in $ K_n$ intersect.

  4. (iv) In the notation of $\mathrm{(iii)}$ , we can additionally uniformly decide (non)emptiness of intersection for any finite collection of balls in $\bigcup _{n \in \omega } K_n$ , but balls may have merely computable radii (and, thus, are not necessarily basic).

  5. (v) There is a computable sequence of computable reals $(\epsilon _n)_{n \in \omega }$ ( $\epsilon _n \leq 2^{-n}$ ) so that, for every n, we can compute the maximal number of points in the space that are at least $\epsilon _n$ -far from each other.

  6. (vi) M is computably homeomorphic to a computable closed subset of the Hilbert cube.

  7. (vii) M is a computable surjective image of $2^{\omega }$ .

  8. (viii) The full continuous diagram of M is decidable.

As we will note later, it is easy to see that $\mathrm{(ii)}$ is also equivalent to the approach that is standard throughout reverse mathematics ([Reference Simpson135]): there exists an enumeration functional that, given a countable cover composed of basic open balls outputs (an index of) some finite subcover of the cover. This approach is perhaps the most familiar one to a working mathematician, while $\mathrm{(i)}$ is rather an effective analogy of total boundedness. Of course, a complete metric space is compact iff it is totally bounded, but this elementary fact is perhaps not quite as well-known as the standard definition of compactness. There are also other characterizations of computable compactness, e.g., for subsets of a fixed space in terms of Hausdorff distance. We will mention this characterisation later when we talk about computable closed sets and the Hilbert cube $\mathrm{(vi)}$ (see Fact 3.39). There are also other characterisations of computable compactness in special classes, e.g., in the class of profinite groups. We will discuss some such characterizations in due course.

In view of this theorem, we have the following definition, which is a characterization established in this paper:

Definition 1.2. A computable Polish space is called computably compact or effectively compact if it satisfies (the equivalent conditions in) Theorem 1.1.

The equivalence of $\mathrm{(i)}$ and $\mathrm{(ii)}$ is well-known, and usually one of the two is taken as the standard definition of a computably compact space. See Theorem 3.3.

It seems that $\mathrm{(iii)}$ or something similar might be also known, but perhaps in some other form (see, e.g., [Reference Hoyrup, Kihara and Selivanov62] for some related informal discussions). Also, Section 8.4 of [Reference Iljazović and Kihara67] contains a discussion of spiritually similar results. Perhaps, the most closely related material can be found in [Reference Pauly119]. However, we were unable to find any explicit proof of the equivalence of $\mathrm{(i)}$ and $\mathrm{(iii)}$ anywhere in the literature. For a proof, see Theorem 3.13.

As far as we know, $\mathrm{(iv)}$ is new. Characterization $\mathrm{(iv)}$ will be very useful in several applications greatly reducing the combinatorial complexity of proofs in many cases. It will be especially useful in computing cohomology groups of spaces, but some further (perhaps, less expected) applications will also be presented. This equivalence is stated and then proven in Theorem 3.16.

Iljazovič [Reference Iljazović65] was the first to discover the equivalence of the fifth formulation $\mathrm{(v)}$ with the standard definition; it has recently been re-discovered in [Reference Pauly, Seon and Ziegler120]. Its significance is the remarkable fact that computable compactness is an isometric invariant of the space. In other words, computable compactness is not a property of some specific nice presentation, but it is an intrinsic property that holds for all isometric presentations. The result will appear as Theorem 3.21.

The sixth version $\mathrm{(vi)}$ is well-known, but we are not sure who was the first to observe its equivalence to computable compactness. See Theorem 3.36 for a proof.

The seventh item $\mathrm{(vii)}$ is an effective version of the classical Hausdorff–Alexandroff theorem (see Theorem 3.40). The result is due to Brattka, de Brecht, and Pauly (see Proposition 4.1 of [Reference Brattka, de Brecht and Pauly20]). Also, working independently, Couch, Daniel, and McNicholl [Reference Couch, Daniel and McNicholl32] proved the result for the special case of closed subspaces of $\mathbb {R}^n$ . Around the same time, Day and Miller [Reference Day and Miller33] independently discovered another important special case of this result, specifically for probability spaces. Interestingly, in Remark 3.23 of his large unpublished survey “Algorithmic randomness, martingales and differentiability” Jason Rute refers to this property (being a computable image of $2^{\omega }$ ) as being a stronger version of computable compactness.Footnote 2 And indeed it may seem at first glance that it should be stronger than, e.g., $\mathrm{(i)}$ . We give two new and substantially different proofs of the result, one using $\mathrm{(iv)}$ discussed above, and the other one using $\Pi ^0_1$ classes and the Hilbert cube. Both proofs serve as a fine illustration of the techniques that we develop in the paper. The effective Hausdorff–Alexandroff theorem will be rather useful in several applications that will be discussed in due course.

Finally, the last item $\mathrm{(viii)}$ of the theorem is new; it is inspired by [Reference Ben Yaacov and Pedersen10, Definition 9.9] and the very recent paper [Reference Camrud, Goldbring and McNicholl25]. It says that any formula of continuous logic formed in the language of pure metric uniformly defines a computable function $M^n \rightarrow [0,1]$ , where n is the number of free parameters in the formula. This pleasant, unexpected, but quite elementary result will be stated formally in Theorem 3.7. Theorem 3.7 will be restricted to spaces of diameter $\leq 1$ , but as noted in the remarks preceding this theorem, it is just a mere notational convenience. The result perhaps confirms one’s suspicion that in the case of compact metric spaces, continuous logic is not particularly expressive.

1.6. Summary of applications

We now discuss several applications (of computable compactness) that can be found in Section 4. We are mainly focused on the applications that are either new, or give new proofs of known results. We also mention several applications that are very recent and are related to our research interests. We also pose several open questions.

Our list of applications is not even close to being exhaustive, but we will discuss the literature where more results of this sort can be found. Here is a summary:

  1. (1) In Section 4.1 the reader can find several useful standard results most of which are at least half-a-century old. They serve as a mere illustration of some of the basic techniques.

  2. (2) The next Section 4.2 contains an unpublished result of Nies and Melnikov that states that $\Pi _1^0$ classes can be used to represent isometric isomorphisms between effectively compact spaces. The result is not difficult, but its consequences are fairly powerful; in particular, combined with several standard results about $\Pi ^0_1$ -classes, this method gives elegant and much more “compact” proofs of some results from the literature.

  3. (3) Section 4.3 contains an application of computable compactness to constructing basic sequences in Banach spaces. The application is elementary but is neat. The subtlety is that, in classical Banach space theory, one routinely uses dual spaces and Hahn–Banach theorem to construct basic sequences (e.g., [Reference Carothers26]), but it is known that the Hahn–Banach theorem is not computable [Reference Brattka16, Reference Metakides, Nerode and Shore102]. Computable compactness gives a way to circumvent this obstacle. The result is very recent and can be found in Long’s M.Sc. thesis [Reference Long90].

  4. (4) The next Section 4.4 applies the techniques developed in Section 3 to Stone spaces; these results are very recent and can be found in [Reference Harrison-Trainor, Melnikov and Ng59, Reference Hoyrup, Kihara and Selivanov62]. For instance, we will see that a Stone space is computably compact iff it is computably metrizable iff the dual Boolean algebra is computably presentable. Among many applications, we will explain why the isomorphism problem for Stone spaces is $\Sigma ^1_1$ -complete. The result is “known” but it seems it has never been stated in the literature; we include it for future reference. We will also see that these techniques can be used to produce an example of a computable topological Polish space not homeomorphic to any computably metrized space.

  5. (5) In Section 4.5 we prove that a profinite group is recursively presented (in the sense of [Reference La Roche128, Reference Smith137]; to be defined) iff it is computably compact; this result is new.

  6. (6) Section 4.6 contains a new algorithm for computing Čech cohomology of a computably compact space. The algorithm is new, but the result itself is not new (though it is very recent [Reference Lupini, Melnikov and Nies91]). In the subsection we also discuss several applications of Čech cohomology in computable topology.

  7. (7) Section 4.7 applies computability of Čech cohomology established in the previous subsection to produce examples of computably metrized compact spaces that are not homeomorphic to any computably compact space. It is not hard to find a computably metrized space that is not isometrically isomorphic to any computably compact space (just take the interval $[0, \Omega ]$ , where $\Omega $ is Chaitin’s omegaFootnote 3 or some other left-c.e. real that codes $0'$ .) However, the situation becomes more complex if we view spaces up to homeomorphism. The result is not new but is very recent, and the proof that we give is a new combination of modern and classical techniques some of which we introduce in the preceding subsections. Our new proof is perhaps the simplest one known so far.

  8. (8) Section 4.8 contains a new proof of computable universality of $C[0,1]$ among computable Polish spaces up to (computable) isometry. The issue is that the standard proofs of universality of $C[0,1]$ rely on the Hahn–Banach theorem; as we have already mentioned above, it is not computable in general. Sierpinski [Reference Sierpiński134] suggested a more direct proof that he thought was “effective”; however, his proof gives a merely $0'$ -computable embedding. We use tools of computable compactness to produce a computable embedding of any computable Polish space to the standard presentation of $C[0,1]$ . The result is not new [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5], but the proof that we here give is new. Our new proof is much less combinatorially involved than the one in [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5]; the latter does not use computable compactness tools. (However, it is not necessarily clear that our proof holds primitively recursively, while the proof from [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5] gives a primitive recursive embedding.)

  9. (9) In Section 4.9 we prove that every computably compact space of finite covering dimension can be computably embedded into a finitely dimensional Euclidean space. This is an improved version of a very recent result of Harrison-Trainor and Melnikov [Reference Harrison-Trainor and Melnikov58] that establishes that there is an arithmetical embedding. Our result is stronger and the technique that we use is different from what has been used in [Reference Harrison-Trainor and Melnikov58]. The new version heavily relies on one of the new characterizations of computable compactness that we prove in the paper. It will allow us to effectivize one of the standard proofs from the classical literature with only minor modifications.

  10. (10) Section 4.10 contains the proof of the fact that, for a computably compact X, the space of probability measures $\mathcal {P}(X)$ on X is a computable homeomorphic image of $2^\omega $ . This is known, even though the standard reference [Reference Day and Miller33] does it only for the special case of $X = 2^{\omega }$ and via an explicit construction of a computable map from $2^{\omega }$ onto $\mathcal {P}(X)$ . But it is actually easier to establish computable compactness of $\mathcal {P}(X)$ directly (using covers), and then apply (vii) of Theorem 1.1. The result is very recent and is due to Marcone and Valenti [Reference Marcone and Valenti92]. Computable compactness of $\mathcal {P}(X)$ can be used to show that a compact computable group is computably compact iff it admits a computable Haar probability measure. This is a known result and we will discuss it more fully in Section 4.10.

  11. (11) The final Section 4.11 contains several open questions that are related to the material contained in the previous subsections. Most of these questions are directly or indirectly related to compactness.

To make our exposition smoother, we shall often define notions when we need them. The most commonly known basic notions of computable metric space theory can be found in the preliminaries.

2. Preliminaries

All of our spaces are Polish (separable and completely metrizable) spaces. Such spaces are also sometimes called Polishable. All spaces are also compact, unless stated otherwise. There will be only very few exceptions towards the end of the paper where the spaces considered will not be compact, namely the Urysohn space and the space of continuous functions on the unit interval $C[0,1]$ .

We will almost never consider the empty space, even though it is actually possible to include this rudimental case into our framework. However, many proofs become more uniform and definitions more convenient if we exclude this case.

We remind the reader that a real $\alpha $ is computable if there exists a computable sequence $(q_{f(i)}\mid i\in {\mathbb N})$ of rational numbers such that $|\alpha -q_{f(i)}|<2^{-i}.$ If we have a computable sequences of rationals but only know that $q_{f(i)}\to \alpha $ , but not a computable modulus of convergence, then we would say that $\alpha $ is a $\Delta _2^0$ -real; and if the sequence $q_{f(i)}$ is monotonically increasing (resp. decreasing), then $\alpha $ is said to be left-c.e. or lower semi-computable (resp. right c.e. or upper semi-computable).

Much work in computable analysis from recent years has been concerned with the theory of representations [Reference Weihrauch146]. In the type 1, countable case, when we talk about functions acting on, for example, polynomials, we really mean functions acting on numbers or strings “representing” the objects. In the type 2 case, a representation is a way of assigning an infinite string $\alpha $ in Baire space $\omega ^{\omega }$ with the object we wish to run algorithms upon; and to do so in a computationally meaningful way. However, in the case of Polish spaces, Cauchy sequences provide a natural and effective way to represent elements. Thus, we stick throughout with the notation as presented in the subsections below.

2.1. Effective metrizations of Polish spaces

A Polish space $(M,d)$ is right-c.e. presented or admits a right-c.e. metric if there exists a sequence $(\alpha _i)_{i\in \omega }$ of M-points which is dense in M and such that for every $i,j\in \omega $ , the distance $d(\alpha _i, \alpha _j)$ is a right-c.e. real, uniformly in i and j. (In particular, we always assume that the metric is complete.) More formally, there is a c.e. set $W \subseteq \omega ^{2}\times \mathbb {Q}$ such that for any i and j,

$$\begin{align*}\{ q\in \mathbb{Q}\,\colon d(\alpha_i, \alpha_j) < q\} = \{ q\,\colon (i,j,q)\in W\}. \end{align*}$$

Note that the sequence $(\alpha _i)_{i \in \omega }$ may contain repetitions; equivalently, it is possible that $d(\alpha _i, \alpha _j) = 0$ for some $i,j$ . We call points $\alpha _i$ from the sequence special or ideal. For instance, an undirected (simple) graph with the shortest path metric is a right-c.e. metrized space. We will see that $\Pi ^0_1$ classes can also be viewed as right-c.e. metrized spaces.

The definition of a left-c.e. Polish space is obtained from the notion of a right-c.e. Polish space using the notion of a left-c.e. real, mutatis mutandis.

Definition 2.1. A Polish space is computably presented or, perhaps more descriptively, computably metrizable if there is a (complete) metric on the space which is both right-c.e. and left-c.e.

Strictly speaking, a computable or a right-c.e. metrization of a space is a countable object $(\alpha _i)_{i\in \omega }$ , but we will usually identify a computable metrization $(\alpha _i)_{i\in \omega }$ of space M with its completion $\overline {(\alpha _i)_{i\in \omega }}$ .

Remark 2.2. Note that we intentionally did not emphasise whether we consider Polish spaces up to isometric isomorphism or under some other notion of similarity, such as, e.g., quasi-isometry or homeomorphism. Indeed, these will lead to non-equivalent notions. For example, for a real $\xi $ , the space $[0, \xi ]$ is isometrically isomorphic to a computably metrized space if, and only if, $\xi $ is left-c.e. However, for any real $\xi $ this space is homeomorphic to the unit interval $[0,1]$ which is of course computably metrizable. In this paper we usually consider Polish spaces under homeomorphism, that is, a Polish space has a right-c.e. presentation if it is homeomorphic to the completion of a right-c.e. metrized space. Nonetheless, we will emphasise this in most of the theorems and lemmas that we prove to make sure that there is no conflict of terminology.

2.2. Computable topological spaces

There are several definitions of a computable topological space that can be found in [Reference Kalantari and Weitkamp73, Reference Korovina and Kudinov83, Reference Spreen139]. We will use the following.

Definition 2.3 (see, e.g., Definition 3.1 of [Reference Korovina and Kudinov84] or Definition 4 of [Reference Weihrauch and Grubba148]).

A computable topological space is given by a computable, countable basis of its topology for which the intersection of any two basic open sets (“basic balls”) can be uniformly computably listed. More formally, it is a tuple $(X,\tau ,\beta ,\nu )$ such that:

  • $(X,\tau )$ is a topological $T_0$ -space,

  • $\beta $ is a base of $\tau $ ,

  • $\nu \colon \omega \to \beta $ is a computable surjective map (i is called an index of $\nu (i)$ ), and

  • there exists a c.e. set W such that for any $i,j\in \omega $ ,

    $$\begin{align*}\nu(i) \cap \nu(j) = \bigcup \{ \nu(k)\,\colon (i,j,k) \in W\}. \end{align*}$$

Let $(X,\tau ,\beta ,\nu )$ be a computable topological space. For $i\in \omega $ , by $B_i$ we denote the open set $\nu (i)$ . As usual, we identify basic open sets $B_i$ and their $\nu $ -indices. There are many versions of this notion above in the literature (see, e.g., [Reference Spreen139]). All of these notions are essentially Definition 2.3 with some extra assumption. For example, one can also additionally require that there is a computable dense sequence $(x_i)_{i \in \omega }$ such that $\{\langle i, j \rangle : x_i \in B_j \}$ is computably enumerable. See [Reference Nogina115, Reference Spreen139] for many other extra assumptions, some of which definitely seem ad hoc. We thus stick with the basic Definition 2.3. Perhaps, the most natural example of a computable topological Polish space is given by the proposition below.

Proposition 2.4 (cf. Theorem 2.3 of [Reference Korovina and Kudinov84]).

Every right-c.e. Polish space is a computable topological space.

Proof Let $(M,d)$ be a right-c.e. Polish space, and let $(\alpha _i)_{i\in \omega }$ be its sequence of special points. By $\tau $ we denote the metric topology of $(M,d)$ . As usual, the base $\beta $ of $\tau $ contains basic open balls

$$\begin{align*}B(\alpha_i,q) = \{ x\in M\,\colon d(\alpha_i,x) < q\},\ \ \ i\in\omega,\ q\in\mathbb{Q}^{+}. \end{align*}$$

For $i\in \omega $ and $q\in \mathbb {Q}^{+}$ , we put $\nu (i,q) = B(\alpha _i,q)$ .

We prove that the tuple $(M,\tau ,\beta ,\nu )$ is a computable topological space. It is sufficient to establish the following: for any $i,j\in \omega $ and $q,r\in \mathbb {Q}^{+}$ , we can (uniformly) effectively enumerate a set $X \subseteq \omega \times \mathbb {Q}^{+}$ such that

(1) $$ \begin{align} B(\alpha_i,q) \cap B(\alpha_j, r) = \bigcup \{B(\alpha_k, t) \,\colon (k,t) \in X \}. \end{align} $$

Our set X is defined as follows: X contains all pairs $(k,t)$ such that

$$\begin{align*}d(\alpha_i,\alpha_k) < q - t \text{ and } d(\alpha_j,\alpha_k) < r-t. \end{align*}$$

Since the space $(M,d)$ is right-c.e., it is not hard to see that the set X is c.e., uniformly in $i,j,q,r$ . If $(k,t)\in X$ , then by using the triangle inequality, we can easily show that $B(\alpha _k,t)$ is a subset of $B(\alpha _i,q) \cap B(\alpha _j,r)$ .

Let x be an arbitrary point from $U = B(\alpha _i,q) \cap B(\alpha _j, r)$ . Choose positive rationals $\epsilon $ and $\delta $ such that $\epsilon < q - d(\alpha _i, x)$ and $\delta < r - d(\alpha _j, x)$ . Since U is open, we can find $k\in \omega $ and $t \in \mathbb {Q}^+$ such that $x\in B(\alpha _k, t) \subseteq U$ and $t < \min (\epsilon /2, \delta /2)$ . Then we have

$$\begin{align*}d(\alpha_i,\alpha_k) \leq d(\alpha_i,x) + d(\alpha_k,x) < (q - \epsilon) + t < q - \epsilon/2 < q - t. \end{align*}$$

Therefore, $(k,t)$ belongs to X, and the set X satisfies (1). Hence, $(M,\tau ,\beta ,\nu )$ is a computable topological space.

For instance, every computably metrized Polish space is a computable topological space. We shall return to computable topological and right-c.e. spaces later, when we talk about Stone duality. Effective compactness can also be defined for computable topological and right-c.e. spaces, but we will not need this degree of generality until Section 4.4. (This will be clarified in the remarks before Theorem 4.28.) Until Section 4.4 we restrict ourselves to computable, completely metrized spaces.

2.3. The definition of computable compactness

We have already explained what it means for a Polish space to be computably metrized. We usually assume that all our spaces are Polish metric and non-empty. Recall that a complete metric space M is compact iff for every $\varepsilon>0$ , there exists a finite set F of points such that every point has distance less than $\varepsilon $ to F. For now, we say that a space is computably compact if it satisfies $\mathrm{(i)}$ of Theorem 1.1:

Definition 2.5. A computably metrized space is called computably compact if there exists a computable function that, given n, outputs the index of a finite tuple of basic open balls of radii ${<}2^{-n}$ that cover M.

We should explain a bit more carefully all the terms that we use in the definition above. A ball centred in a special point is basic if its radius is a rational number. When we consider finite covers, we usually say that we can compute a finite cover by basic open balls if we can compute the index of a finite set that codes the indices of the finitely many centres and the rational radii of basic open balls in the cover. This should not be confused with enumerating a finite cover, i.e., listing one ball after another in a c.e. fashion.

Remark 2.6. Most proofs in this article do not actually need the radii to be rational numbers, but would work with balls of radius a computable real. However, we cannot list computable reals effectively. Therefore, we cannot hope to have an effective base of topology consisting of all basic balls with computable radii and computable points.

Suppose a compact space is computably metrized. How much computational power do we need to make it computably compact?

Definition 2.7. Let $ M = (M, d, (p_i)_{i \in {\mathbb {N}}})$ be a compact computable metric space. A compactness modulus of $ M$ is any function that bounds

$$\begin{align*}h(n) = \min \{j \colon \, \forall i \exists k< j \, d(p_i, p_k) \leq 2^{-n}\} \end{align*}$$

from above. We call h the least modulus of compactness.

Note that if $h(n)= j$ , then the $2^{-n+1}$ -basic open balls centred in $p_0, \ldots , p_j$ cover the space. Since $d(p_i, p_k) \leq 2^{-n}$ is a $\Pi ^0_1$ condition and the quantifier $\exists k< j$ is bounded, and the space is compact, h is computable relative to $0'$ . It is not difficult to show that there exists a computably metrized compact space in which the least modulus of compactness computes $0'$ , and indeed, any modulus of compactness as well. As we mentioned in the introduction, the interval $[0,\Omega ]$ defines a computably metrized space that is not isometrically isomorphic to any computably compact space (by Theorem 3.21), and its modulus of compactness (for any computable presentation) computes $0'$ .

In what will follow, we will not necessarily need the (least) modulus of compactness. Indeed, it is sufficient to calculate some (and not necessarily the least) j such that $\forall i \exists k< j \, d(p_i, p_k) \leq 2^{-n}$ . One way to state this would be to require j to be “the first found” (in some $\Delta ^0_2$ approximation sense) that works. A space is computably compact if for every n we can compute some j that works. It is not difficult to manufacture a pathological example of a space where some j can be computably found for a given n, but one cannot compute the least such j. (See the next subsection for a similar counterexample.)

2.4. More about basic open balls

Notation 2.8. For a basic open B, write $B^c$ for the basic closed ball with the same centre and radius as B.

The reader should keep in mind that the space can be very strange, quite unlike ${\mathbb R}^n$ . For instance, the closure $\overline {B}$ of B does not have to be equal to $B^c$ in general (think of an isolated point in $B^c\setminus B$ ). Also, in general we cannot decide whether two basic open or closed balls intersect or not, as is illustrated by the example below.

Example 2.9. There exists a computably compact subspace of the unit square such that there is no uniformly computable procedure deciding whether two given basic open or basic closed $2^{-n}$ -balls intersect.

To make sure that the non-emptiness of intersection of open balls is undecidable, for every n create a gadget consisting of two points $x_n$ and $y_n$ at distance $2^{-n} -2^{-n-2}$ from each other, and also put a third point $z_n$ at distance exactly $2^{-n}$ from each of $x_n$ and $y_n$ . The point is at the intersection of the $2^{-n}$ -circles centred at $x_n$ and $y_n$ .

  • Wait for the nth potential procedure to declare that $B(x_n, 2^{-n}) \cap B(y_n, 2^{-n}) =\emptyset $ .

  • If this ever happens at some stage s, take $m = s+n+1$ and put a new point $w_n$ at distance exactly $2^{-m}$ from $z_n$ so that $w_n \in B(x_n, 2^{-n}) \cap B(y_n, 2^{-n})$ .

To make sure that the non-emptiness of intersection of basic closed balls is undecidable, for every n create a similar gadget, but this time keep $z_n$ out of the space at every finite stage. Instead, initiate the enumeration of a sequence $(\xi _{i,n})$ of points in the complement of $B^c(x_n, 2^{-n}) \cup B^c(y_n, 2^{-n})$ rapidly converging to $z_n$ , i.e., $d(z_n, \xi _{i, n}) = 2^{-n-i}$ . At stage s, put $\xi _{s, n}$ into the space.

  • Wait for the nth potential procedure to declare that $B^c(x_n, 2^{-n}) \cap B^c(y_n, 2^{-n}) \neq \emptyset $ .

  • If this ever happens at some stage s, stop putting points $\xi _{s,n}, \xi _{s+1,n} \ldots $ into the space.

It should be clear that, for each gadget, the diagonalization works. We also note that the gadgets are uniformly computably compact. We can fit all these gadgets into the unit square and get a computably compact metric space (of Cantor–Bendixson rank 2) with the desired property.

Thus, we see that the non-emptiness of set-theoretic intersection of basic open balls in not c.e. in general. We will return to this issue in Section 3.3 where we will see that there are enough balls for which this property actually is decidable; hence, we can get a characterization of computable compactness where the basic balls used in covers have decidable intersections.

A similar example can be produced to show that inclusion is also not c.e. in general. The following stronger notion is c.e.; it will be very useful throughout the paper. We write $r(B)$ for the radius of a basic ball B and we use $cntr(B)$ to denote its (distinguished) center.

Definition 2.10. A basic open ball U is said to be formally included into a basic open W, written $U \subseteq _{form} W$ , if

$$ \begin{align*}r(U) + d(cntr(U), cntr(W)) < r(W). \end{align*} $$

This notion has been around for many decades (see, e.g., [Reference Spreen139] where it is called strong inclusion). If the centres and the radii are computable (not necessarily special and rational, respectively), formal inclusion remains c.e. The same can be said about formal s-disjointness defined as follows.

Definition 2.11. Two basic open balls U and W are formally s-disjoint if $r(U) + r(W) < d(cntr(U), cntr(W))$ and this can be seen after calculating the radii and the distance with precision $2^{-s}$ . We say that U and W are formally disjoint if they are formally s-disjoint for some s.

We note that formal inclusion remains c.e. in the context of right-c.e. metric spaces, while formal disjointedness remains c.e. in left-c.e. metric spaces.

2.5. Effectively continuous maps

Let X be a computable topological space. For a point $x\in X$ , its name is the set

$$\begin{align*}N^x = \{ i\in\omega\,\colon x\in B_i\}. \end{align*}$$

We say that a map $f:X \rightarrow Y$ between computable topological spaces X and Y is computable if there exists an enumeration operator that, given the name of $x \in X$ , outputs the name of $f(x) \in Y$ .

An open name of an open set $U \subseteq X$ is a set $W\subseteq \omega $ such that

$$\begin{align*}U = \bigcup_{i\in W} B_i. \end{align*}$$

Definition 2.12. Let X and Y be computable topological spaces. A function $f\colon X \to Y$ is effectively continuous if there is a c.e. family $F\subseteq \mathcal {P}(X) \times \mathcal {P}(Y)$ of pairs of (indices of) basic open sets such that:

  1. (C1) For every $(U,V) \in F$ , we have $f(U) \subseteq V$ .

  2. (C2) For every point $x \in X$ and every basic open E in Y such that $f(x)\in E$ , there exists a basic open D in X with $(D,E) \in F$ and $x\in D$ .

The elementary fact below is well-known and can be traced back to, e.g., [Reference Ceitin27]. In this specific form it can be found in [Reference Melnikov and Montalbán97]. The lemma essentially says that a map is computable if, and only if, it is effectively continuous.

Lemma 2.13. Let $f\colon X\to Y$ be a function between computable Polish spaces. Then the following conditions are equivalent:

  1. (1) f is effectively continuous.

  2. (2) There is an enumeration operator $\Phi $ that on input an open name of an open set V in Y lists an open name of the set $f^{-1}(V)$ in X.

  3. (3) There is an enumeration operator $\Psi $ that given the name of a point $x\in X$ , enumerates the name of $f(x) \in Y$ .

(We remark that the proof below works for right-c.e. spaces. It also works for computable topological spaces with c.e. formal (strong) inclusion that can be defined abstractly without any reference to a metric; see, e.g., [Reference Melnikov and Montalbán97, Reference Spreen139].)

Proof $(1) \Rightarrow (2).$ Suppose $V = \bigcup _{i \in W} B_i$ . Note that (C2) implies that

$$ \begin{align*}f^{-1}(V) = \bigcup \{D \in X: (D, E) \in F \, \& \, \exists i \in W \, E \subseteq_{form} B_i\},\end{align*} $$

and thus the name of $f^{-1}(B_i)$ can be listed using only positive information about $W,$ with all possible uniformity.

$(2) \Rightarrow (3).$ Note that $B \in N^{f(x)}$ if and only if $f^{-1}(B)$ contains a basic open set in $N^x$ .

$(3) \Rightarrow (1).$ Define a collection F of pairs $(D,E)$ of (indices of) basic open sets in $X \times Y$ as follows. Fix a basic open E in Y. Enumerate all basic open D in X, and for each such D, enumerate all finite collections $D, A_1,\ldots , A_k$ of basic open sets (in X) such that $D \subseteq _{form} \cap _{i \leq k} A_i$ (meaning that D is formally contained in each $A_i$ ). Feed these finite collections to $\Phi $ and wait for some E to be enumerated in the output. When E is enumerated (if ever), put $(D,E)$ into F.

We claim that F defined above satisfies (C1) and (C2). We check (C1). If $(D,E) \in F$ then $f(D) \subseteq E$ . Indeed, suppose $d \in D$ . There exists a sequence $D, A_1, \ldots , A_k$ such that $\Phi ^{\{D, A_1,\ldots , A_k\}}$ enumerates E. Recall $D \subseteq _{form} \cap _i A_i$ implies $D \subseteq \cap _i A_i$ , thus for any $d \in D$ the sequence listed by $\Phi ^{N^d}$ will contain E, and therefore $f(D) \subseteq E$ . We now check (C2). Fix $x \in X$ and a basic open $E \ni f(x)$ . We must show that for some basic open $D \ni x$ , $(D, E) \in F$ . By assumption, $\Phi ^{N^x}$ enumerates $N^{f(x)}$ that contains E. Suppose E is listed with use $A_1, \ldots , A_k$ . Since the $A_i$ all contain x, there exists a basic open $D \ni x$ that is formally included into their intersection. Since the operator uses only positive information about its oracle, it will list E on input $\{D, A_1, \ldots , A_k\}$ as well, and thus $(D,E)$ will be enumerated into F.

2.6. $\Pi ^0_1$ -classes

$\Pi _1^0$ classes will be important for some of the work to follow. Thus we give a brief reminder of the basic definitions and results.

We fix the standard computable presentation of $2^{\omega }$ under the usual shortest common initial segment ultra-metric. The space $2^{\omega }$ can be viewed as $[2^{<\omega }]$ the set of infinite paths through the complete binary tree, so points are paths. A closed subset C of $2^{\omega }$ is called an a $\Pi ^0_1$ class if we can computably enumerate the basic clopen sets whose union make up the complement of C in $2^{\omega }$ . That is, C is the set of paths $[T]$ through a computable subtree T of $2^{<\omega }$ .

A moment’s thought reveals that in computable mathematics $\Pi _1^0$ classes occur everywhere. One of the fundamental correspondences is $\Pi _1^0$ classes and degrees of theories, pioneered by Jockusch and Soare in the early 1970s [Reference Jockusch and Soare70Reference Jockusch and Soare72], and even earlier by Kreisel [Reference Kreisel86] and Shoenfield [Reference Shoenfield133]. That is, $\Pi _1^0$ classes effectively correspond to (completions of) axiomatizable theories under Stone duality.

We shall need the following elementary fact:

Fact 2.14. An isolated point in a $\Pi ^0_1$ -class is computable.

Thus, for instance, if a $\Pi _1^0$ class is countable, it must have a computable point. Another well-known but less elementary fact that we will refer to is the following result.

Theorem 2.15 (The Low Basis Theorem [Reference Jockusch and Soare72]).

A non-empty $\Pi ^0_1$ class contains a member P of low Turing degree, that is, $P'\equiv _T \emptyset '$ .

Since we are concerned with computable compactness, it seems reasonable to see what computable compactness means in this context.

Example 2.16. Let $C=[T] \subseteq 2^{\omega }$ be a $\Pi _1^0$ class such that Ext $(T)=\{\sigma \in T\mid \exists \alpha \in 2^{\omega }(\sigma \alpha \in [T])\}$ is computable.Footnote 4 Then $C= [T]$ can be viewed as a computably compact space. To see why, first use computability of Ext $(T)$ to define a computable sequence of (uniformly computable) strings $D=\{\alpha _i\mid i\in \omega \} \subseteq 2^{\omega }$ so that D is dense in C; we omit the details. (The example will be generalised in Section 3.5 where we will give a complete proof of a more general result.) Clearly, being the completion of D, C forms a computably metrized space under the ultra-metric inherited from $2^{\omega }$ . Given n, we compute a $2^{-n}$ cover. Compute $E_n=\{\sigma \mid \sigma \in $ Ext $(T)\land |\sigma |=n+1\}$ . Let $E_n=\{\tau _1,\dots , \tau _k\}$ . For each i we can use the fact that Ext $(T)$ is computable to calculate the leftmost extension $\alpha _i$ of $\tau _i$ in C, and then the balls of radius $2^{-n}$ around the $\alpha _i\cap C$ cover C.

Many other facts about $\Pi _1^0$ classes can be found in [Reference Cenzer29, Reference Cenzer and Remmel30] and Chapter 2 of [Reference Downey and Hirschfeldt36].

3. The definition of computable compactness is robust

3.1. The other two standard definitions of computable compactness

Our convention is that all of our spaces are nonempty Polish spaces. Definition of computable compactness says that for every n we can compute a cover of the space by basic $2^{-n}$ -balls. This definition seems a weak form of compactness, as it seems that having a fixed cover for each $2^{-n}$ does not seem quite as good as having access to all finite covers. The following definition would seem to give a stronger notion of computable compactness.

Definition 3.1. We define computably metrized space to be $*$ -computably compact if the collection of all finite covers of M by basic open balls can be given as a c.e. collection of explicit finite sets.

We also note that Definition 3.1 is equivalent to:

Definition 3.2. We say that a computably metrized space is computably countably compact if there is a partial computable operator that, on input any potential c.e. open basic cover, halts if it is a cover and outputs some finite sub-cover.

It is easy to see that a space is effectively $*$ -compact iff it is computably countably compact. To see why computable countable compactness implies $*$ -computable compactness, we can enumerate all finite collections of basic open balls and apply the algorithm: if the procedure halts output its subcover. This enumerates a collection of finite covers, and to enumerate them all, we consider the union of this collection with the collection of all finite sets of balls. The other direction is also straightforward: if the space is $*$ -computably compact, given a c.e. cover wait till we enumerate a finite subcover. These versions of countable compactness is essentially the approach used in reverse mathematics (e.g., [Reference Simpson135]).

Interestingly, the two potential definitions suggested above (and a few more) turn out to be equivalent.

Theorem 3.3 (Folklore).

For a computably metrized (compact) Polish space M, TFAE:

  1. (1) M is computably compact.

  2. (2) M is $*$ -computably compact.

Proof The implication $(2)\rightarrow (1)$ is obvious.

Assume $(1)$ . We prove $(2)$ . Take a finite collection $(B_i)$ of basic open sets and assume it is a cover. We must argue that eventually we will be able to effectively recognise that it is indeed a cover. The idea is that there exists an $\epsilon = 2^{-n}$ so small that every $\epsilon $ -cover of M is formally contained in this given cover. (This will be the Lebesgue number of the cover, in particular.) This will also be true for the $\epsilon $ -cover that will be given to us according to the definition of computable compactness. Since formal inclusion is c.e., we will be able to recognise that this formal inclusion has occurred. Noting that formal inclusion does imply set-theoretic inclusion, so if some $\epsilon $ cover is formally included in some other finite collection of basic open balls, then this other collection must also be a cover. Thus, if we succeed, it will show that $(B_i)$ is equivalent to saying that, for some n, every ball in the $2^{-n}$ -cover given to us by the definition of computable compactness (and indeed, any other $2^{-n}$ -cover) is formally included in one of the $B_i$ . This is, of course, a $\Sigma ^0_1$ -property.

It remains to prove that such an $\epsilon $ exists. We argue non-computably. Let $c_i$ be the center of $B_i$ , and $r_i$ be its the radius. Define for every i, a function $f_i (x) = r_i - d(x,c_i)$ if x is in the ball $B_i$ , and $0$ otherwise. This function is continuous. Now take the supremum of the finite family $(f_i)$ to define a new continuous g; $g(x)=\sup _i f_i(x)$ . If $(B_i)$ indeed was a cover, then the function g would be strictly positive, because each x is inside one of the $B_i$ .

Let v be its infimum that is achieved somewhere, by compactness. Take a rational $\epsilon =2^{-m}$ less than $v/2$ . Then for every point y, we have $ \epsilon < r_i - d(y, c_i)$ ; that is

$$ \begin{align*}d(y, c_i)+ \epsilon< r_i,\end{align*} $$

equivalently, $B(y, \epsilon ) \subset _{form} B_i$ . This inclusion will still hold if we replace $\epsilon $ with an even smaller $\epsilon '$ . Thus, in particular, every basic open $\epsilon '$ -ball is formally included in one of the $B_i$ . Consequently, $(1)$ implies $(2)$ .

Remark 3.4. The proof of $(1) \rightarrow (2)$ above additionally tells us that, for any given finite basic cover there is an $\epsilon $ small enough so that any $\epsilon $ -cover formally refines the given cover. Also note that to recognize formal inclusion in a c.e. way, we do not need the radii $r_i$ to be rational numbers; (uniformly) computable $r_i$ will suffice.

In view of Theorem 3.3, henceforth we use computably compactness and $*$ -computably compactness interchangeably, and without further comment.

3.1.1. Elementary properties of computably compact spaces

Examples of computably compact spaces are the unit interval $[0,1]$ , the unit circle that can be viewed as the set of complex numbers having norm one: $\{\xi \in \mathbb {C}: || \xi || =1\}$ , the Hilbert cube, cantor space $2^\omega $ , and also “natural” (rational) geometric realisations of finite simplicial complexes that are central to algebraic topology. Simplicial complexes will be used as a tool later in the paper, and indeed will be discussed in the next subsection. We shall give much more intricate examples of computably compact spaces in due course.

There are several properties of computably compact spaces that are immediate from the definitions. These, for instance, include those summarised in the following:

Proposition 3.5 (Folkore).

  1. (1) Let $f:M \rightarrow \mathbb {R}$ be computable and let M be computably compact. Then $\sup _{x \in M} f(x)$ and $\inf _{x \in M} f(x)$ are computable real numbers. Furthermore, this is uniform.

  2. (2) The class of (non-empty) computably compact spaces is closed under taking (finite or computably infinite) direct products. More specifically, if $(M_i)_{i \in I}$ is a uniformly computable sequence of spaces, where $I \in \omega \cup \{\omega \}$ , then the direct product

    $$ \begin{align*}\prod_{i \in I} M_i\end{align*} $$
    under (say) the metric
    $$ \begin{align*}\sum_{i \in I} 2^{-i} \dfrac{d(x_i, y_i)}{1+d(x_i, y_i)},\end{align*} $$
    where $x_i$ denotes the ith projection of $x \in \prod _{i \in I} M_i$ , is a computably compact metric spaceFootnote 5 . (See, e.g., Lemma 3 of [Reference Rettinger126].)
  3. (3) If $f, g :M^n \rightarrow \mathbb {R}$ are computable and M is computably compact, then the following functions are also computable:

    • $\sup _{x \in M} f(x, x_2, \ldots , x_n)$ and $\inf _{x \in M} f(x, x_2, \ldots , x_n)$ ;

    • $\max \{f, g \}$ and $\min \{f, g\}$ ;

    • $f-g, f+g, \alpha g$ for any computable real $\alpha $ .

    This is also uniform in the strongest sense possible.

We omit the elementary proof. We remark that in (2), the choice of a dense computable sequence is not canonical. One way of choosing a dense computable sequence is to fix some (e.g., the first found) sequence of special points $\alpha $ in the product, and then using elements that are “eventually $\alpha $ .” That is the dense subset will be given by the collection of sequences of special points that are equal to $\alpha $ for cofinitely many coordinates (projections). There are other potential metrics that we can use instead of the one suggested above, but the natural choices will be effectively equivalent (meaning that the identity map will be computable with respect to one and the other metric under consideration).

3.2. Continuous logic and decidability

In this subsection we discuss continuous model theory and continuous logic. For a smooth introduction to this subject, we cite [Reference Ben Yaacov, Berenstein, Henson and Usvyatsov9]. We will not need the definitions of continuous model theory in their full generality. Our structures are compact metric spaces of diameter at most $1$ . The restriction on the diameter can be removed using linear scaling of the metric. We view such spaces as structures in the signature $\{d\}$ , where $d:M^2 \rightarrow [0,1]$ .

The idea is that every formula $\phi $ of continuous logic is (associated with) a uniformly continuous function, and $[\phi ]: M^n \rightarrow [0,1]$ . In classical logic the truth values $\{T,F\}$ are built into the language, and continuous logic has $[0,1]$ similarly built into the signature. We therefore fix the standard computably compact copy of $[0,1]$ given by $\mathbb {Q} \cap [0,1]$ and view it as a part of the language, not a part of our structure. Traditionally, $\phi (\bar {x})$ is interpreted as “true” if $[\phi (\bar {x})] = 0$ , and false if $ [\phi (\bar {x})] = 1$ . But of course, there are continuum many possibilities in-between. Having in mind this intended interpretation of formulae, we write $f, g,h \ldots $ to denote our continuous formulae. Because of the aforementioned somewhat unusual interpretation of the truth values, it makes sense to define the analog

of implication as follows:

In particular, $1$ (which is the “ultimate false”) implies any g. Also, we interpret the disjunction as the minimum:

$$ \begin{align*}[f \vee g] = \min \{[f], [g] \},\end{align*} $$

and we interpret the conjunction as the maximum of the two functions. The analog of the negation of f is

. Also, we include $\dfrac {1}{2} f$ to mean $\dfrac {1}{2}[f]$ . Finally, instead of quantifiers we use $\sup $ and $\inf $ . For example, if $f(x,y)$ has already been defined, we can define $g(x)$ to be

$$ \begin{align*}\sup_{y} f(x,y),\end{align*} $$

and in this case clearly

$$ \begin{align*}[g]= [\sup_y f(x,y)] = \sup_{y \in M} [f(x,y)],\end{align*} $$

which is (uniformly) continuous if f was.Footnote 6

Since our language is merely $\{d\}$ , the atomic formulae are just $d(x,y)$ and the constant functions $0$ and $1$ . We close these formulae under finite iterations of $\sup , \inf , \wedge , \vee , \dfrac {1}{2} \cdot ,$ and to define the (full) continuous diagram of $(M, d)$ . The definition below is inspired by [Reference Ben Yaacov and Pedersen10, Definition 9.9] and [Reference Camrud, Goldbring and McNicholl25, Definition 3.2]. Recall that we fixed the usual computable presentation on the unit interval.

Definition 3.6. We say that a Polish space of diameter ${\leq}1$ is continuously decidable if its continuous diagram is uniformly computable. That is, given (the Gödel number of) a continuous formula $\phi (\bar {x})$ (from the full continuous diagram of M) we can uniformly produce an index for a Turing operator that computes the function

$$ \begin{align*}[\phi (\bar{x})]: M^n \rightarrow [0,1],\end{align*} $$

where $\bar {x} = x_1, \ldots , x_n$ .

In the definition above, we could allow M to have an arbitrary diameter $1 \leq \delta \leq m \in \mathbb {N}$ and use $m^{-1} [\phi (\bar {x})]$ as an interpretation of our formulae. Alternatively, we could scale the metric and use $d'(x,y) = m^{-1} d(x,y)$ . Thus, the theorem below is not really restricted to spaces of diameter $\leq 1$ ; it is a mere notational convenience.

Theorem 3.7. Suppose X is a computable Polish space that is compact and has diameter $\leq 1$ . Then the following are equivalent:

  1. (1) X is continuously decidable.

  2. (2) X is computably compact.

Proof $(2) \rightarrow (1)$ . The supremums and infimums of computable functions are uniformly computable (see Proposition 3.5(1)), and so is for every computable f and g. The proof then proceeds by induction on the complexity of continuous formulae (with parameters).

  1. (1) The distance function is computable by our assumption, and so are the constant functions $1$ and $0$ .

  2. (2) If $f(x, \bar {y}), g(x, \bar {y})$ are computable, then so are , and $\dfrac {1}{2} f(x, \bar {y})$ (see Proposition 3.5(3)).

The latter also includes the case when there are no parameters, which means that the function is just the constant function (a computable real).

$(1) \rightarrow (2)$ . Let $(x_i)$ be the computable dense sequence. There is a formula of continuous logic saying that

which we can computably evaluate with precision $2^{-n}$ . If we discover that

$$ \begin{align*}U_n(x_0, ..., x_m) < 2^{-n},\end{align*} $$

then every point is at distance at most $2^{-n+1}$ from one of the $x_i$ , by the triangle inequality. Since we can effectively list such formulae, and for every n there exists an m for which the formula holds up to $2^{-n}$ (by compactness), we conclude that we can effectively produce at least one $2^{-n}$ -cover for every n.

The result above should hold for any metric compact structures, e.g., compact Polish groups. Of course, $(1) \rightarrow (2)$ remains the same, but $(2) \rightarrow (1)$ should be carefully verified. We leave this as a conjecture.

Remark 3.8. Note that in the proof, we only need to decide formulae with parameters special points. So it follows that a presentation is decidable with parameters special points iff it is decidable with arbitrary parameters.

3.3. Deciding the intersection

The results in this section appear to be new as state; however, similar arguments and some informal explanations closely related to what we do here can be found in the literature (e.g., in [Reference Hoyrup, Kihara and Selivanov62, Reference Pauly119]). One standard way of using a (finite) cover of a compact space in dimension theory and algebraic topology is to use Alexandroff’s notion of a nerve.

Definition 3.9 (Alexandroff [Reference Alexandroff2]).

A nerve of a cover is a simplicial complex in which the faces are the collections of basic open sets that have a non-trivial intersection.

For example, each basic open set is a zero-dimensional simplex (a node), and balls $\{B,C,D\}$ form a two-dimensional face if $B \cap C \cap D \neq \emptyset $ . From the computability-theoretic standpoint, the issue with this definition is that, for a fixed finite open cover, the non-emptiness of each specific intersection is merely $\Sigma ^0_1$ ; recall Example 2.9 in the preliminaries. Intuitively, most problems arise when the notions “closed ball” and “closure of ball” disagree. This in fact can happen only for countably many radii, and we can find sufficiently small “acceptable radii” [Reference Pauly119]. To state the result formally, we push the notion of computable compactness to its limits.

Definition 3.10. A sequence of basic open balls is $\cap $ -decidable if for every finite sequence of balls $B_0, \ldots , B_k$ from the sequence, we can computably decide whether $\bigcap _{i = 0, \ldots , k} B_i = \emptyset .$

Before we proceed, we state and prove one elementary but important lemma. Recall that, for a basic open B, we write $B^c$ for the basic closed ball with the same centre as B, and that the closure $\overline {B}$ of B does not have to be equal to $B^c$ in general.

Lemma 3.11. Suppose M is computably compact. Then, for basic closed balls $B_i^c$ and $B_j^c$ , the property $B_i^c \cap B_j^c = \emptyset $ is c.e. uniformly in $i,j$ . The same is true for any finite collection of basic closed balls.

Proof The open set $M \setminus B_i^c$ is c.e. Indeed, we just list all the basic open balls that are formally disjoint from $B_i^c$ via a standard argument.Footnote 7 Thus, the union of the complements, which is the complement of the intersection $B_i^c \cap B_j^c$ , is also c.e. open. It covers the space if, and only if, the intersection is empty. By computable compactness of M, this is c.e. The case of finitely many balls is similar.

Definition 3.12. A computably metrized (compact) M is nerve-decidable, or $**$ -computably compact, if for every $n>0$ we can computably find a finite $2^{-n}$ -cover $K_n$ (represented as a finite tuple of basic open balls) of M so that $K_n$ is $\cap $ -decidable uniformly in n.

Theorem 3.13. A computably metrized M is nerve-decidable ( $**$ -computably compact) if, and only if, it is computably compact.

Proof Obviously, $**$ -computably compactness implies computable compactness. To this end, we assume computable compactness of M. We will use the equivalence of computable compactness and $*$ -computable compactness throughout the rest of the proof without explicit reference.

We need to show that, for every $\epsilon>0$ , there exists a finite basic open $\epsilon $ -cover K of the space. Fix a finite $\epsilon /2$ -cover of the space by basic open balls, and replace each ball in the cover with an $\epsilon $ -ball with the same centre. Let S be this new $\epsilon $ -cover. Recall that $B^c$ denotes the basic closed ball with the same centre as B. For each basic open $B_1, \ldots , B_k \in S$ , (exactly) one of the possibilities is realized:

  1. (a) $ \bigcap _{i \leq k} B_i^c = \emptyset $ , or

  2. (b) $\bigcap _{i\leq k} B_i \neq \emptyset $ , or

  3. (c) $ \bigcap _{i \leq k} B_i^c \neq \emptyset $ but $\bigcap _{i\leq k} B_i = \emptyset $ .

Note that there are only finitely many conditions like that in total.

If we shrink the radii of all $B \in S$ by a $\delta <\epsilon /2$ (but keep the same centres), then the conditions of the form $(a)$ will still hold, and the smaller balls will still cover the space because the $\epsilon $ -balls do. If $\delta $ is small enough, then the conditions of the form $(b)$ will still be satisfied, since there are only finitely many conditions like that involved.Footnote 8 The third alternative $(c)$ must be witnessed only by points y such that, for some $B_i = B(c,r)$ , $d(y,c) =r$ . This means that, after the shrinking by $\epsilon /2>\delta >0$ so small that the alternative $(b)$ still holds for each tuple of balls, we completely exclude the third alternative for the new cover.

This argument shows that such a cover exists. Since the conditions are c.e. by Lemma 3.11, it remains to search for a cover such that each finite collection of basic balls in the cover satisfies either $(a)$ or $(b)$ .

By Remark 3.4, we can additionally assume that $K_{n+1}$ formally refines $K_n$ . Clearly, we get the following corollary which will be useful later:

Corollary 3.14. Every computably compact space admits uniformly computable sequence of $2^{-n}$ -nerves (one nerve for each n), where the latter are represented as a finite combinatorial simplices. Furthermore, the formal inclusion between covers $K_{n+1}$ and $K_n$ induces a simplicial map between the respective nerves $;$ these maps are uniformly computable in n. (We cite [Reference Munkres108] for the standard definitions from algebraic topology that we omit here.)

3.3.1. A stronger condition

It will be convenient to have a system of covers $(K_n)$ so that not only each $K_n$ is $\cap $ -decidable but the whole collection $\bigcup _n K_n$ is $\cap $ -decidable. (We strongly conjecture that there is an elementary counterexample.) For instance, we will see soon that having such a stronger system of covers will allow us to computably map $2^{\omega }$ onto the space; this is $(vii)$ of Theorem 1.1.

We are not sure whether such covers can be uniformly constructed for basic open balls with rational radii (represented as a pair of integers), but we can contract such a system for balls with centres in special points and uniformly computable radii.Footnote 9 We call such balls basic computable open.

Definition 3.15. A computably metrized M is strongly computably compact if M admits a system of $2^{n}$ -covers $K_n$ , $n \in \omega $ , by basic computable open balls such that $\bigcup _n K_n$ is $\cap $ -decidable.

Theorem 3.16. A computably metrized M is computably compact if, and only if, it is strongly computably compact.

Proof By slightly increasing the radii of all the balls in a cover, we can ensure their radii are rational. Thus, every strongly computably compact space is computably compact. To this end, we assume the space is computably compact.

The idea behind the proof is as follows. We would like to argue that the idea from the proof of the previous Theorem 3.13 can be iterated. For example, suppose we have come up with a $\cap $ -decidable $K_0$ and need to find $K_1$ so that $K_0 \cup K_1$ is $\cap $ -decidable. But to find such a cover, we might have to slightly shrink the radii of the balls that we have already put into $K_0$ . This is because it could be that for some $B \in K_0$ and C that we attempt to put into $K_1$ , there is a point at distance $r(B)$ from the centre of B that lies in C and is isolated, so there is nothing in $B \cap C$ .

Suppose we iterate the strategy form the proof of Theorem 3.13 and allow the procedure to slightly shrink all the balls in $K_0$ , thus updating the radii of balls in $K_0$ . But note that $K_0$ must still satisfy the closed properties $ \bigcap _{i \leq k} B_i^c = \emptyset $ and finitely many open properties $\bigcap _{i\leq k} B_i \neq \emptyset $ . The former is not an issue since the radii will decrease. The latter, however, needs to be maintained more carefully. When we first discover the finitely many open relations of the form of finitely many strict inequalities (when $K_0$ is first introduced), we also compute a rational parameter $\delta _0>0$ such that the relations will still hold if we decrease the radii of the balls by $\delta _0.$ This is possible since the conditions build down to finitely many strict inequalities involving the radii and computable numbers:

$$ \begin{align*}d(c_i, x_j) < r_i,\end{align*} $$

where $c_i$ are centres of the balls and $x_i$ are special points witnessing that a certain intersection is not empty.

We then define $\delta _{0, n} = 2^{-n-2}\delta _0$ and note that $\sum _i \delta _{0, i} < \delta _0.$ We intend to shrink the radii of each ball in $K_0$ by at most $\delta _{0,s}$ at stage s. This will make the radii in the balls computable while maintaining the finitely many conditions that $K_0$ needs to satisfy.

We also iterate this. When we define $K_1$ , we will have more open conditions to maintain for $K_0 \cup K_1$ . We compute a $\delta _1>0$ and set $\delta _{1, n} = 2^{-n-2}\delta _1$ . We also ensure that $\delta _{1, n} \leq \delta _{0, n}$ , for every n. When we define (our first approximation to balls in) $K_2$ at stage t, we will allow balls in $K_0$ to shrink by at most $\delta _{1, t} \leq \delta _{0,t}$ and balls in $K_1$ by at most $\delta _{1, t}$ . All the finitely many conditions will still be satisfied.

We iterate this process until, in the end of the construction, we finally get a collection of computable balls $\bigcup _n K_n$ . At no stage we are stuck. By the choice of the parameters, all of the open conditions still hold, while the closed conditions will be satisfied vacuously.

Hopefully, the explanation above is sufficiently convincing, but we shall give a formal proof for completeness.

Formal proof.

Lemma 3.17. For every $\epsilon>0$ and $\delta>0$ and any finite collection $K'$ of basic open balls, there exists a finite basic open $\epsilon $ -cover K of the space and a collection of basic open balls $K"$ such that:

  1. (i) Every ball in $K"$ has the same centre as some ball in $K'$ but its radius is at most $\delta $ -smaller.

  2. (ii) For each basic open $B_1, \ldots , B_k \in K" \cup K$ , either $ \bigcap _{i \leq k} B_i^c = \emptyset $ or $\bigcap _{i\leq k} B_i \neq \emptyset $ holds.

Of course, $\bigcap _{i \leq k} B_i^c = \emptyset $ implies $\bigcap _{i\leq k} B_i = \emptyset $ , and thus K in the lemma has computable nerve, and for the same reason $K \cup K'$ is $\cap $ -decidable.

Proof of Lemma 3.17

Fix a finite $\epsilon /2$ -cover of the space by basic open balls, and replace each ball in the cover with an $\epsilon $ -ball with the same centre. Let S be this new $\epsilon $ -cover. Recall that $B^c$ denotes the basic closed ball with the same centre as B.

For each tuple of basic open $B_1, \ldots , B_k \in S \cup K'$ , (exactly) one of the possibilities is realized:

  1. (a) $ \bigcap _{i \leq k} B_i^c = \emptyset $ , or

  2. (b) $\bigcap _{i\leq k} B_i \neq \emptyset $ , or

  3. (c) $ \bigcap _{i \leq k} B_i^c \neq \emptyset $ but $\bigcap _{i\leq k} B_i = \emptyset $ .

Note that there are only finitely many conditions in total.

If we shrink the radii of all $B \in S$ by a $\delta '< \min \{ \delta , \epsilon /2 \}$ (but keep the same centres), then the conditions of the form $(a')$ will still hold, and the smaller balls will still cover the space because the $\epsilon $ -balls do. If $\delta '$ is small enough, then the conditions of the form $(b')$ will also still be satisfied, since there are only finitely many conditions like that involved. Note that the third alternative must be witnessed only by points y such that, for some $B_i = B(c_i,r)$ , $d(y,c_i) =r$ . This means that, after we shrink the radii by $\epsilon /2>\delta '>0$ , $(b')$ will still holds for each tuple of balls, but we completely exclude the third alternative. Define $K"$ to be the balls in $K'$ after the shrinking, and K is the shrunken balls from S.

The rest of the proof proceeds by induction; we iteratively apply Lemma 3.17 to produce a system of covers that satisfies the properties required in the definition of a strongly computably compact presentation. We produce a sequence $(K_n)$ of covers, as follows.

At stage $0$ , search for a finite collection of basic open balls K satisfying conditions of Lemma 3.17 with $\epsilon = \delta = 1$ and $K' = \emptyset $ . Define $\hat {K}_{0,0}$ equal to the first found such K. Also, for the finite collection of strict inequalities that witness non-emptiness of intersections in $K_{0,0}$ calculate a parameter $\delta ' \in \mathbb {Q}$ such that the inequalities would still hold if we decrease the radii by $\delta '$ . Set $\delta _0 = \delta '$ and $\delta _{0,i} = 2^{-i-2}\delta _{0}$ .

At stage $s>0$ , suppose $K_{i, s-1}$ ( $i <s $ ) and $\delta _{s-1, s-1}$ have already been defined. Search for a finite collection of covers K that satisfies the lemma with $K' = \bigcup _{i<s} K_{i, s-1}$ , $\epsilon = 2^{-s}$ , and $\delta = \delta _{s-1, s-1}$ . This will give a finite collection of balls $K"$ having the same centres as balls in $K'$ but perhaps having radii at most $\delta $ -smaller than the radii of the respective balls in $K'$ . For $i<s$ , define $K_{i, s}$ to be the collection of those balls in $K"$ that have the same centre as some ball in $K_{i, s-1}$ . Define $K_{s,s} = K$ , where K is first found satisfying the conditions of the lemma. Compute a rational $\delta '>0$ so small that the finitely many strict inequalities that witness non-emptiness of finite collections of balls in $\bigcup _{i\leq s} K_{i, s}$ will still hold if we decrease all the radii of all balls in $\bigcup _{i\leq s} K_{i, s}$ by $\delta '$ . Set $\delta _{s} = \min \{\delta _s, \delta '\}$ and define $\delta _{s,s} = 2^{-s-2}\delta _{s}$ . Proceed to the next stage.

The verification boils down to noting that at no stage of the construction we are stuck, so $K_{i,s}$ and $\delta _{s,s}$ are defined for every s. This is because of Lemma 3.11 implying that the conditions $(a')$ and $(b')$ are uniformly c.e., and because of Lemma 3.17 saying that balls and parameters with the needed properties exist. Thus, we just search for the first found balls and parameters.

At every stage s, the radii of the balls in $K_{i,s}$ shrink by at most $\delta _{s,s} \leq 2^{-s}$ , which makes each of the radii uniformly approach a computable real number as s goes to infinity. Set $K_i$ equal to these balls that have their radii equal to the limit of the radii of the balls with the same centre in $K_{i,s}$ . When compared to the radius of the ball in $K_{s,s}$ when it was first introduced, the radius of the respective ball in $K_s$ will be smaller by at most $\sum _{n>s} \delta _{n,n} < \sum _{n>s} \delta _{s,n} \leq \delta _s $ , and $\delta _s$ is not greater than the parameter $\delta '$ that was calculated at stage s and that was sufficient to maintain the non-emptiness of finite intersections in $K_{s,s}$ . Since the radii can only decrease, the conditions that say that the closed balls do not intersect will be preserved from a stage to a stage, and in the limit.

It follows therefore that $\bigcup _n K_n$ consists of uniformly computable collection of basic computable balls and is $\cap $ -decidable.

Remark 3.18. The reader should note that, instead of using basic open covers, we could just as well used basic closed covers in the proof of Theorem 3.16. For instance, for any finite collection of basic computable balls $C_0, \ldots , C_k$ , we have $\bigcap _{i \leq k} C_i =\emptyset \iff \bigcap _{i \leq k} C^c_i =\emptyset ,$ where $C_i^c$ is the basic closed ball with the same centre and radius as $C_i$ . Also, by Remark 3.4, we can always assume that $K_{n+1}$ is formally contained in $K_n$ , and this will still be true if we choose working with closed covers. For that, define a new system of (closed or open) covers $K_{f(n)}$ where $f(n)$ is a computable monotone function that grows sufficiently fast so that $K_{f(n+1)}$ formally refines $K_{f(n)}$ .

However, even when we are working with closed basic computable balls, the intersection can always be witnessed by a special point, because the respective open balls intersect too.

Recall that $\overline {C}$ denotes the closure of a basic computable open ball C, and recall that

$$ \begin{align*}C \subset \overline{C} \subset{C^c},\end{align*} $$

and, in general, both inclusions can be strict. But these inclusions also guarantee that we can use closures of the open balls to form covers in Theorem 3.16 and still decide intersection. We can also come up with any combination of open, closed, and closures (e.g., decide whether $B_i \cap \overline {B_j} \cap B^c_k = \emptyset $ ) for any computable balls in K constructed in Theorem 3.16.

Definition 3.19. If a computable sequence $(K_n)$ of finite $2^{-n}$ -covers of computable balls satisfies the properties described in Definition 3.15 then we say that $(K_n)$ is a fully $\cap $ -decidable system of covers of the space. Such a K is given by a uniformly computable sequence of (finite sets $K_n$ of) indices of radii and special points, and we can choose whether we want to consider open, closed, or closures of open balls that have these parameters (see Remark 3.18).

For instance, when we say “ $B^c(r,q)$ is in $K_n$ ” or “ $\overline {B(r,q)}$ in $K_n$ ,” or the same for $B(r,q)$ , we really mean that parameters $\langle r, q \rangle $ are listed in $K_n$ (where q is given as an index of a computable real).

The following lemma will be useful later.

Lemma 3.20. Let $K = \bigcup _n K_n$ be a fully $\cap $ -decidable system of covers of a space M. Then, for every closed ball $D^c$ in K we can enumerate all basic open B in M such that $B \cap D^c \neq \emptyset $ .

Proof Suppose $B \cap D^c \neq \emptyset $ and let x be any (not necessarily special) point in the intersection. Suppose the radius of B is $\delta $ , and let $c_1$ be the centre of B, and $r_1$ its radius. For some positive $\delta $ , we have

$$ \begin{align*}d(x, c_1) = r_1 -\delta.\end{align*} $$

Fix n so that $2^{-n}< \delta /2$ , and consider the finite set $K_n$ . Since $K_n$ is a (closed or open) cover of the whole space, there must exist some $C \in K_n$ such that $x \in C$ . Since $x \in D^c$ , it must be that

$$ \begin{align*}C\cap D^c \neq \emptyset,\end{align*} $$

and (by our assumption) this can be recognised computably. We claim that for this C, we have that C is formally included into B.

Indeed, if $c_2$ is the centre of C and $r_2$ is it radius, then we have that $d(x, c_2) < r_2 \leq 2^{-n} < \delta /2$ , and therefore

$$ \begin{align*}d(c_1, c_2) + r_2 \leq d(x, c_1) +d(x,c_2) +\delta/2 < r_1 - \delta + \delta/2 +\delta/2 = r_1,\end{align*} $$

which is the same as to say that C is formally included into B.

It follows that B intersects $D^c$ if, and only if, there is an $n>0$ and a ball $C \in K_n$ such that $C \cap D^c \neq \emptyset $ and C is formally included into B. This is a $\Sigma ^0_1$ -property.

3.4. Isometry-invariance of computable compactness

Iljazovič [Reference Iljazović65] discovered that the notion of computable compactness admits another characterization that entails that it is isometry-invariant, i.e., every isometrically isomorphic computable metrization of the space must also be computably compact. This property has recently been independently rediscovered in [Reference Pauly, Seon and Ziegler120].

Theorem 3.21. Suppose M is computably compact and N is a computably metrized space isometrically isomorphic to M. Then N is computably compact as well.

We claim that the theorem can be derived as a consequence of condition $\mathrm{(v)}$ in Theorem 1.1:

There is a computable sequence of computable reals $(\epsilon _n)_{n \in \omega }$ such that $\epsilon _n \leq 2^{-n}$ and so that, for every n, we can compute the maximal number of points in the space that are at least $\epsilon _n$ -far from each other (in the sense of strict inequality).

We first prove Theorem 3.21 assuming that $\mathrm{(i)} \leftrightarrow \mathrm{(v)}$ in Theorem 1.1, and then we prove $\mathrm{(i)} \leftrightarrow \mathrm{(v)}$ .

Proof of Theorem 3.21

Assume that, in M, we can compute $(\epsilon _n)_{n \in \omega }$ and the maximal number $D(n)$ corresponding to $\epsilon _n$ . In N, search for $D(n)$ -many special points that are $\epsilon _n$ -far from each other. The $\epsilon _n$ -balls around these points will give a finite cover of the space. We can slightly enlarge the radii to make sure that they are rational.

Proof of $\mathrm{(i)} \leftrightarrow \mathrm{(v)}$ in Theorem 1.1

The proof of Theorem 3.21 above essentially shows that $\mathrm{(v)}$ implies $\mathrm{(i)}$ . Thus, we assume computable compactness and prove $\mathrm{(v)}$ .

The reader perhaps wonders why we did not use $\epsilon _n = 2^{-n}$ in $\mathrm{(v)}$ . To clarify this subtlety, we shall attempt to show that, in a computably compact M, the following invariant $D(M,2^{-n})$ is uniformly computable in n:

$D(M,2^{-n})$ is the maximal number of points of the space M that are $>2^{-n}$ -apart from one another.

The issue that we will face will clarify why we need to adjust our $\epsilon _n$ ’s. Also, it will be easy to modify this naive attempt and obtain a procedure that actually works for some $\epsilon _n \leq 2^{-n}$ .

We describe our attempt. Given $\bar {x} \in M^m$ , we can calculate $\inf _{i<j \leq m} d(x_i, x_j) $ and then

$$ \begin{align*}\sup_{\bar{x} \in M^m} \, \inf_{i<j \leq m} d(x_i, x_j).\end{align*} $$

If this supremum is $< 2^{-n}$ , then m is too large, i.e., $m>D(M,2^{-n})$ . Note that this is a c.e. event. On the other hand, by searching through all possible m-tuples we can bound the maximal number of such points from below. The issue is that the supremum could be exactly equal to $2^{-n}$ , so we may end up with a pair of integers $n_0, n_0+1$ each of which can potentially be equal to the invariant $D(M,2^{-n})$ ; here $n_0+1$ corresponds to the situation when there are $n_0+1$ points at distance exactly $2^{-n}$ from one another.

In this case we shall wait long enough so that any $(n_0+2)$ -tuple has at least one pair of points at distance $> 2^{-n}$ , and for some small $\xi _n < 2^{-n-1}$ there exist $n_0 +1$ points at distance $2^{-n}- \xi _n$ . Then

$$ \begin{align*}D(M,2^{-n}- \xi_n)= n_0+1.\end{align*} $$

This allows us to compute a computable sequence of rationals

$$ \begin{align*}\epsilon_n = 2^{-n}- \xi_n,\end{align*} $$

where clearly $\epsilon _n \leq 2^{-n}$ , such that $D(M,\epsilon _n)$ is a computable sequence of natural numbers. Indeed, for this $\epsilon _n$ there is an $n_0+1$ tuple $\bar {y}_n$ of points that satisfy the desired properties. We can assume these points are special.

It follows from the proof above that these $\epsilon _n$ can be chosen rational and indeed, computed in the strong sense (as fractions). Note that we also obtain:

Corollary 3.22. Suppose that M and N are isometrically isomorphic computable metrized spaces. Then both admit the same modulus of compactness up to Turing degree.

3.5. Calculus of effectively closed sets

In this subsection we present some well-known basic results about effectively closed sets, and we also derive several pleasant consequences of these results that will be important in the sequel. The notion of an effectively closed set is a generalisation of a $\Pi ^0_1$ class, and it is especially useful if the ambient space is effective compact. We will need some basic facts of this generalised theory, but of course a lot more is known (see the very recent large survey [Reference Iljazović and Kihara67]).

Definition 3.23. A closed subset C of a computably metrized M is effectively closed if $M \setminus C$ is c.e. open.

It should be clear that effectively closed sets are closed under finite unions and arbitrary computable intersections (meaning that the effective procedures listing the complements must be uniformly indexed). The following lemma is also an immediate consequence of the definition:

Lemma 3.24 (Folklore).

Suppose $f: A \rightarrow B$ is a computable surjection, and assume C is effectively closed in B. Then $f^{-1}(C)$ is effectively closed (in A).

Proof This is because $A \setminus f^{-1}(C) = f^{-1}(B\setminus C)$ is c.e. open. To see why, recall that f is computable if, and only if, it is effectively open. If a basic open D is enumerated into $B \setminus C$ , then we will list all pairs $(D', D")$ in the continuous name of f such that $D"$ is formally included in D. Since every $x \in D$ is contained in such a $D"$ (by surjectivity), this will give an enumeration of $f^{-1}(D)$ . Putting these enumerations together for all such D in $B \setminus C$ , we will list its preimage.

Another observation is an easy generalization of a well-known fact about $\Pi ^0_1$ classes.

Fact 3.25 (Folklore).

Suppose $P = \{p\}$ is effectively closed singleton in a computably compact space X. Then the only point p of P is (uniformly) computable.Footnote 10

(This can of course be pushed to show that isolated points can also be computed, though non-uniformly.)

Proof Given n, wait for a basic open ball D of radius $2^{-n}$ and finitely many basic open $B_1, \ldots , B_n \in X \setminus P$ such that $D, B_1, \ldots , B_n$ cover X. Then $p \in D$ .

The fact above admits various generalisations, but we will encounter one such generalisation (specifically, in the proof of Corollary 4.11). More generally, effectively closed sets, $\Pi ^0_1$ -classes, computable functions, and computably compact spaces are closely technically related. To make this relationship explicit, we need one more definition. As usual, we identify basic open balls with their indices.

Definition 3.26. A closed subset of a computably metrized M is c.e. if $\{B: B \mbox { basic open and } B \cap C \neq \emptyset \}$ is c.e.

Sets that satisfy the definition above are sometimes called computably overt in the literature. For more about effectively overt spaces, we cite [Reference Brattka and Presser19, Reference de Brecht, Pauly and Schröder23]. The fact below is well-known; we are not sure who was the first to observe this. We cite, e.g., [Reference Brattka and Presser19, Corollary 3.14(1)].

Lemma 3.27. A closed subset C of a computably metrized space M is computably enumerable if, and only if, C possesses a uniformly computable (in M) dense sequence of points.

Note that the dense sequence makes C a computable Polish space under the induced metric.

Proof of Lemma 3.27

Suppose C possesses such a computable sequence $(\alpha _i)_{i \in \mathbb {N}}$ . Then the density of the sequence in C implies that $B_i \cap C \neq \emptyset $ iff $\exists j \alpha _j \in B_i$ , which is a uniformly $\Sigma ^0_1$ statement.

Now suppose C is a computably enumerable closed subset of M. Our goal is to construct a uniformly computable (finite or infinite) sequence of points $(\alpha _i)_{i \in I}$ that is dense in C. The proof below does not have to be non-uniform, but for notational convenience we split it into two cases, namely, when C is finite or infinite.

If C is finite, then it clearly contains only computable points. To see why, assume it is not empty (in this case there is nothing to prove) and let x be any point in C. Take a ball small enough so that $\{x\}\in B\cap C$ . To get a $2^{-n}$ -approximation to x, wait for a basic open $B'$ of radius $< 2^{-n}$ so that $B'\cap C \neq \emptyset $ and additionally $B'$ is formally contained in B.

Without loss of generality, we assume C is infinite. We uniformly approximate a computable sequence by stages. Before we describe stage s, recall that two basic open balls U and W are formally s-disjoint if $r(U) + r(W) < d(cntr(U), cntr(W))$ and this can be seen after calculating the radii and the distance with precision $2^{-s}$ . Then U and W are formally disjoint if they are formally s-disjoint for some s.

At stage $0$ , search for a basic open ball $B_{0, 0}$ of radius ${<}1$ such that $B_{0,0} \cap C \neq \emptyset $ . If such a ball is never found then do nothing. If it is every found, go to the next stage.

At stage $s>1$ first check whether there exists a basic open ball with index $<s$ which is formally s-disjoint from $B_{0, s-1}, \ldots , B_{s-1, s-1}$ . If such a basic open B exists, then choose the first fund $B_{s,s} \subseteq _{form} B$ and $B_{i, s} \subseteq _{form} B_{i, s-1}$ , $i < s$ such that $B_{j, s} \cap C \neq \emptyset $ , the $B_{j, s}$ are pairwise formally disjoint and $r(B_{j, s}) < 2^{-s}$ , $j = 0, \ldots , s$ . Otherwise, if no such B exists, fix the first found pairwise formally disjoint $B_{0,s}, \ldots , B_{s,s}$ that intersect C, have radii $ < 2^{-s}$ , and such that $B_{i, s} \subseteq _{form} B_{i, s-1}$ for $i < s$ (note there is no further restriction on $B_{s,s}$ ). This ends the construction.

Let $\alpha _i$ be the unique point of the Polish space such that $\{\alpha _i\} = \bigcap _{j \geq i} B_{i,j}.$ Since the construction is uniform and the radii of balls are rapidly shrinking, the points $\alpha _i$ form a uniformly computable sequence. Since each of the $B_{i, j}$ ( $j =i, i+1, \ldots $ ) intersects C and C is closed, each $\alpha _i \in C$ . It remains to check that $(\alpha _i)_{i \in \mathbb {N}}$ is dense in C. Let $\overline {(\alpha _i)}_{i \in \mathbb {N}}$ be the completion of $(\alpha _i)_{i \in \mathbb {N}}$ .

Suppose $c \in C$ . We claim that $c \in \overline {(\alpha _i)}_{i \in \mathbb {N}}$ . Assume $c \notin \overline {(\alpha _i)}_{i \in \mathbb {N}}$ , and there is a ball U centred in c which is outside $\overline {(\alpha _i)}_{i \in \mathbb {N}}$ . There will be a basic open ball $B' \ni c$ of radius at most $2^{-n}$ and which is formally contained in U with precision $2^{-n}$ :

$$ \begin{align*}d(cntr(U), cntr(B')) + r(B') < r(U) +2^{-n}.\end{align*} $$

Then at every stage $s>n+4$ the balls $ B_{i,s-1}$ , $i = 0, \ldots , s-1$ will be formally s-disjoint from B, as will be readily witnessed by the metric. At some late enough stage $s'$ we will get a confirmation that $B \cap C \neq \emptyset $ . There exist only finitely many basic balls that have their index smaller than the index of B. Therefore, eventually B will be used to define $B_{t,t} \subseteq _{form} B$ , contradicting the assumption that $U \cap \overline {(\alpha _i)}_{i \in \mathbb {N}} = \emptyset .$

Definition 3.28. A closed subset of a computably metrized M is computable if it c.e. and effectively closed.

As we mentioned immediately after the statement of Lemma 3.27, a c.e. closed subset of a computable metric space M can be viewed as a computably metrized space under the induced metric. It thus makes sense to ask when this subspace is computably compact. If M is computably compact, then it is both computable compact subset of itself and an effectively closed subset of itself. Interestingly, this trivial example is not misleading. The proposition below is also folklore (see, e.g., [Reference Brattka and Presser19, Corollary 4.14(1)]).

Proposition 3.29. For a closed subset C of a computably compact M, the following are equivalent:

  1. 1. C is a computably compact subspace of M.

  2. 2. C is computable.

Before we proceed to the proof, the reader might well wonder what is wrong with the following analog of the classical argument that closed subsets of compact spaces are compact:

Suppose that C is an effectively closed subset of a computably compact space P, then C is computably compact. Applying computable compactness we can compute a finite subcover and then attempt to “throw away” $\overline {C}$ (that can be listed). One obvious problem with this idea is that we can never be sure whether a basic open ball B (in P) intersects C, and thus we can never be sure whether we can keep B in our cover of C. By Lemma 3.27, this is equivalent to locating a computable dense sequence in C. This problem cannot be circumvented as C might not contain a computable dense sequence. Indeed, as Kleene showed in the 1950s there are effectively closed subsets of $2^\omega $ containing no computable points at all. We discuss more about this issue in Section 4. We turn to the proof of Proposition 3.29.

Proof Assume (1). It is clear that C is c.e. (by Lemma 3.27). To list its complement, fix $x \in M \setminus C$ . Let $\delta = \inf _{c \in C} d(x, c)$ . Then any $\delta /4$ -cover of C must be formally disjoint from any ball centred in y with $d(y,x)<\delta /4$ . For every n, fix a finite $2^{-n}$ -cover $\mathcal {K}$ of C. It follows that $M \setminus C$ is equal to the union of the (uniformly) effectively open sets $U_n$ , where

$$ \begin{align*}\{B: B \mbox{ basic open and } B \mbox{ is formally disjoint from every ball in }\mathcal{K}\}.\end{align*} $$

It follows that (2) holds.

Now assume (2). C is computably metrized by Lemma 3.27; let $(y_j)$ be the computable dense subsequence. Fix $\epsilon = 2^{-n}$ . We need to find an $\epsilon $ -cover of C by basic open balls.Footnote 11 Regardless of whether the balls involved are basic or not, as long as their centres and radii are computable, the relation of formal containment remains c.e.

If a finite collection $\mathcal {K}$ of basic open (in C) balls formally contains a cover $\mathcal {K}'$ by basic open (in M) balls, then clearly $\mathcal {K}$ is a cover of C. We claim that this condition is also necessary (for $\mathcal {K}$ to cover C).

From the proof of Lemma 3.3 we know that, for a given cover $\mathcal {K}$ of C by (basic or not) open balls there is a small enough $\epsilon $ such that every $\epsilon $ -cover of C will be formally contained in at least one ball of $\mathcal {K}$ .

Take $\delta = \epsilon /4$ . Fix a finite $\delta $ -cover $\mathcal {K}'$ of C by balls that are centred in special points of M, not C. Every $B' \in \mathcal {K}'$ intersects C at some point x, and by the choice of $\delta $ , $d(x, cntr(B')) +\delta < \epsilon $ , thus $B(\epsilon , x) \supset _{form} B'$ . By transitivity of formal inclusion,Footnote 12 we have that $B'$ must be formally contained in some ball in $\mathcal {K}$ .

By computable compactness of M and computability of C, we can produce at least one $\delta $ -cover $\mathcal {K}'$ of C by basic open balls of M, uniformly in $\delta $ . (To see why, replace every basic open ball in the c.e open name of $M \setminus C$ by the effective union of balls of radii at most $\delta $ that are formally contained in it. This gives a new c.e. enumeration of the complement of C but with balls of radii at most $\delta $ . Then take the c.e. collection of all basic $\delta $ -balls that intersect C. Together these sets of balls cover M. Initiate the combined enumeration of these two c.e. sets and wait until at some finite stage we discover that we have a cover of M.)

Since formal inclusion is c.e., this gives a procedure of listing covers of C by basic balls (in C).

We see that computable compactness and computability of a closed set are very closely related notions. We have already mentioned above that an effectively closed set does not have to be computable, in general. However, suppose C is an effectively closed ( $\Pi ^0_1$ ) subset of, say, $\mathbb {R}^3$ , and suppose further that we know that it is a sphere or a ball. Is it computably closed? Miller [Reference Miller103] used algebraic topology to answer this question in the affirmative (in fact, in any dimension). The idea is that, roughly, we can non-uniformly localise it to a compact box in $\mathbb {R}^n$ and then use that a computably compact ball will eventually be contained in a simplex that “looks like the ball”; algebraic topology helps to make this formal. The results of Miller have been extended (e.g., to compact manifolds under some extra conditions) in [Reference Burnik and Iljazović24, Reference Iljazović64, Reference Iljazović66, Reference Iljazović and Sušić68]. But of course, if we are interested in presentations of spaces and especially up to homeomorphism, then a sphere or a compact surface is clearly homeomorphic to a computably compact space (e.g., given by a geometric realisation of its triangulation).

In general, there is no good reason why a basic closed ball (or the closure of a basic open ball) in an abstract Polish space needs to be computable closed; pathological examples similar to Example 2.9 can be constructed. Interestingly, it follows that there are always enough closed balls with computable radii that are computable closed as sets, and indeed uniformly so.Footnote 13 More specifically, an immediate consequence of the proposition above is that, in Theorem 3.16, we can additionally state that the basic closed balls in the covers are computable closed sets:

Proposition 3.30. Suppose $K = \bigcup _n K_n$ is a fully $\cap $ -decidable system of covers of a computably metrized M. Then each computable closed ball $D^c$ in K is a computable closed set (thus, is a computably compact subspace of M), and this is uniform.

Proof Lemma 3.20 says that each such $D^c$ is c.e. closed. If $x \in M \setminus D^c$ , then x is inside an open ball C that is formally disjoint from $D^c$ , and such balls can be computably enumeratedFootnote 14 . Thus, the c.e. union of such open balls formally disjoint from $D^c$ makes up the complement of $D^c$ .

The fact above will be useful when we talk about the universality of $2^\omega $ . More generally, it seems to be useful in any iterated recursive argument in which a space is eventually replaced by its compact subset, and then a subset of this subset, etc. The lemma below will also be useful throughout the rest of the paper. It is also well-known (see [Reference Weihrauch147, Theorem 3.3] and [Reference Pauly117, Proposition 5.5]).

Lemma 3.31. Suppose $f:X \rightarrow Y$ is a computable map, and assume X is computably compact. Then $f(X)$ is c.e. closed (in Y) and computably compact.

Proof Let $(x_i)$ is a computable dense sequence in X. Then $(f(x_i))$ is dense in $f(X)$ . (Every $\alpha = \lim _j x_j$ for some subsequence $(x_j)$ and, by continuity, $f(\alpha ) = \lim _j f(x_j)$ , so $f(X)\subseteq cl(f(x_i))$ . Suppose $\xi \in cl(f(x_i))$ , say $\xi = \lim _j f(x_j)$ . By compactness, $(x_j)$ has a convergent subsequence $(x_{j_k})$ , so let $z = \lim _k x_{j_k} \in X$ be its limit. Then $f(z) = \lim _k f(x_{j_k}) = \lim _j f(x_j) = \xi $ .)

Given a cover $B_j$ of $f(X)$ by basic open (in $f(X)$ ) balls of radius $2^{-n}$ centred in $f(x_j)$ , calculate the c.e. names of each $B_j$ in Y and begin enumeration of $f^{-1}(C)$ for each such open basic C; note that it could be that some of these $f^{-1}(C)$ will be undefined. At some stage the preimages must cover the whole X. We can see which $B_j$ included the basic open (in Y) balls whose images were sufficient to cover X. This gives a way of producing at least one $2^{-n}$ -cover of $f(X)$ uniformly in n; now apply Lemma 3.3.

Combining Lemma 3.31 with Proposition 3.29, we get:

Corollary 3.32. Suppose $f:X \rightarrow Y$ is computable and X is computably compact.

  • If f is surjective then $Y = f(X)$ must be computably compact.

  • If Y is computably compact then $f(X)$ is a computable closed subset of Y.

In computable algebra, the inverse of a computable bijective map is clearly computable as well. In contrast, there is no reason why the inverse of a computable bijection between spaces has to be computable even if its inverse is continuous (we mention here that this is actually true for isometric maps). The theorem below is elementary and is folklore (e.g., [Reference Brattka, de Brecht and Pauly20, Corollary 6.7]), but it is rather important because it tells us that effectively continuous maps are the right morphisms in the category of computably compact spaces.

Theorem 3.33. Suppose $f: X \rightarrow Y$ is a computable bijection between computably metrized spaces, and assume X is computably compact. Then Y is also computably compact, and $f^{-1}$ is computable.

It is easy to see that f is indeed a homeomorphism.Footnote 15 Our task is to produce a more subtle computable version of this observation.

Proof Computable compactness of Y follows from the corollary above. Given a (not necessarily) special point $y \in Y$ , act computably relative to y. The set $Y \setminus \{y\}$ is effectively open relative to y. Indeed, for every $z \neq y$ there must exist formally disjoint basic open $B \ni y$ and $D \ni z$ . Thus, it is sufficient to list, effectively in y, all basic open balls formally disjoint from some ball in the name of y.

Since f is computable, $f^{-1}(Y \setminus \{y\})$ is effectively open relative to y. Since f is bijective, we have that

$$ \begin{align*}X \setminus f^{-1}(Y \setminus \{y\}) = \{f^{-1}(y)\}.\end{align*} $$

To list a basic open D into the name of $x =f^{-1}(y)$ , wait for finitely many basic open balls $B_1,\ldots , B_k$ in $X \setminus C_0 = f^{-1}(Y \setminus \{y\}) $ such that $D, B_1, \ldots , B_k$ cover X. Note that, for each $D\ni x$ , such a finite collection must exist by compactness. Since X is computably compact, the process described above is uniformly computable in y, and thus $f^{-1}$ is computable.

One useful consequence says that partial inverses also exist under some conditions.

Corollary 3.34. Suppose $f:C \rightarrow M$ is a computable injective embedding of a computably compact C into a computably compact M. Then $f^{-1}$ is computable on $f(C)$ (when viewed as a map between the induced computable structure on $f(C)$ and C).

Proof Let N be the computably compact induced computable metrization of $f(C)$ that exists because of Lemma 3.31 and which is furthermore computably compact by Corollary 3.32 and Proposition 3.29. The map $f: C \rightarrow f(C)$ can be viewed as a computable map from C to the induced computable metrication on C, as follows. When $(B, C)$ is enumerated in the name of f, find a basic open ball D in $f(C)$ that formally contains C. The basic open balls in C are balls with centres that are special in $f(C)$ but are computable in M, but formal containment is still c.e. So we enumerate $(B, D)$ into the new name of f.

Another way to view this is to replace an $\epsilon $ -approximation $x_i \in M$ to $f(y)$ by a $2\epsilon $ -approximation $c_i \in C$ to $f(y)$ ; it must exist.

To compute $f^{-1}$ , apply the previous theorem.

We also include another nice fact connecting computable compactness with computable closed sets proved by Brattka [Reference Brattka17]. The result will be used later (in Corollary 4.3) to clarify one of the well-known applications of computable compactness.

Theorem 3.35. Let X and Y be computably compact spaces and $f: X \rightarrow Y$ . Then f is computable if and only if $graph(f)$ is effectively closed and if and only if $graph(f)$ is computable closed.

Proof We know that $X \times Y$ is computably compact. Suppose f is computable. Then $f(x)=y$ is clearly a $\Pi ^0_1$ property.

Now assume $graph(f)$ is effectively closed. The subspace $\{x\} \times Y$ is effectively closed relative to x, thus $graph(f) \cap \{x\} \times Y $ is an effectively closed singleton relative to x. By Fact 3.25 relativized to x, given x we can compute $(x,f(x))$ and, thus $f(x)$ .

It remains to note that $graph(f)$ is actually c.e. closed for a computable f, because if a basic open B (in $X \times Y$ ) intersects the graph then we will eventually recognise it.

We did not really have to assume that Y is computably compact; the proof would still work. But of course, by Theorem 3.33 the space $f(X)$ has to be computably compact, so we can always replace Y with $f(X)$ .

3.6. Computable universality of the Hilbert cube

We now discuss another way of looking at computably compact spaces, using the Hilbert cube H. In $H = [0,1]^\omega $ , we define the distance as $d((x_i),(y_i)) = \sum _i 2^{-i} d(x_i, y_i)$ . A canonical dense sequence is given by rational sequences that are eventually zero.

The Hilbert cube is a universal space for computably compact spaces. To see this, recall that all our spaces are complete with respect to their metric. We embed a given compact computably metrized space M into the Hilbert cube, as follows. Assume the diameter of M is at most one.Footnote 16 Map a point $x \in M$ to the sequence $(d(x,x_i))_{i \in N}$ in $H= [0,1]^\omega $ .

It is easy to see that this embedding is computable and its image is c.e. closed. We will see that the image does not have to be effectively closed, and hence the image does not have to be computable by Proposition 3.29. This embedding gives yet another characterisation of computable compactness, but this time up to homeomorphism:

Theorem 3.36. For a computably metrized compact M, the following are equivalent.

  1. (1) M is homeomorphic to a computably compact space.

  2. (2) M is homeomorphic to a computable closed subset of H.

Proof Note that H being a (computable) product of computably compact spaces is itself computably compact by Proposition 3.5.

If the space has a computably compact presentation, then its image under the canonical embedding will also be computably compact (Proposition 3.29 and Lemma 3.31), and thus the image will be computable closed by Corollary 3.31. On the other hand, if a closed subset of H homeomorphic to the space is a computable closed subset, then it gives a computably compact homeomorphic presentation of the space by Proposition 3.29 because H, being a (computable) product of computably compact spaces, is itself computably compact.

Remark 3.37. We note that, by Theorem 3.33, if (the fixed computable complete metrization of) M is computably compact, then it is computably homeomorphic to $f(M)$ , meaning that both f and $f^{-1}$ (when restricted to M) have to be computable (see Corollary 3.34).

In other words, we can always effectively reduce the study of computably compact spaces up to homeomorphism to the investigation of computable closed subsets of H. One pleasant and well-known (e.g., [Reference Brattka and Presser19, Corollary 3.14]) characterization of computably closed sets in H is given below.

Lemma 3.38. A closed subset C of H is computable if, and only if, $D(x) = d(x, C)$ is a computable function.

Proof We can list the basic open balls $B(x_i, r)$ for which $D(x_i)>r$ , and they must cover $M \setminus C$ . But we can also list the balls $B(x_j, q)$ such that $D(x_i) <r$ , and these are exactly the basic open balls that intersect C.

Note that we can uniformly list r such that $D(x_i)>r$ , i.e., D is left-c.e. (lower semi-computable) iff C is effectively closed, and we can uniformly list r such that $D(x_i) <r$ , i.e., D is right-c.e. (upper semi-computable) iff C is c.e. closed. We omit details. We also note that there is really nothing special about the choice of H in the lemma above; it could as well be some other computably compact space.

The closed subsets of H give us yet another way to look at computably compact spaces. Recall that compact spaces correspond to c.e. closed subsets of H, and computably compact ones to computable closed subsets of H. Note that the space of all compact (or closed) subsets $\mathcal {C}(H)$ of H is a Polish metric space in which the metric is given by the Hausdorff distance and the countable dense set is given by finite discrete subsets of special points of H.

Fact 3.39 (Folklore).

For a c.e. closed subset C of H, C is computable iff C is a computable point in $\mathcal {C}(H)$ .

Proof If C is computable then it is computably compact by Proposition 3.29. If $(B_i)$ is a finite $2^{-n}$ cover of C and $x_i$ is a special point in $B_i$ , then every point of C is at most $2^{-n+1}$ -far from one of the $x_i$ .

On the other hand, assume $c \in B_i \cap C$ ; indeed c is contained in $B_i$ together with an $\epsilon $ -ball. Thus, there is $\epsilon $ so small that any D that is $\epsilon $ -close to C in $\mathcal {C}(H)$ contains a special point in $B_i$ . This will be eventually recognised, and thus such $B_i$ can be computably enumerated, making C c.e. closed.

Of course, there is again nothing really special about H is the fact and the remark above, and it can be replaced by some other computably compact space if necessary. For instance, one could look at computability of graphs of functions $f: [0,1] \rightarrow [0,1]$ and see that f is computable iff it can be approximated by piecewise linear functions iff the graph is a computable closed set (cf. Theorem 3.35). Generalizations of this fact can be found in [Reference Brattka17].

3.7. Computable universality of Cantor space

We assume that our spaces are non-empty Polish ones, and so that our metrics are complete.

We identify $2^\omega $ with its standard computable presentation of Cantor space by infinite strings under the usual ultrametric. It is well-known that every compact metric space is a homeomorphic image of $2^{\omega }$ ; this is the classical Hausdorff–Alexandroff theorem. The following computable version of this fact fully characterises computable compactness.

Theorem 3.40 [Reference Brattka, de Brecht and Pauly20].

A computably metrized (non-empty) compact M is computably compact if, and only if, there is a computable continuous surjective $f:2^{\omega } \rightarrow M$ .

If M is a computable image of $2^{\omega }$ then it has to be computably compact by Theorem 3.33. To this end, we therefore assume M is computably compact. We give two proofs of the harder direction of the theorem. The first proof exploits the strongest so far combinatorial characterisation of computable compactness given in Section 3.3 (specifically, Theorem 3.16) and basically follows the standard textbook argument pretty closely. The second proof is more indirect. It handles the combinatorics differently using a space-filling curve and a technical Lemma 3.41 that is of independent interest.

The first proof

Fix a fully $\cap $ -decidable system of covers $(K_n)$ of M that exists by Theorem 3.3. By Remark 3.18, we can use finite basic computable closed covers throughout.

We follow the standard classical topological proof very closely, and we use $\cap $ -decidability of $\bigcup _{n} K_n$ throughout. Suppose $K_0 = \{D_1, \ldots , D_{k}\}$ , and fix $D_i \in K_0$ . Then $K_1$ contains finitely many balls that cover $D_i$ ; denote them $D_{i,j}$ . These can be computed and indeed, these $D_{i,j}$ are exactly the closed balls in $K_1$ that intersect $D_i$ , because the rest are disjoint from it. Define $\hat {D}_{\langle i,j\rangle } = D_i \cap D_{i, j}$ .

We can computably proceed by recursion and define $\hat {D}_{\sigma }$ , which is a finite non-empty intersection of basic closed balls, where $\sigma $ ranges over a computably branching tree T with no dead ends (observe that $\sigma \neq \tau $ does not necessarily imply that $\hat {D}_\sigma \neq \hat {D}_\tau $ ). Equip the set of all infinite paths through $[T]$ with the standard (longest common prefix) ultrametric; then $[T]$ is computably metrized space in which the dense sequence is given by $\sigma 1^\omega $ , $\sigma \in T$ . We identify $\sigma $ with the basic clopen ball of $[T]$ consisting of all strings with prefix $\sigma $ .

Also recall that, by the construction of $(K_n)$ , without loss of generality we can assume that basic open balls intersect whenever the respective closed balls intersect, and thus we can always calculate a special point $x_\sigma $ in each $\hat {D}_\sigma $ (see Remark 3.18). We could view $x_\sigma $ to be an $\epsilon $ -approximation to any path in $[T]$ extending $\sigma $ , where $\epsilon =2^{-n+1}$ for the largest n such that a ball from $K_n$ is mentioned in $\hat {D}_\sigma $ . So we define $f(\sigma ) = x_{\sigma }$ with precision $2^{-n+1}$ .

For an infinite path $\xi \in [T]$ , $\hat {D}_{\xi \upharpoonright n} \subseteq \hat {D}_{\xi \upharpoonright m}$ whenever $ m\leq n $ are prefixes of $\xi $ , and since the diameter of $\hat {D}_{\xi \upharpoonright n}$ is at most $2^{-n+1}$ and it is non-empty, we conclude that

$$ \begin{align*}\bigcap_{n} \hat{D}_{\xi \upharpoonright n} = \{\alpha\}\end{align*} $$

for some $\alpha \in M$ . So we set $f(\xi ) = \alpha \in M$ . It is routine to show that the procedure above defines a computable and surjective $f: [T] \rightarrow M$ . It is not difficult to see that $[T]$ is a computable image of $2^{\omega }$ ; as we promised in the preliminaries, we include a proof of this well-known fact.

Claim 1 (Folklore).

  1. (1) If T is a computable, computably branching tree with no dead ends then there is a computable surjective map from $2^{\omega }$ onto $[T]$ .

  2. (2) For every computable, non-empty $\Pi ^0_1$ class C there is a surjective computable map from $2^{\omega }$ onto C.

Proof We first reduce (2) to (1). Realise C as the set of (infinite) paths through a computably branching tree T without terminal nodes, as follows. Computably rearrange T into a new tree $\Gamma $ such that $[T]$ is computably homeomorphic to $[\Gamma ]$ and $\Gamma $ is (at most) binary. To do so, split a node only if both basic clopen sets associated with the two successors of the node in T contain elements of C. (Note that, given a basic clopen set, we can decide whether it intersects C.) Neither $\Gamma $ nor T has terminal nodes, and there is a computable homeomorphism between C and $[\Gamma ]$ .

For (1), we can also reduce the case of an arbitrary computably branching tree to the case when the tree is at most binary. If a node splits into n successors, where $n>2$ , replace it with a gadget in which every node has at most two successors. This gives a computable and (at most) binary tree $\Gamma $ with no dead ends such that $[\Gamma ]$ is computably homeomorphic to $[T]$ .

Thus, it remains to prove (1) for such a $\Gamma $ . Define the map g from $2^{\omega }$ onto $[\Gamma ]$ by recursion. We define the name of g by mapping clopen sets (on)to clopen sets. We also identify finite strings with the respective clopen sets in both trees.

At a stage s, assume g has already been declared on paths/basic clopen sets of length s- $1$ . Suppose $g(\sigma ) = \tau \in \Gamma $ such that $|\tau | = |\sigma | = n-1$ . If $\tau 0$ and $\tau 1$ both exist in $\Gamma $ , then set $g(\sigma 1) = \tau 1 $ and $g(\sigma 0) = \tau 0 $ . Otherwise, without loss of generality, only $\tau 0$ exists. In this case, set $g(\sigma i) = \tau 1 $ for $i=0,1$ . Do that for every string of length n, and then go to the next stage. The map is clearly computable and surjective, and thus induces a computable surjective map of $2^{\omega } $ onto C.

In combination with f defined above, this gives a computable surjection of $2^{\omega }$ onto M.

The second proof

Recall that we assumed that M is computably compact. Without loss of generality, we can assume it is a computable closed subset of H (see Remark 3.37). Recall that there is a computable map from $2^{\omega }$ onto $[0,1]$ ; for instance, map every infinite sequence $\sigma $ in $2^{\omega }$ into the binary expansion $\sum _{i \in \omega } 2^{-i-1} \sigma (i)$ . Also, the famous Hilbert’s curve computably maps $[0,1]$ onto $H = [0,1]^{\omega }$ (see, e.g., [Reference Sagan130] for a primitive recursive version due to Schoenberg). (See [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5] for a detailed explanation of computability of this particular construction. We also cite [Reference Couch, Daniel and McNicholl32] for more about computability of space-filling curves.) This gives a computable surjective $f: 2^{\omega } \rightarrow H \supseteq M$ , and we know from Lemma 3.24 that $f^{-1}(M)$ is a $\Pi ^0_1$ -class which, unfortunately, does not have to be computable in general. Recall that, in the beginning of the subsection, we assumed that M (thus, P) is non-empty. If it were a computable $\Pi ^0_1$ class, then we would be able to computably surjectively map $2^{\omega }$ onto it by Claim 1. But first, we must be in the position to apply the claim. The lemma below helps.

Lemma 3.41. Suppose $f:2^{\omega } \rightarrow K $ is computable, surjective, and $ K$ is computably compact. If $P \subseteq K$ is (non-empty) computable closed, then there is a computable $\tilde {f}: 2^{\omega } \rightarrow K $ and a computable $\Pi ^0_1$ -class $C \subseteq 2^\omega $ such that $\tilde {f}(C) = P$ .

Furthermore, $\tilde {f}$ can be chosen so that $\tilde {f}$ agrees with f on $f^{-1}(P)$ and $\tilde {f}(2^{\omega } \setminus C) \subseteq K \setminus P$ ; we will also include the verification of these properties in our proof below. Also, we will see that the simultaneous construction of $\tilde {f}$ and C is uniform. The proof below is somewhat informal: after all, we have already proven the theorem. We hope that the elementary formal details that are missing should be easy to reconstruct.

Proof This is done as follows. We use a c.e. formal open name of f and computable compactness of K and computability of P throughout. In particular, we will use that f is uniformly computably continuous. This is done by listing $2^{-n}$ -covers $K_n$ of K and using the formal name of f to find a cover S of $2^{\omega }$ such that, for every $\sigma \in S$ there is a $D \in K_n$ so that $(\sigma , D)$ is in the name.

Since P is computable and thus is a computably compact subspace (see Proposition 3.29), we can assume that we know which open sets in $K_n$ intersect P and which do not. To see why, create two lists: one is the list of all finite covers of P, and the second list includes finite collections of basic open balls in K that are formally disjoint from some cover from the first list. For every $\epsilon $ , there is a finite $\epsilon $ -cover $K' \cup K"$ of K, where $K'$ is from the first list and $K"$ is from the second list.Footnote 17 The finite set of balls $K"$ can be empty, but $K'$ is never empty. If $\epsilon = 2^{-n}$ then we can set $K_n = K' \cup K"$ .

The construction of C and $\tilde {f}$ proceeds as follows.

Suppose at a stage we see that, for some basic open set $\sigma $ in $2^{\omega }$ , $f(\sigma ) \subseteq B$ for some $\epsilon $ -ball B such that $B \cap P = \emptyset $ . Then declare $\sigma $ outside of the closed set C that we build, and let (the name of) $\tilde {f}$ copy (the name of) f.

Now suppose, using the same notation and premises, $B \cap P \neq \emptyset $ . It still possible that $f(\sigma ) \cap P = \emptyset $ (because all we know is that $f(\sigma ) \subseteq B$ , so it can miss P), but we do not know that yet. In this case declare that $\sigma $ intersects C and proceed to the next stage. (As we made sure above, for any such B and $\sigma $ that we use at the stage we can decide whether B intersects P or not.)

At the next stage we will find a refined cover of K and $2^{\omega }$ and, in particular, of $\sigma $ . If at least one such $\sigma '$ refining (extending) $\sigma $ has the property that $f(\sigma ') \subset B'$ , where $B' \cap P \neq \emptyset $ (here $B'$ is taken from the more refined cover of K and $B'$ ) then we let (the name of) $\tilde {f}$ copy (the name of) f.

Of course, it is entirely possible that we discover that for all of the finitely many extensions $\sigma '$ of $\sigma $ , the respective ball $B'$ (such that $f(\sigma ') \subseteq B'$ ) does not intersect P. However, we have already declared that $\sigma \cap C \neq \emptyset $ .

In this case, go to the previous stage and find a computable point $x \in B \cap P$ (that can be uniformly extracted from the proof of Lemma 3.27) and declare

$$ \begin{align*}\tilde{f}(\xi) = x\end{align*} $$

for every $\xi \in B$ . In this case we also say that the clopen ball B is declared artificially in C. (This is also the only case when $\tilde {f}$ does not agree with f; we set f and $\tilde {f}$ equal in all other cases.)

By construction, $\tilde {f}$ is well-defined on all of $2^{\omega }$ and is computable. We need to argue that it additionally has the properties claimed in the statement of the lemma.

If $\xi \in B$ then clearly $\tilde {f}(\xi ) \in P$ . If $\xi \in f^{-1}(P)$ then at no stage it can be declared in a ball which is out or artificially in C, so it must be that $\tilde {f}$ and f agree on $\xi $ .

If $\xi $ is such that it is never in any ball that is artificially in or out, it means that for every $2^{-n}$ there must be a point $\alpha _n \in P$ that is $2^{-n}$ -close to $\tilde {f}(\xi )$ , and we see that $\tilde {\xi } = \lim _n \alpha _n \in P$ because P is compact and thus closed.

Finally, $f(2^{\omega } \setminus C) \subseteq K \setminus P$ follows from the fact that if a basic clopen $\sigma $ is declared out of C, we let $\tilde {f}$ follow f in its definition within $\sigma $ .

It follows that M is a computable surjective image of a computable $\Pi ^0_1$ -class. It remains to map $2^{\omega }$ to such class surjectively using Claim 1. This finishes the second proof.

Note that, in the second proof, the combinatorics is handled using Lemma 3.41 rather than using $\cap $ -decidable covers; we did not need them here.

4. Applications

4.1. A few elementary applications of $\Pi ^0_1$ -classes

In this subsection we briefly discuss several applications of effectively closed sets and $\Pi ^0_1$ classes in classical computable analysis. Most of these applications are well-known and are not difficult. However, they serve as a good illustration of the convenience of the techniques we have described in the previous sections. Indeed, in each case we can come up with a brute-force direct proof which would, however, be much less pleasant and often would give a less general result too.

Consider a computable function $f:[0,1]\to \mathbb {R}$ . Then the set of zeroes $Z_f = \{x \in [0,1]: f(x) = 0\}$ is effectively closed in $[0,1]$ . The following result shows that any $\Pi ^0_1$ class can be “realized” as the set of zeros of a computable function. This allows for simple applications of $\Pi _1^0$ classes in real analysis.

Theorem 4.1 (Nerode and Hwang [Reference Nerode and Huang110]).

Given a $\Pi _1^0$ class C (C is thought of a subset of the Cantor set) there is a computable function $f:[0,1]\to {\mathbb R}$ whose zeroes $Z_f = \{x: f(x)=0\}$ exactly the members of C.

Sketch.

Define a computable function by stages on the Cantor set (linear elsewhere) so that, while an interval is not yet declared out of C, f keeps getting closer to $0$ , say, from below. If the interval is declared out, freeze the function at this interval and, thus, keep it away from zero. It shall approach zero but only at points that correspond to paths in C.

Ignoring the $\Pi _1^0$ coding, this method of diagonalization sketched above goes back to Specker [Reference Specker138] and is a mainstay of Aberth [Reference Aberth1], and arguably has roots in the work of Bishop [Reference Bishop11]. We also cite [Reference Brattka, de Brecht and Pauly20, Corollary 3.14] for a more general version of Theorem 4.1.

Here are well-known (cf. [Reference Brattka, de Brecht and Pauly20, Theorem 11.8.3 and Corollary 11.8.4]) easy applications:

Corollary 4.2. For a function $f:[0,1] \rightarrow \mathbb {R}$ , let $Z_f = \{x: f(x)=0\}$ denote the set of its zeros.

  1. (1) There is a computable function $f:[0,1]\to \mathbb {R}$ with uncountably many zeroes and no computable zeroes.

  2. (2) If $f:[0,1]\to \mathbb {R}$ is computable and $Z_f\neq \emptyset $ , then $Z_f$ contains a low point.

  3. (3) If $Z_f\ne \emptyset $ is finite then all of its members are computable.

  4. (4) If $Z_f$ is infinite and countable, then it contains infinitely many computable points.

Proof

  1. (1) Fix an uncountable $\Pi ^0_1$ -class P without computable points and apply Theorem 4.1; for example, some $\Pi _1^0$ class consisting of only Martin-Löf random reals (e.g., [Reference Downey and Hirschfeldt36]).

  2. (2) By Theorem 3.40, there is a computable surjection $g: 2^{\omega } \rightarrow [0,1]$ , and by Lemma 3.41 the pre-image of the effectively closed $X = f^{-1}Z_f$ is also effectively closed in $2^\omega $ , that is, it is a $\Pi ^0_1$ class. Using this argument, we easily see that if $Z_f$ is nonempty then it has a low point, by the Low Basis Theorem.

  3. (3) This is because isolated members of effectively closed sets are computable.

  4. (4) If $Z_f$ is infinite and countable, and thus it has no perfect kernel. In particular, there must be infinitely many isolated points; apply (3).

The elementary corollary below entails that the intersection of two computable closed sets is not computable in general. This unfortunate property of computable closed sets is well-known. The issue is that, although we can list balls that intersect both sets, some balls like that can have no points from the intersection of the closed sets.

To see why the corollary implies this counter-intuitive property of closed sets, note that every non-empty computable closed set has at least one computable point (since it has to be effectively overt).

Corollary 4.3. There exist two computable compact subsets of the unit square $[0,1]^2$ that intersect but have no computable points in the intersection.

Proof In view of Theorem 3.35, it is sufficient to take $C_1 = graph(f)$ for f in (2) of the theorem above, and $C_2 = [0,1]$ (the “x-axis”) which is clearly computable too.

Another application of $\Pi ^0_1$ -classes, similar technically to (1) of Theorem 4.2, is concerned with Markov computability. As mentioned in the introduction, the original definition of computable function used by Turing in [Reference Turing143] was that f is computable if there is a Turing operator taking any computable index of a computable real $\xi $ to some index of the computable real $f(\xi )$ . Note that we could define this notion of computability for a function that is not even defined on non-computable reals, let alone continuity. It is of course much more interesting to have a continuous counter-example.

Theorem 4.4 (Folklore; see Remark 4.5).

There is a continuous, Markov computable $f:[0,1] \rightarrow R$ such that $\sup _{x \in [0,1]}f(x)$ is not computable and, thus, f is not computable (by, e.g., $(1)$ of Proposition 3.5).

The function constructed below, when viewed as a function on computable reals only, has a unique continuous extension on the whole interval $[0,1]$ that cannot be (uniformly, type II, Kleene) computable. Thus, another way to state the theorem is that there is a Markov computable function (which, by definition, can be merely defined only for computable reals) that has a continuous extension on $[0,1]$ but has no computable continuous extension on $[0,1]$ .

Sketch.

This is somewhat similar to the proof of Theorem 4.2(1). Fix a $\Pi ^0_1$ class without computable members and define f on the Cantor set (and linearly elsewhere), but this time make its value approach a left-c.e. non-computable real $\alpha $ . Note that, if a point x is computable, then it has to be either on a segment of the Cantor set that was declared out at some stage, or it is on a linear segment connecting two such points that have been declared out. Observe also that each linear segment connects computable points. In either case, we can wait for the point to be listed in the effectively open complement of the homeomorphic image of the $\Pi ^0_1$ class, go to the stage of the construction where that happened, and compute the index of the image.

Remark 4.5. The first example of a Markov computable function not extendible to a continuous computable one was provided by Aberth (see [Reference Aberth1, Theorem 7.3]). We are not sure who was the first to construct such an example with domain restricted to $[0,1]$ ; this seems to be folklore. The history according to Aberth is in the back of his book [Reference Aberth1, pp. 178–179]. Zaslavskii [Reference Zaslavskiĭ149] was certainly among the first to study various basic properties of Markov computable functions. Similar ideas and constructions are routinely used in reverse mathematics. For example, see [Reference Simpson135, Theorem IV.2.3(2)], which can be viewed as a slight modification of the construction found in Specker [Reference Specker138]. Specker used a $\Pi ^0_1$ class with no computable members to construct a Markov computable function that approaches a computable real from below but does not attain the supremum at any computable point. Simpson uses the same idea to (essentially) construct an example of a Markov computable function on $[0,1]$ that is not even bounded, but the key idea remains the same. We simply slightly modify this construction and make the supremum approach a left-c.e. non-computable real instead of driving it to $\infty $ or to a computable value; the rest remains the same.

Another more recent application of $\Pi _1^0$ classes in computable analysis is by Barrett, Downey, and Greenberg [Reference Barrett, Downey and Greenberg6], and concerns Cousin’s lemma. This is a core lemma in the theory of the Denjoy integral. Recall that a gauge is a function $\delta :[0,1]\to {\mathbb R}^+$ . A tagged partition is a partition $0=a_1<a_2<\cdots a_n=1$ together with a sequence $z_i\in (a_i,a_{i+1})$ . For a gauge $\delta $ we say that a tagged partition is $\delta $ -fine iff for all i, $[a_i,a_{i+1}]\subset (z_i-\delta (z_i),z_i+\delta (z_i))).$ Cousin’s lemma states that for any gauge $\delta $ , there is a $\delta $ -fine partition. Using similar codings to those of Theorem 4.2, we have the following theorem.

Theorem 4.6 (Barrett, Downey, and Greenberg [Reference Barrett, Downey and Greenberg6]).

There is a computable gauge $\delta $ with no computable $\delta $ -fine partition.

Actually this was stated in [Reference Barrett, Downey and Greenberg6] as “RCA $_0$ proves that ‘Cousin’s lemma for continuous functions’ is equivalent to WKL $_0$ .” Many results in Reverse Mathematics concerning WKL $_0$ correlate to coding $\Pi _1^0$ classes. (See [Reference Simpson135].) In passing we remark that in [Reference Barrett, Downey and Greenberg6], the authors looked also at Borel gauges $\delta $ . We say that f is effectively Baire 0 if it is computable, and effectively Baire $n+1$ , if it is the pointwise limit of a computable collection of effectively Baire n functions. In [Reference Barrett, Downey and Greenberg6] it is shown that if $\alpha $ is a computable ordinal, then there is an effective Baire 2 function f such that any $\delta $ -fine partition computes $\emptyset ^{(\alpha )}$ .

4.2. The space of isometries

An isometry is a metric-preserving map. It is clearly continuous. Note that an isometry is always injective, and if f is surjective then we say that it is an isometric isomorphism. Using a brute-force search, we can easily show that the inverse of a computable isometric isomorphism is always a computable map even if the spaces are not computably compact. In particular, we do not need to refer to Theorem 3.33 to compute the inverse of an isometric isomorphism.

Remark 4.7. However, we can argue that its proof can be used to find a more satisfying way to compute it. For instance, we might be able to argue that a primitive recursive procedure might be possible under the right choice of definitions. The subject of primitive recursive or “punctual” analysis (see [Reference Bazhenov, Downey, Kalimullin and Melnikov7, Reference Downey, Melnikov and Ng39]) is largely unexplored. Moreover, connections between polynomial time analysis ([Reference Ko81, Reference Ko and Friedman82]) and compactness also remain to be analysed.

The following result was stated in [Reference Melnikov and Nies99] without proof. As correctly noted in [Reference Franklin and Turetsky44] the space of isometries between any computable Polish spaces can be viewed as a $\Pi ^0_1$ -class in Baire space, but since we are only interested in compact spaces and classes we shall not explain this. The details can be found in [Reference Franklin and McNicholl43].

Theorem 4.8 (Melnikov and Nies).

Suppose $ X$ is computably compact and $ Y$ is computably metrized and is isometrically isomorphic to $ X$ . Under an appropriate coding, the collection of all isometric isomorphisms $Iso( X, Y)$ can be viewed as a $\Pi ^0_1$ -classFootnote 18 .

Proof Unfortunately, the space $C( X, Y)$ of all continuous maps from $ X$ to $ Y$ does not have to be compact. Nonetheless, there are still ways to appeal to the theory of effectively closed and computably compact sets. But it seems easier to just do the coding explicitly.

Recall that an $\epsilon $ -isometry is a function f such that $|d(x,y) - d(f(x), f(y))| \leq \epsilon $ , where $\epsilon>0$ and $x,y$ range over the space. By Theorem 3.21, $ Y$ has to be computably compact as well. Let h be a computable compactness modulus of $ Y$ as defined in Definition 2.7. The idea is that we have at most $h(n)$ -many essential refinements of a given partial $2^{-n+1}$ -isometry from $ X$ to $ Y$ since any other choice will be within a $2^{-n}$ -error. We will also use the fact that every isometric embedding $ X$ in $ Y$ has to be onto, by compactness, and because $ X $ is isometric to $ Y$ . Suppose the special points of $ Y$ are given by the sequence $(r_i)_{i \in \mathbb {N}}$ , and let $(p_i)_{i \in \mathbb {N}}$ be the dense computable sequence in $ X$ . We define a computably bounded tree $B \subseteq \omega ^{ < \omega }$ .

Definition 4.9 (The definition of the tree).

The n-th level of B is given by Gödel numbers of (some) tuples from

$$ \begin{align*}\{r_0, \ldots, r_{h(n)}\}^n\end{align*} $$

that satisfy the $\Pi ^0_{1}$ condition

$$ \begin{align*}|d_Y(r_i,r_k) - d_X(p_i,p_k)| \le 2^{-n+1}\end{align*} $$

for each $i< k <n$ . (Recall h is a computable compactness modulus for $ Y$ .)

We view these tuples $\overline r =\langle r_0, \ldots , r_{n-1} \rangle $ as possible isometric images of $\langle p_0, \ldots , p_{n-1} \rangle $ , up to an error of $2^{-n+1}$ . Thus, we require the $\Pi ^0_{1}$ condition that $|d_Y(r_i,r_k) - d_X(p_i,p_k)| \le 2^{-n+1}$ for each $i< k <n$ . For a tuple $\overline u$ at level n and a tuple $\overline v$ at level $n+1$ , we posit as a further $\Pi ^0_{1}$ condition that v is a child of u if $d(u_i,v_i ) \le 2^{-n}$ for each $i< n$ . We let B consist of all strings $\sigma $ such that for each $n < |\sigma |$ , $\sigma (n)$ is on level n, and if $n>0$ then $\sigma (n)$ is a child of $\sigma (n-1)$ . Then B is $\Pi ^0_{1}$ ; furthermore, clearly there is a function $\hat h \le _{\mathrm {T}} h$ that bounds any $f \in [B]$ .

We claim that $[B]$ codes $Iso( X, Y)$ , in the sense that there is a map from $[B]$ onto $Iso( X, Y)$ . Furthermore, we claim that the map is computable in the sense that there is a computable functional that turns any infinite path through B into an isometry from X to Y.

This is verified below.

Suppose there is an isometric embedding $\Theta \, \colon X \to Y$ . Then let $\pi (n) $ be a tuple of special points on level n that is at distance less than $2^{-n}$ from $\langle \Theta (p_0), \ldots , \Theta (p_{n-1}) \rangle $ . Then $\pi \in [B]$ , and using $\pi $ we can effectively reconstruct $\Theta $ .

Now suppose $ f \in [B]$ . We claim that f uniformly computes an isometric embedding $\Theta _f \colon X \to Y$ . For each i, we have a Cauchy sequence $s^i_n = f(n)_i$ (where $n>i$ ). Thus f uniformly computes the function $\Theta _f$ given by $\Theta _f(i) = \lim _{n>i} f(n)_i$ . For each $i<k <n$ we have

$$ \begin{align*}|d_Y(s^i_n,s^k_n) - d_X(p_i,p_k)| \le 2^{-n+1}.\end{align*} $$

Thus, $\Theta _f$ is an isometric embedding. Note that this is all uniformly effective.

We can now appeal to facts about $\Pi _1^0$ classes.

Corollary 4.10. For a computably compact space X, if $Y \cong _{iso} X$ then there is a low isometric isomorphism witnessing this.

Using different methods, Iljazović [Reference Iljazović65] proved a special case of the next corollary for the case when $Aut_{iso}(M)$ is finite.

Corollary 4.11. Suppose a computably compact X has only at most countably many self-isometries. If $Y \cong _{iso} X$ then there is a computable isometric isomorphism witnessing this.

Proof This follows from the fact that $Iso( X, Y)$ must contain an isolated point. To see why, fix an arbitrary $\psi : X \rightarrow Y$ . Then every isometry $\phi $ from $ X$ to $ Y$ gives an automorphism $\psi ^{-1} \phi \psi $ of $ X$ , and since there are only countably many isometric isomorphisms, there could be only countably many members in $Iso( X, Y)$ . Thus, it cannot be a perfect space, so it must contain an isolated point $\Theta $ .

Take any neighbourhood U in $C(X, Y)$ under the metric

$$ \begin{align*}d(f,g) = \sup_{x \in X} d_Y(f(x), g(x))\end{align*} $$

so that it contains a unique member $\Theta \in Iso(X, Y)$ . If $F: [B] \rightarrow Iso( X, Y)$ is the computable functional from Definition 4.9, then $F^{-1}(\Theta )$ does not have to be a singleton in $[B]$ . On the other hand, $C(X, Y)$ does not have to be compact. Thus, we cannot appeal to Fact 3.25 directly. However, this is not really an issue, because all paths through $F^{-1}(\Theta )$ eventually give very close approximations to $\Theta $ and, thus, we can use any extension that looks good so far (to be clarified). As was pointed out by one of the referees, Fact 3.25 and the argument that we present below admit a generalisation that would suffice, but we give a direct proof.

Fix an n so that $2^{-n}$ is smaller than the diameter of U. Fix a sufficiently long $\sigma \in B$ that:

  1. (1) $\sigma $ is extendible to an infinite path in $[B]$ , and

  2. (2) the F-images of all its extensions in $[B]$ lie in U.

Note that for any such extension $\pi \in [B]$ , we must have $F(\pi ) = \Theta .$

Given $m>n$ , wait for a late enough stage s so that all extensions of $\sigma $ that have not yet been declared out of B have their potential F-images at distance at most $2^{-m}$ from each other. Since $\Theta $ is isolated in $U \subseteq Iso(X, Y)$ and $[B]$ is a $\Pi ^0_1$ class, it follows that such a stage must exist. Choose any such $\rho _m$ extending $\sigma $ that has not yet been declared out of B. It determines a finite partial map that can be used to calculate $\Theta $ to precision $2^{-m+1}$ . It follows that $\Theta $ is computable.

It is natural to ask whether the isomorphism in the corollary above can be reconstructed uniformly from a given pair of compact presentations of the space. The answer to this question is (perhaps, not surprisingly) negative; an intricate example can be found in [Reference Greenberg, Melnikov, Knight and Turetsky53]. The cited paper also contains a subtle definability-theoretic analysis of computably unique metric spaces, i.e., up to computable isometry. It is also known that every compact Polish space admits a Scott sentence of very low complexity (see [Reference Melnikov and Nies99]).

In their very recent paper [Reference Iljazović and Validžić69], Iljazović and Validžić prove two further interesting results generalising Corollary 4.11 and the techniques that Iljazović used in [Reference Iljazović65]. Both results from [Reference Iljazović and Validžić69] can be derived from Theorem 4.8. For example, using clever combinatorial techniques, they show:

Corollary 4.12. In a computably compact metric space, the orbit of a computable point under the action of the self-isometry group is $\Pi ^0_1$ .

We give a proof that uses Theorem 4.8.

Proof Suppose $ X$ is computably compact and consider the presentation $ P = [B]$ of $C( X, X)$ as a computably bounded $\Pi ^0_1$ class given in Definition 4.9. Without loss of generality, we can assume that the computable point that we care about is actually special; if it is not, add it to the computable dense sequence. We can therefore assume $x = p_0$ .

We examine the class $ P$ of all potential partial $2^{-n}$ -isometries and see whether there is an $f \in P$ such that $f(p_0) =y$ . By compactness, this is the same as to say that, for every n, there is a $\sigma \in P$ of length n that codes some $2^{-n+1}$ -isometry $g_n$ mapping $p_0$ to some $r_i \in Y$ with $d(y, r_i)\leq 2^{-n}$ . Note that the existential quantification over such $\sigma $ is computably bounded, since there are only finitely many such $\sigma $ at level n of $ P$ , and we can computably bound this number. Also, the condition $d(y, r_i)\leq 2^{-n}$ is $\Pi ^0_1$ uniformly in n and y. Thus, the overall property of being in the orbit of $x = p_0$ is $\Pi ^0_1$ , uniformly in y and n. In other words, the orbit is effectively closed.Footnote 19

We see that a careful use of $\Pi ^0_1$ classes and effective compactness can help to simplify proofs. Nonetheless, we emphasise again that in this subsection we view spaces up to isometric isomorphism. When we study spaces up to homeomorphism, the situation usually becomes more complex. We will discuss spaces up to homeomorphism a bit later; here we only cite [Reference Neumann111] where it is shown that the closure of the set of orientation-preserving self-homeomorphism of the unit square forms a computable closed set in $C([0,1]^2, [0,1]^2)$ .

We now discuss another corollary that uses index sets to estimate the complexity of the classification problem for compact spaces, up to isometry. Fix an effective listing $(M_i)$ of all (partial) computable Polish spaces. Each such $M_i$ is given by a dense sequence that can be identified with $\omega $ and a (partial) computable metric on it. (The space $M_i$ represents is the completion $\overline {M_i}$ of $M_i$ .) We could list all partial computably compact spaces in a similar way, but this approach is not standard and has never been used in the literature.

Corollary 4.13 (Melnikov and Nies [Reference Melnikov and Nies99]).

The following index sets are arithmetical:

  1. (1) The characterisation problem $\{ i: \overline {M_i} \mbox { is compact} \}$ .

  2. (2) The isometric isomorphism problem $\{\langle i,j \rangle : \overline {M_i} \cong _{isom} \overline {M_j} \, \& \, \overline {M_i}, \overline {M_j} \mbox {are compact} \}$ .

Sketch.

For $(1)$ , say that the metric is total, is indeed a metric, and for every n there is a $2^{-n}$ -cover of the space by closed basic balls.

To see why $(2)$ holds, note that (by Corollary 4.10) it is sufficient to state that there exists a $0'$ -computable isometry. All conditions that express that it “works” are arithmetical.

In contrast with compact spaces, the characterisation problem for locally compact Polish spaces is $\Pi _1^1$ -complete as conjectured in [Reference Melnikov and Nies99] and then formally clarified in [Reference Nies and Solecki113] (the sketch contained in [Reference Melnikov and Nies99] is incorrect). We will return to index sets later when we discuss computable Stone duality.

We now discuss potential converses to Theorem 4.8. Miller (personal communication with Nies) suggested the following example.

Proposition 4.14. Let $A,B \subseteq \mathbb {N}$ be disjoint c.e. sets. There are isometric computably compact computable metric spaces $L, R$ such that any representation of an isometry computes a set S such that $A \subseteq S$ and $B \cap S = \emptyset $ .

Let A and B be disjoint c.e. sets. The collection of separating sets $P=\{X: X\supseteq A\mbox { and } X\cap B=\emptyset \}$ is a non-empty $\Pi _1^0$ class. A pair of c.e. sets A and B is effectively inseparable if there is no computable set C, such that $C\supseteq A $ and $\overline {C}\supseteq B$ . For example, by the proof of the incompleteness theorem, for Peano Arithmetic (PA), the c.e. sets of (Gödel codes for) provable formulae $A = \{\# \psi : PA \vdash \psi \}$ and $B = \{\# \psi : PA \vdash \neg \psi \}$ form an effectively inseparable pair. (For a more straightforward example, consider $A = \{e : \varphi _e(0) = 0\}$ and $B = \{e : \varphi _e(0) = 1\}$ .) If we choose $A,B$ effectively inseparable, then this shows that the $\Pi ^0_{1}$ class of isometries from $ X$ to $ Y$ is Medvedev complete within the $\Pi ^0_{1} $ classes, meaning that whenever there is a member of some other class of degree $\textbf {d}$ then this Medvedev-complete class also has a member of that degree. Thus, the isometries are as complicated as allowed by Theorem 4.8. In particular, there exist isometric computably compact spaces that are not computably isometric.

Proof We describe the metric spaces by giving a connected graph of special points. If there is an edge the distance is defined directly. All the other distances between pairs of special points $p,q$ will be given indirectly as the path distance. We ensure in the construction that this distance function is consistent and computable. There will be only one limit point in the space. Thus the space has Cantor–Bendixson rank $2$ .

Let $\delta _n= 4^{-n}$ . For each n, there are special points $a_n, u_n, v_n, a_{n+1}$ in L that have pairwise distance $\delta _n$ . We call this basic configuration the n-th diamond. The space R looks similar with special points $a_n', u_n', v_n', a_{n+1}'$ sharing the same properties.

At any stage of the construction, the procedure $\textsf {mark}(x, \gamma ) $ , where x is a special point already introduced, adds a new special point y with $d(x,y) = \gamma $ .

Construction of $L,R$ . We may assume at most one number enters $A\cup B$ at any stage.

If $n $ enters A at stage s, call $\textsf {mark}(u_n, 3^{-s})$ and $\textsf {mark}(u^{\prime }_n, 3^{-s})$ .

If $n $ enters B at stage s, call $\textsf {mark}(u_n, 3^{-s})$ and $\textsf {mark}(v^{\prime }_n, 3^{-s})$ .

It is clear that $L,R$ are isometric. Each space is computably compact: let $h(n)$ be so large that the special points up to $h(n)$ include the first $n+1$ diamonds, and the points used for marking up to stage n. Then in either space the special points up to $h(n)$ form a $2^{-n}$ -net. Now suppose that $\Theta \colon L \to R$ is an isometry. The special points $a_n$ and $a_n^{\prime } \ (n>0)$ are singled out by having three points at distance $\delta _n$ , and three points at distance $\delta _{n+1}$ . Thus, $\Theta (a_n)= a^{\prime }_n$ . Therefore $\Theta (u_n) \in \{u_n' , v_n'\}$ . Let $S= \{n \colon \, \Theta (u_n) = u^{\prime }_n\}$ . Then $A \subseteq S$ and $B \cap S = \emptyset $ as required.

Since $d(u_n', v_n') = \delta _n$ , using a term sufficiently far out in the Cauchy name for $\Theta (u_n)$ , we can decide whether $n \in S$ using the representation as an oracle.

We conjecture the following.

Conjecture 4.15. Every $\Pi ^0_1$ -class can be realised (e.g., up to m-degree) as $Iso(M,N)$ for two isometric computably compact spaces.

Conjecture 4.15 holds for computable discrete algebraic structures in the place of effective compact spaces [Reference Franklin and Turetsky44] and we conjecture that it should be possible to turn such structures into compact spaces. Also, as was noted by one of the referees, the simple construction above should have implications at the level of the Weak König’s lemma, under the appropriate coding and in the spirit of the results found in, e.g., [Reference Gherardi and Marcone49, Section 6]. Specifically, among other things [Reference Gherardi and Marcone49] studies the computability-theoretic and reverse mathematical strengths of the Hahn–Banach theorem in Banach spaces. The cited paper also utilises the technique of effective compact sets, but we will not discuss these results here. Instead, we shall discuss the recent results about bases in Banach spaces.

4.3. Basic sequences in Banach spaces

Some of the most used Polish Spaces are Banach spaces, and there is a reasonably well-developed theory of effective Banach spaces beginning with Pour-El and Richards [Reference Pour-El and Richards123]. We note that Banach spaces are usually viewed under isometric isomorphism, and it is well-known that every isometric isomorphism has to be affine (this is the Mazur–Ulam theorem).

Definition 4.16. A computable Banach space is a computably metrized Banach space in which the Banach space operations are computable.

This definition means that any computable Banach space needs to be separable, since it needs a computable dense set. We regard this as presented with a computable norm $||\cdot ||$ , and for simplicity will consider the space as a complete normed vector space B over the reals, although the results also work if the field is the complex numbers.

Some consequences of computable compactness, such as an effective version of the open mapping theorem, can be found in [Reference Brattka15]. We will give a couple of recent applications of computable compactness to the theory of computable Banach spaces. A simple application of computable compactness is Pour-El–Richards’ [Reference Pour-El and Richards124] result that linear independence in a Banach space is $\Sigma _1^0$ . To see this, we note that $\{x_1,\dots ,x_n\}$ is independent iff

$$ \begin{align*}\min_{\lambda_i \in {\mathbb R}\setminus \{0\}}||\sum_{i=1}^n \lambda_i x_i||>0.\end{align*} $$

But by normalizing we can consider the ball

$$ \begin{align*}S=\Big\{(\lambda_1,\dots,\lambda_n)\in {\mathbb R}^{n}\setminus \{0\} \mid \sum_{i=1}^n |\lambda_i|=1\Big\},\end{align*} $$

for the quantification, and this is computably compact, meaning that the minimum $\min _{(\lambda _1,\dots ,\lambda _n)\in S}||\sum _{i=1}^n \lambda _i x_i||$ is $\Sigma _1^0$ .

Almost all elementary linear algebra works via the fact that vector spaces have bases. However, the analog for Banach spaces is not so easy. The most accepted candidate of a basis for a Banach space is called a Schauder Basis.

Definition 4.17. A sequence $X=\{x_i\mid i\in \omega \}$ is called a Schauder Basis for B iff for each $z\in B$ there is a unique sequence $\{\lambda _i \mid i\in \omega \}$ such that

$$ \begin{align*}\sum_{i=1}^\infty \lambda_ix_i=z.\end{align*} $$

Brattka and Dillhage [Reference Brattka and Dillhage18] showed that the theory of computable Banach spaces with well-behaved computable Schauder basesFootnote 20 is relatively well-behaved. In particular, many theorems using duality lift quite smoothly to have computable versions.

However, one of the unfortunate aspects of Banach space theory is that not only don’t (computable) Banach spaces necessarily have computable Schauder bases, but in fact some don’t have Schauder bases at all. This is a remarkable result of Enflo [Reference Enflo40]: There is a separable Banach space with no Schauder basis. (This result solved a question of Banach that had been open for 45 years.) Bosserhoff [Reference Bosserhoff13] proved that Enflo’s construction could be made computable to give a computable Banach space.

The fundamental fact about Schauder bases is the following characterization by Banach.

Lemma 4.18 (Banach).

Let $X=x_1,x_2,\dots $ be a sequence of elements of B. Then this sequence forms a Schauder basis iff:

  1. (1) $x_i\ne 0$ for all i.

  2. (2) The finite span of $\{x_i\mid i\in \omega \}$ is dense in B.

  3. (3) There is a $K\in {\mathbb R}$ such that for all $m<n$ , and all sequences of scalars $\lambda _i$ ,

    $$ \begin{align*}\Bigg|\Bigg|\sum_{i=1}^m \lambda_i x_i\Bigg|\Bigg|\le K\left|\left|\sum_{i=1}^n \lambda_i x_i\right|\right|.\end{align*} $$

K in (3) above is called the Basis Constant bc $(X)$ of the Schauder basis. The hard direction of this lemma is to suppose that X is a basis and consider the projections $S_k(\sum _{i=1}^\infty \lambda _i x_i)=\sum _{i=1}^k \lambda _i x_i$ . We need to prove that $\sum _j ||S_j||$ is finite, and this is achieved by considering the equivalent norm $||\cdot ||'$ defined by $|| \sum _{i=1}^\infty \lambda _i x_i ||'=\sup _m ||\sum _{i=1}^m \lambda _i x_i||.$ This is bounded by the Open Mapping Theorem.

Note that we can also define the basis constant of a space as the infimum of the basis constants of Schauder bases for the space. We remark that there are even finite dimensional spaces without a basis with $K=1$ . But in the finite dimensional case, we can at least get a computable basis constant for the whole space. That is, a simple application of computable compactness yields the following:

Lemma 4.19. Let X be a computable Banach space.

  1. (1) (Bosserhoff [Reference Bosserhoff13]) Assume $x_1,\dots ,x_n \in X$ is a (computable) independent sequence. Then bc $(x_1,\dots ,x_n)$ is a computable real.

  2. (2) (Downey, Long, and Greenberg [Reference Long90]) For a finite dimensional X, bc $(X)$ is a computable real.

Notice that Lemma 4.19 means that each finite dimensional projection in the proof of the existence of K must have a computable basis constant. Therefore the sup K is a computable sup of computable reals. That is K is a left c.e. real for a computable Schauder basis X. In fact, in Long’s M.Sc. thesis [Reference Long90] it is shown that any left c.e. real can be the basis constant of a computable Banach space. It is presently unknown what can be said about the basis constants of computable spaces.

The one theorem we will look at is the following. It provides a counterpoint to the theorem of Metakides and Nerode [Reference Metakides and Nerode100] where they constructed a computable vector space over ${\mathbb Q}$ where every c.e. independent set is finite.

Theorem 4.20 (Downey, Long, and Greenberg [Reference Long90]).

If B is an infinite-dimensional computable Banach space, then B has an infinite dimensional subspace with a computable Schauder basis $Z=z_1,z_2,\ldots $ .

Sketch.

Let $E=\{e_i\mid i\in \omega \}$ be an effective dense set for B. We begin with a lemma of Mazur: If B is an infinite dimensional Banach space and Y a finite dimensional subspace, $\epsilon>0$ then there is $x\in B$ with $||x||=1$ and

$$ \begin{align*}||y||\le (1+\epsilon)||y+\lambda x||,\end{align*} $$

for all $y\in B$ and $\lambda \in {\mathbb R}$ . Since E is dense, it is not hard to show that we may choose $x=e_i$ for some i, by playing with the triangle inequality, choosing one close to x. Now we can follow the classical argument of Banach. Choose a sequence of reals $\epsilon _i$ with $\prod _{i=1}^\infty (1+\epsilon _i)<\infty .$ Then construct the basic sequence in stages. Having constructed $z_1,\dots ,z_n$ , find an $e_i$ in the effectively dense sequence E with bc $(x_1,\dots ,x_n, e_i)\le \prod _{i=1}^{n+1} (1+\epsilon _i),$ and we know by computable compactness, that this procedure is computable.

We will return to Banach spaces a bit later, when we discuss the effective content of Banach–Stone duality that establishes a 1–1 correspondence between computable presentability of Banach spaces in a broad class with computably compact presentability of totally disconnected compact spaces.

4.4. Computable Stone duality with applications

Recall that two basic open balls $B(c_1, r_1)$ and $B(c_2, r_2)$ are formally disjoint if $r_1+r_2< d(c_1, c_2)$ . Two sets of basic open balls are formally disjoint if any pair of basic open balls, one coming from the first set and the other from the second, are formally disjoint. A clopen split of M is a pair of (cl)open sets $X , Y$ such that $X \sqcup Y =M$ .

4.4.1. Computable Stone duality

Various versions of the elementary lemma below can be found in [Reference Brattka, Le Roux, Miller and Pauly21, Reference Harrison-Trainor, Melnikov and Ng59, Reference Hoyrup, Kihara and Selivanov62, Reference Melnikov95], but is some of the cited papers the proof contains minor but misleading errors, thus we give a proof.

Lemma 4.21. Suppose an oracle X can effectively enumerate all basic finite covers of M. Then X can also effectively enumerate all clopen splits of M.

Proof Suppose $M = X \sqcup Y$ is a split, and let $\delta $ be the infimum-distance between these compact open sets

$$ \begin{align*}\delta = \inf_{(x,y) \in X \times Y} d(x,y).\end{align*} $$

(Since $X\times Y$ is compact and d is continuous, it attains its infimum at some pair $(x_0, y_0)$ . In particular, $\delta>0$ .)

Suppose $0< \epsilon < \delta /4$ . Then every finite $\epsilon $ -cover will consist of two formally disjoint subsets of basic open balls. Indeed, every ball covering a point in X cannot contain a point in Y, and every ball covering a point in Y cannot contain a point in X. If a basic open B has its centre in X and D has its centre in Y, then the distance between their centres is at least $\delta $ , while the sum of their radii is at most $\delta /2< \delta $ , making them formally disjoint.

On the other hand, if a finite open cover of M consists of two formally disjoint subcovers, then these subcovers induce a split of M into clopen components. Since the property of being formally disjoint is a c.e. property, X is able to list all such covers.

Another way to state the lemma above is that any modulus of compactness of M can computably enumerate the clopen splits of M. Also note that we could have used $\cap $ -decidable covers in the proof of the lemma above, and this way we can additionally assume that, for the clopen sets that we list, we can additionally decide whether they intersect or not. This will be very convenient in the proof of the next result.

Theorem 4.22 [Reference Hoyrup, Kihara and Selivanov62].

Let M be a computably compact Stone space $(a$ totally disconnected compact Polish space). Then the Boolean algebra of its clopen subsets admits a computable presentation.

Proof Fix a $\cap $ -decidable system of covers $K = \bigcup _{n \in \omega } K_n$ . Using the previous Lemma 4.21, effectively list all clopen splits of M into (open, formally disjoint names of) pairs of clopen sets. Let $(X_i, Y_i)$ be the enumeration of these clopen splits. Note that we can also wait and see whether both $X_i$ and $Y_i$ are non-empty; just wait for a special point to appear in one of the two. In this case we say that the split is proper. This is a c.e. event because $X_i$ and $Y_i$ are both given by their open as well as their closed covers, whichever is more convenient. Thus, without loss of generality we can assume that we list only the proper splits. Write $X^{-1}_i$ for the corresponding $Y_i$ in a proper split; and let $X_i^0$ be another notation for $X_i$ .

The Boolean algebra is generated by the empty set and arbitrary finite non-empty conjunctions of the form $\bigwedge _{i} X^{\epsilon _i}_i$ , where $\epsilon _i \in \{0,1\}$ . Since the system of covers K is $\cap $ -decidable, we can indeed decide whether such a finite intersection is empty. In other words, if F is the free Boolean algebra generated by the $X_i$ , then the Boolean algebra of clopen sets of M is isomorphic to $\frac {F}{I}$ , where I is a computable ideal. This makes the Boolean algebra computable.

Remark 4.23. For a computably compact Stone space, we can uniformly produce the dual Boolean algebra of its clopen sets. (As usual, we assume our spaces are non-empty. Alternatively, we can stretch our terminology a bit and view the one-element lattice as a Boolean algebra.) It is also not difficult to see that the construction is also locally uniform in the following sense. Using clopen components we can produce a computably branching, computable tree T without dead ends such that the space is homeomorphic to $[T]$ . If we take the usual ultrametric on the infinite paths through T, then this metric will be computably compatible with the original metric in the sense that $Id: M \rightarrow [T]$ is a computable map.

This result allows us to establish the following representation theorem.

Theorem 4.24 [Reference Harrison-Trainor, Melnikov and Ng59].

Let M be a computably metrized Stone space. Then the Boolean algebra of its clopen subsets admits a computable presentation.

Proof Let M be the computable space. Recall that $0'$ can compute a modulus of compactness of the space. Relativize the previous theorem to get $0'$ -computable presentation of the Boolean algebra of clopen sets. Given an element of the Boolean algebra, we can use its representation via a finite union of basic computable balls and ask whether there exist two unequal special points $x,y$ that are contained in this clopen set; this is a $\Sigma ^0_1$ property. This element is an atom if, and only if, no such pair of points exists. Thus, the atom relation is also $0'$ -computable. It is well-known that every $0'$ -computable Boolean algebra in which the atom relation is also $0'$ -computable has a computable presentation (see [Reference Knight and Stob80] for the explicit statement and [Reference Downey and Jockusch37] for the first implicit use of this property). It follows that the Boolean algebra of clopen sets has a computable copy.

Given a computable Boolean algebra B, it is not difficult to represent its dual Stone space $\widehat {B}$ as the collection of infinite paths $[T]$ through a computably branching, computable tree T without dead ends (see [Reference Goncharov50] for the details). Thus, we have:

Theorem 4.25 [Reference Harrison-Trainor, Melnikov and Ng59, Reference Hoyrup, Kihara and Selivanov62].

For a countable Boolean algebra B, B has a computable presentation iff its dual Stone space $\widehat {B}$ can be computably metrized iff $\widehat {B}$ has a computably compact metrization.

Corollary 4.26 [Reference Harrison-Trainor, Melnikov and Ng59].

Every computably metrized Stone space is homeomorphic to a computably compact Stone space.

4.4.2. Computable topological vs. computable Polish spaces

The following result is folklore (see, e.g., [Reference Cholak, Coles, Downey and Herrmann31, Reference Tran142]).

Theorem 4.27. For a countable Boolean algebra B, the following are equivalent:

  1. (1) B admits a c.e. presentation.

  2. (2) The dual Boolean algebra $\widehat {B}$ is homeomorphic to a $\Pi ^0_1$ -class.

Idea.

To see why $(1) \Rightarrow (2)$ should hold, think of a $B = A/I$ , where A is atomless and I is a c.e. ideal. One can view A as a full binary tree in which some nodes can be declared equal. Instead of making them equal, we can declare them to be outside of a $\Pi ^0_1$ tree T such that the Stone space of B is $[T]$ . To understand why $(2) \Rightarrow (1)$ should hold, define a c.e. ideal by setting a node x to be equal to the left-most node y at the same level that still remains in the tree (representing the $\Pi ^0_1$ class).

Working independently, Bazhenov, Melnikov, and Harrison-Trainor [Reference Bazhenov, Harrison-Trainor and Melnikov8] proved another closely related and much more subtle computable version of Stone duality. To state it, note that the basic notion of computable compactness (Definition 3.1) can be defined without the assumption that the metric is computable. Definition 3.1 also works for computable topological spaces: just say that we can effectively enumerate all finite covers of the space by basic open sets. In this case we say that the computable topological space is effectively compact. Recall that right-c.e. spaces are computable topological spaces, where the base is given by the basic open balls (see Proposition 2.4). An example of such a right-c.e. “effectively compact” space is any non-empty $\Pi ^0_1$ class. (This requires a relatively straightforward inductive argument that can be found in, e.g., [Reference Bazhenov, Harrison-Trainor and Melnikov8].)

Theorem 4.28 [Reference Bazhenov, Harrison-Trainor and Melnikov8].

For a countable Boolean algebra B, the following are equivalent:

  1. (1) B admits a c.e. presentation.

  2. (2) The dual space $\widehat {B}$ is homeomorphic to an effectively compact right-c.e. completely metrized space.

Idea.

The proof of $(1) \Rightarrow (2)$ is similar to the proof of $(1) \Rightarrow (2)$ the previous theorem. (A non-empty $\Pi ^0_1$ class can be viewed as a right-c.e. metrized space.)

To prove $(2) \Rightarrow (1)$ use a theorem of Odintsov and Selivanov [Reference Odintsov and Selivanov116] who showed that a $\Pi ^0_2$ -presented Boolean algebra admits a c.e. presentation. It is therefore sufficient to show that the Boolean algebra of clopen sets has the form $\beta / I$ , where $\beta $ is the atomless algebra and I is its $\Pi ^0_2$ ideal. This can be done using methods similar to the techniques described in this section; we omit the details.

Recall again that every right-c.e. space is a computable topological space (Proposition 2.4). Recall also that Feiner [Reference Feiner42] constructed an example of a c.e. presented Boolean algebra that does not admit a computable presentation. Thus, Theorems 4.27 and 4.28 imply:

Corollary 4.29 [Reference Bazhenov, Harrison-Trainor and Melnikov8].

There exists a computable topological Polish space that is not homeomorphic to any computably (completely) metrized space.

In spite of appearing as a standard classical result, Corollary 4.29 is very recent. We really have a stronger consequence. In view of Theorem 4.27, it follows also that effective compactness for computably metrized and right-c.e. metrized spaces differ up to homeomorphism.

4.4.3. Applications to classification problems

The next corollary measures the classification problem for compact computable Polish spaces up to homeomorphism. Recall that we fixed an effective listing $(M_i)_{i \in \omega }$ of all (partial) computable Polish spaces. (We identify $M_i$ with the completion of the respective dense computable sequence.)

As was pointed out by Selivanov (in personal communication with the second author), it seems that the corollary below has actually never been explicitly stated in the literature. The corollary is, of course, not really new. Compare the corollary below with Corollary 4.13.

Corollary 4.30. The homeomorphism problem $\{\langle i,j \rangle : M_i \cong _{hom} M_j \, \& M_i, M_j \mbox { are compact} \}$ for computable compact Polish spaces is $\Sigma ^1_1$ -complete.

Proof The $\Sigma ^1_1$ -hardness follows from the $\Sigma ^1_1$ -completeness of the isomorphism problem for computable Boolean algebras [Reference Goncharov and Knight51] and the fact that Stone duality is computably uniform.

We need to argue that the index set is $\Sigma ^1_1$ . We give only a sketch since this fact seems to be well-known. A rather similar fact is folklore in descriptive set theory [Reference Gao47]. A detailed proof in the lightface case (and in the harder context of topological groups) can be found in [Reference Melnikov95]. A very closely related (and, in some sense, stronger) argument is Lemma 3.6 of [Reference Harrison-Trainor and Melnikov58].

It is arithmetical to say that $M_i$ is a (presentation of a) compact Polish space (see (1) of Corollary 4.13). To say that there is a homeomorphism $f: M_i \rightarrow M_j$ , it is sufficient to state that there exist continuous surjective $f_1: M_i \rightarrow M_j$ and $f_2: M_j \rightarrow M_i$ such that $f_1 \circ f_2 = Id_{M_i}$ . Every $g: X \rightarrow Y$ between compact X and Y can be represented by, e.g., a pair $(\tilde {g}, m)$ where $\tilde {g}: \omega ^2 \rightarrow \omega $ and $m: \omega \rightarrow \omega $ , where the function $\tilde {g}(n,k)$ is interpreted as the image of the nth special point with precision $2^{-k}$ , and m as the modulus of uniform continuity.

It is arithmetical to say that $(\tilde {g}, m)$ represents a continuous function $\lim _k g(\cdot ,k): X \rightarrow Y$ . This is because totality is arithmetical, and also one can express that m is a modulus of continuity that works for $\tilde {g}$ as a closed property. Thus, as before, if it fails then it must fail for some special points. Since the continuous image of a compact space is closed, it is arithmetical to say that $(\tilde {g}, m)$ represents a surjective function. (If it does not, then again there is a special point in the complement witnessing this.)

This allows to state the existence of $f_1$ and $f_2$ in a $\Sigma ^1_1$ way. Finally, to say that $f_1 \circ f_2 = Id_{M_i}$ , it is sufficient to say that it is true for special points because the property is (again) closed. This can be expressed arithmetically (in the presentations of) $f_1$ and $f_2$ .

Of course, the result above can be relativized to any oracle, thus implying the classical descriptive-theoretic result saying that the homeomorphism problem for compact Polish spaces is analytic complete.

Remark 4.31. The $\Sigma ^1_1$ -completeness in the proof above is witnessed by computably compact Stone spaces. It is also not difficult to see that the index set of Stone spaces is arithmetical, and thus the homeomorphism problem is actually complete within the class of Stone spaces (that can further be assumed computably compact). To see why saying that $M_i$ is a Stone space is an arithmetical property, iterate the process of splitting the space and search for a non-trivial connected component using Lemma 4.21. Every connected component can be expressed as a finite union of basic open balls, and thus the existence of a non-trivial connected component can be expressed as a first-order, arithmetical property.

A substantially different proof of Corollary 4.30 can be extracted from a closely related result for topological groups established in [Reference Melnikov95]. A computably metrized topological group is a computable Polish space with computable group operations defined on the space. We say that it is computably compact if the space is furthermore computably compact.

Theorem 4.32 [Reference Melnikov95].

The topological isomorphism problem for computably metrized connected compact abelian groups is $\Sigma ^1_1$ -complete.

The proof of the result above uses a computable version of Pontryagin duality that was proved in [Reference Melnikov95] and has recently been extended in [Reference Lupini, Melnikov and Nies91]; we omit the definitions. In fact, it follows from the version of computable duality established in [Reference Lupini, Melnikov and Nies91] that the $\Sigma ^1_1$ -completeness is witnessed by computably compact groups. We now explain how the theorem above gives a different proof of Corollary 4.30. As we shall discuss later in the paper (see Section 4.7, the second proof of Theorem 4.40), using algebraic topology it is possible to show that two compact connected abelian Polish groups are homeomorphic (as spaces) if, and only if, they are isomorphic as topological groups. Assuming this result, Corollary 4.30 follows from the theorem above, but this time the corollary is witnessed by connected computably compact spaces, not totally disconnected computably compact spaces.

To conclude the subsection, we mention one more application of computably compact Stone spaces, this time to Banach spaces. Recall that computable Banach space is a computably metrized Banach space in which the Banach space operations are computable. Recall that Banach–Stone duality states that $C(K_0; \mathbb {R})$ and $C(K_1; \mathbb {R})$ are linearly isometrically isomorphic if, and only if, the respective compact spaces $K_0$ and $K_1$ are homeomorphic. In [Reference Bazhenov, Harrison-Trainor and Melnikov8], a computable version of Banach–Stone duality has been established:

Theorem 4.33. For a countable Boolean algebra B, B has a computable copy iff the space $C(\widehat {B}; \mathbb {R})$ is a computable Banach space.

In view of Theorems 4.27 and 4.28, this correspondence gives an explicit application of computable compactness to computable Banach space theory. In particular, we obtain the following corollary. Fix a computable list $(B_i)_{i \in \omega }$ of all (partial) computable linear spaces over $\mathbb {Q}$ with a computable norm, and write $\overline {B_i}$ for the completion of $B_i$ with respect to its norm.

Corollary 4.34. The linear isometric isomorphism problem $\{\langle i,j \rangle : \overline {B_i} \cong _{iso} \overline {B}_j\}$ for computable separable Banach spaces is $\Sigma ^1_1$ -complete.

Proof We have that $C(\widehat {B_0}; \mathbb {R}) \cong _{iso} C(\widehat {B_1}; \mathbb {R})$ iff $\widehat {B_0} \cong _{hom} \widehat {B_1}$ (iff $B_1 \cong B_2$ ). The proof of aforementioned result from [Reference Bazhenov, Harrison-Trainor and Melnikov8] is uniform when passing from computably compact Stone spaces to the respective Banach spaces. So $\Sigma ^1_1$ -hardness follows from the previous corollary.

It remains to note that the upper bound is also $\Sigma ^1_1$ . It is sufficient to state that there is an isometry that works for special points, maps zero to zero, and is, furthermore, surjective (these properties are closed). The well-known Mazur–Ulam theorem asserts that every isometry with these properties has to be linear.

Further results and open questions related to index sets in analysis, and to compact spaces and compact groups more specifically, can be found in [Reference Downey and Melnikov38].

4.5. Profinite groups

Profinite groups are the Galois groups. They are inverse limits of finite groups. The study of effective profinite groups began with Metakides and Nerode [Reference Metakides and Nerode101], La Roche [Reference La Roche127, Reference La Roche128], and Smith [Reference Smith136, Reference Smith137], where they defined the group to have a co-r.e. presentation if it was isomorphic to a computably bounded $\Pi _1^0$ class $[T]$ (in Baire space) where the group operations were computable. La Roche and Smith defined the group to be recursively presentable (computable) if the set of extendible nodes in T forms a computable set. If F is a computable (countable) field, and K is a c.e. subfield of F, then the Galois group $G(F\backslash K)$ is a co-r.e. profinite group. As Smith [Reference Smith137] observed, Waterhouse’s result [Reference Waterhouse145] can be effectivized to show that each co-r.e. profinite group is effectively isomorphic to $G(F\backslash K)$ for some computable F and K.

A profinite group is recursive if it can be represented as the projective limit of computable linear sequence of finite groups $(F_i)$ given by their strong indices and computable surjective $f_i: F_{i+1} \rightarrow _{onto} F_i$ . Smith [Reference Smith137] showed that a profinite group is recursive if, and only if, it is isomorphic to a decidable computably bounded $\Pi _1^0$ class $[T]$ where the group operations were computable. Since every infinite profinite group is homeomorphic to $2^{\omega }$ , and any two computably compact presentations of $2^{\omega }$ are computably homeomorphic (e.g., [Reference Bazhenov, Harrison-Trainor and Melnikov8]), without loss of generality we can assume that $[T] = 2^{\omega }$ .

A natural question arises what happens when the metric on the group is not necessarily an ultrametric. For example, it is sometimes convenient to think of abelian profinite groups as subgroups of an infinite direct power of the unit circle group.

We give a classification of profinite groups with an arbitrary compatible metric that have a recursive presentation. The result below is new. A similar result that establishes an arithmetical bound without the assumption of computable compactness can be found in [Reference Melnikov95]. Recall that the notion of a computably compact group was defined before Theorem 4.32.

Theorem 4.35. For a profinite group G, the following are equivalent:

  1. (1) G has a recursive presentation.

  2. (2) G has a computably compact presentation.

Proof Clearly, every recursive presentation is computably compact. Now assume we are given a computably compact presentation. Using Lemma 4.21, computably list all clopen components of the group. At this stage there are two ways we can proceed to prove the theorem.

The first possibility is to use the materials of the previous section to construct a computably branching tree T with no dead ends such that the domain of G is $[T]$ , and note that the natural shortest-prefix ultrametric inherited from the tree is computably compatible with the original metric (in the sense that the identity map $G \rightarrow [T]$ is computable; see Remark 4.23). Then we can use the aforementioned result of Smith and conclude that G admits a recursive presentation (i.e., via a surjective linear computable inverse system). We will not give any further details.

The second possibility is to directly calculate the recursive presentation without any reference to effective compatibility and the result of Smith. To make the paper self-contained, we give the details below.

To say that a clopen component is a normal subgroup, use the fact that every clopen component is a computable subspace of the group, and thus is computably compact, by Proposition 3.29. To see if a clopen C is a subgroup, search for a pair of finite covers, say $(B_i)$ and $(D_j)$ , of C such that for every $i,j$ there is a k with the property

$$ \begin{align*}B_i \cdot B^{\prime}_j \subseteq D_k\end{align*} $$

and for every i there is a k such that

$$ \begin{align*}B_i^{-1} \subseteq D_k.\end{align*} $$

We also search for a finite cover $(U_n)$ of G such that for all $n,m$ , and i there is a k with

$$ \begin{align*}U_n^{-1}\cdot B_i \cdot U_m \subseteq D_k.\end{align*} $$

We argue that such a cover exists, and this will imply that we can computably list all clopen subgroups of G. Then we explain how to use these subgroups to build a recursive presentation of the group.

Since the clopen component C can be expressed as a (finite) union of open balls, the preimage of the clopen component under the computable maps $x, y \rightarrow xy$ , $x \rightarrow x^{-1}$ and $z, x\rightarrow z^{-1} x z $ in the respective product space (respectively, $C \times C$ , C, and $G\times C \times G $ ) can be uniformly listed. If C were not a normal subgroup then there will be special points witnessing this, and these would be witnessed together with sufficiently small basic open balls containing them. On the other hand, if C is a normal subgroup then every equation of the form, say,

$$ \begin{align*}z^{-1} x z = y,\end{align*} $$

where $x, y \in C$ and $z \in G$ , would be witnessed by small enough basic open balls containing these points, i.e.,

$$ \begin{align*}U^{-1}\cdot B \cdot U \subseteq D,\end{align*} $$

where $z \in U$ , $x \in B$ , and $y \in D $ . These products of these balls would give a cover of the respective compact product space (in the case of conjugation and in the notation above, $B \times U \times D$ cover $G \times C \times G$ .) It follows that we can find a finite subcover.

We conclude that we can list all clopen normal subgroups of G. Note that, by the uniform computable compactness of each such clopen C, we can compute the diameter of C, which is $\sup _{x,y \in C}d(x, y)$ . Using the techniques of Lemma 4.21 and Theorem 4.22—that basically can be summarised by saying that we take the next cover by very small balls—we can furthermore produce a nested sequence of (finite open names of) clopen normal subgroups $\{C_i: i\in \omega \}$ such that:

  1. (1) $C_{i+1}\subseteq C_{i}$ is formal.Footnote 21

  2. (2) $diam\, C_i < 2^{-i}.$

  3. (3) For every i there exists a computable finite tuple $(x_{i,j})$ of special points (given by its strong index) such that $(x_{i,j} C_i )$ is a cover of G.

  4. (4) For every $i,j, n$ , if $x_{i,j}C_{i+1} \subseteq x_{i+1,n}C_{i+1}$ then this inclusion is formal.

  5. (5) When $j \neq j'$ , $x_{i,j}C_{i+1} \cap x_{i,j'} C_{i+1} = \emptyset $ .

If we succeed, then $\bigcap _{i \in \omega } C_i = \{0\}$ , so it is a uniformly computable basis of clopen normal subgroups of G. We will then use the cosets to calculate the finite $G / C_i$ and the homomorphisms from $G / C_{i+1}$ onto $G / C_i$ .

More formally, we proceed by recursion. Assume $C_{i-1}$ has been defined. We search for a $C_i$ that satisfies all these four conditions. If we drop “formal” in all these conditions, then it should be clear that such a $C_i$ and $x_{i,j}$ must exist. Then fix such a $C_i$ .

By Lemma 4.21 and the analysis of normality above, a normal clopen $C_i$ will eventually be found, and furthermore both $C_i$ and the finitely many cosets mod $C_i$ will be represented as a finite collections of balls. Our task it to show that we can effectively recognise that these finite parameters describing the cosets define what we need. For that, we might need to adjust the finite covers by refining them so that, for instance, the inclusion is witnessed by formal inclusion of covers. This is done as follows.

We satisfy $(1)$ by choosing the radii of a finite cover describing $C_i$ small (see Remark 3.4), and we satisfy $(2)$ by evaluating the computable diameter of the clopen set (this is again essentially done by further refining the cover). Here we use that $C_i$ is indeed a computable closed set because of Lemma 4.21, so we can apply Proposition 3.29.

We elaborate why we will eventually find special points $(x_{i,j})$ and will eventually recognize that they satisfy (3). For that, note that each coset of $C_i$ is open, and thus in particular contains a special point, say x. In particular, every coset mod $C_i$ has the form $xC_i$ . Since for every special x its coset $xC_i$ is the image of $C_i$ under the computable map $y \rightarrow xy$ and $C_i$ is computably compact with all possible uniformity, by Lemma 3.31 we conclude that $xC_i$ is also computably compact, and with all possible uniformity. By refining the cover of $xC_i$ (see Remark 3.4), we can ensure that all set-theoretical inclusions of $xC_i$ into the clopen sets seen so far in the construction hold formally. We can also ensure that if two cosets do not intersect then this is also witnessed formally.Footnote 22 This gives a way of computably recognising condition $(5)$ . We can also wait for finitely many such special points $x_{i,j}$ so that the respective cosets $x_{i,j}C_i$ cover the whole space.

To reconstruct the computable operation on $G / C_i$ , calculate the product and the inverse on the special points $x_{i,j}$ with a sufficient precision until you see that the result is in one of the cosets modulo $C_i$ . This is all computable because the cosets $x_{i,j}C_i$ are (uniformly) given by their finite open covers, and the operations on G are computable.

Finally, use effectiveness of condition $(4)$ to calculate the surjective group-homomorphism $\phi _i:G/ C_{i+1} \rightarrow G/ C_i$ that maps every $x_{i+1, j}C_{i+1}$ to the unique coset $x_{i, j'}C_{i}$ that contains it. This gives a computable surjective inverse system

$$ \begin{align*}(G/ C_{i}, \phi_i)_{i \in \omega}\end{align*} $$

the (inverse, projective) limit of which is topologically isomorphic to G. Since the system is uniformly computable (in the sense of strong indices of finite sets), this gives a recursive presentation of G.

Remark 4.36. In view of the results in the previous subsection that connect c.e.-presented Boolean algebras with $\Pi ^0_1$ -classes, we conjecture that co-c.e. presented profinite groups should correspond to computably compact right-c.e. metrized groups. Melnikov [Reference Melnikov95] gives the first example of a profinite computably metrized group that does not admit a recursive presentation. In view of our theorem above and the results of Smith, the notion of a recursive profinite group seems to be the “right” notion of computability for profinite groups. See [Reference Melnikov95] for a complete description of computably categorical profinite abelian groups and an effective version of Pontryagin duality that works for such groups.

4.6. Computability of Čech cohomology

The earliest application of simplicial homology in computable analysis we are aware of can be found in Miller’s thesis [Reference Miller103] (this application has already been discussed above). Simplicial (co)homology is computable in its nature, and this can be made formal. For example, Chapter 1 (Section 11) of [Reference Munkres108] contains a careful verification of the computability of the homology groups for finite simplicial complexes. This of course entails computability of cohomology groups as well. More specifically, given a (strong index of a) simplicial complex, we can uniformly compute its ith homology group represented as $\bigoplus _{i \leq k} \langle a_i \rangle $ , where $a_0,\ldots , a_k$ are the generators of the group such that the orders of the cyclic $ \langle a_i \rangle $ are also uniformly computable. Since $A^i = Hom (A_i, \mathbb {Z})$ , we can easily observe that respective cohomology groups are also computable in this strong sense.

In this section we extend these results to arbitrary computably compact spaces and their Čech cohomology groups that will be defined shortly. For a finite simplicial complex, its Čech cohomology is isomorphic to its simplicial cohomology (see the last chapter of [Reference Munkres108]). One of the convenient features of Čech cohomology is that it does not rely on triangulation and works for an arbitrary compact metric space.

4.6.1. Background from algebraic topology

Given a compact M, let $\mathcal {N}$ be the directed set of all its finite open covers (under refinement). Since the covers by basic $\epsilon $ -balls, where $\epsilon $ ranges over positive rationals, are cofinal among all covers, without loss of generality we can restrict ourselves only to covers by basic open balls with rational radii. For instance, $\mathcal {N}$ could be the $\cap $ -decidable system of covers nested under formal refinement instead of the usual refinement (at this stage, computability of these conditions is not important).

For each member C of $\mathcal {N}$ , recall that its nerve $N(C)$ is the collection of all sets in the cover that intersect non-trivially. One can view $N(C)$ as a (finite) simplicial complex in which the n-dimensional faces are exactly the n-element subsets X of $N(C)$ such that $\bigcap \{Y: Y \in X \}$ is a non-empty set. For these finite simplicial complexes we can define their cohomology groups $H^*(N(C))$ (with coefficients in $\mathbb {Z}$ ) as follows.

We follow Section 73 of [Reference Munkres108] and define the Čech cohomology group of a compact metrized space as follows. For a fixed finite set of basic open balls $C \in \mathcal {N}$ and the respective simplex $N(C)$ , define the simplicial chain complex as usual:

$$ \begin{align*}\cdots \rightarrow_{\delta_3} A_2 \rightarrow_{\delta_2} A_1\rightarrow_{\delta_1} A_0,\end{align*} $$

where $A_i$ are finitely generated free abelian groups and $\delta _i$ are boundary homomorphisms, and then define the associated cochain complex $A^i = Hom (A_i, \mathbb {Z})$ and define $d_i : A^{i} \rightarrow A^{i-1}$ to be the dual homomorphism of $\delta _{i+1}$ . Then $H^i(N(C)) = Ker(d_{i} ) / Im (d_{i-1})$ is the ith cohomology groupFootnote 23 of the simplex $N(C)$ which is a finitely generated abelian group which can be thought of as given by finitely many generators and relations. Let $H^*(M)$ be the direct limit of $H^*(N(C))$ induced by the inverse system $\mathcal {N}$ under the refinement maps.

4.6.2. The result

Recall that a (discrete, countable) group is c.e.-presented if it is isomorphic to a factor of a computable free group by its computably enumerable subgroup. In other words, the operations of the group are computable by equality is c.e., thus the name.

Theorem 4.37 [Reference Lupini, Melnikov and Nies91].

For a computably compact M, its ith Čech cohomology group admits a c.e. presentation uniformly in i.

A version of this proof for computably compact spaces can be found in [Reference Lupini, Melnikov and Nies91], and similar result for computable Polish spaces (and with a simpler proof, but giving merely $0'$ -computable nerves) is contained in [Reference Melnikov96]. The proof in [Reference Lupini, Melnikov and Nies91] relies on a new constructive version of Čech cohomology that was designed to circumvent the following obvious obstacle: for a given cover, we cannot (in general) compute its nerve. However, Theorem 3.16 tells us that this difficulty can be circumvented even if we use the standard notion of a nerve. Thus, we do not need to out-source to the notationally heavy apparatus of algebraic topology compared to which the somewhat tedious proof of Theorem 3.16 looks rather tame.

Proof of Theorem 4.37

As we noted above, we can assume that we a given a system of $2^{-n}$ covers $\mathcal {N}$ that is linearly nested under formal inclusion and is $\cap $ -decidable; by Theorem 3.16 and Remark 3.18 this can be done computably. We say that a sequence of finitely generated uniformly computable abelian groups $(A_j)$ is strongly completely decomposable if each $A_i$ uniformly splits into a direct sum of its cyclic subgroups, and furthermore the sets of generators of the cyclic summands are given by their strong indices.

Fix a $\cap $ -decidable finite cover C.

Claim 2. The groups $H^i(N(C))$ are strongly completely decomposable (uniformly in C and i).

Proof The finite complex $N(C)$ is computable because the cover C is $\cap $ -decidable. A close examination of the definitions shows that, given C (as a finite set of parameters) and i, we can compute the generators of $A^i = Hom (A_i, \mathbb {Z})$ and compute $d_i$ . We will need the fact below which is well-known (see [Reference Fuchs45] for a proof).

Fact 4.38. Let $G \leq F$ be free abelian groups. There exist generating sets $g_1, \ldots , g_k$ and $f_1, \ldots , f_m$ ( $k \leq m$ ) of G and F, respectively, and integers $n_1, \ldots , n_k$ such that for each $i \leq k$ , we have $g_i = n_i f_i$ .

We can computably find the set of generators $(a_j)$ of $Ker(d_{i} )$ and a set of generators $(b_s)$ of $Im (d_{i-1})$ such that for each s there is an integer m and an index i such that $ma_i = b_s$ ; we know that such generators exist so we just search for the first found ones. It follows that the factor $H^i({N}(C)) = Ker(d_{i} ) / Im (d_{i-1})$ is strongly completely decomposable with all possible uniformity.

Recall that a group admits a $\Sigma ^0_1$ presentation if it is isomorphic to a factor of a computable group by a $\Sigma ^0_1$ subgroup.

Claim 3. The direct limit $\lim _{C \in {\mathcal {N}}} H^i(N(C))$ admits a $\Sigma ^0_1$ presentation.

Proof We can list the $\epsilon $ -covers and decide whether two given basic open balls intersect in the listed covers. The refinement relation between two covers $C\subseteq _{form} C'$ in ${\mathcal {N}}$ induces a simplicial map between the respective nerves ${N}(C)$ and ${N}(C')$ , and this induces a homomorphism between the respective cohomology groups $H^i({N}(C)) \rightarrow H^i({N}(C'))$ . By Claim 2, these finitely generated abelian groups are effectively completely decomposable uniformly in C and i. Note that $Im \, \phi $ is generated in $H^i({N}(C'))$ by the images of the generators of $H^i({N}(C))$ . Similarly to the proof of Claim 2, choose new generators of $H^i(N(C'))$ and $Im \, \phi $ so that the latter are integer multiples of the former. In particular, it is easy to see that $Im \, \phi $ is a computable subgroup of $H^i(N(C'))$ . This means that we can augment $Im \, \phi $ with extra generators in a computable way to expand it to $H^i(N(C'))$ . It follows that

$$ \begin{align*}\lim_{C \in \mathcal{N}} H^i(N(C)) = H^i(G)\end{align*} $$

can be consistently defined as the “union” of the $H^i(N(C)), C \in \mathcal {N}$ , to obtain a group in which the operations are computable and the equality is $\Sigma ^0_1$ . (The equality is merely $\Sigma ^0_1$ because an element $a \in H^i(N(C))$ can be mapped to $0$ in some $H^i(N(C"))$ which appears arbitrarily late in the directed system.)

This finishes the proof of the theorem.

We will also see that in Theorem 4.37 “uniformly c.e. presented” cannot be improved to “uniformly computably presented”; this is Corollary 4.43. (In fact, in the example given in the next subsection each individual cohomology group will actually have a computable presentation, just not uniformly so.)

4.6.3. Applications

Perhaps the most significant application to date is computability of Pontryagin duality for computably compact connected groups (see [Reference Lupini, Melnikov and Nies91]); we omit the definitions. Further applications of computability of cohomology include various index set results in topology (see [Reference Lupini, Melnikov and Nies91]). One sample result is:

Corollary 4.39 [Reference Lupini, Melnikov and Nies91].

The index set of solenoid spacesFootnote 24 is arithmetical among all compact Polish spaces.

It follows that in any class of compact manifolds in which non-homeomorphic members have non-isomorphic cohomology groups (for some i), the homeomorphism problem is arithmetical provided that the respective cohomology groups have arithmetical isomorphism problem. The significance of this fact is that, in general, even if a computably metrized manifold admits a triangulation, it is not known whether it always admits an arithmetical triangulation.Footnote 25 Indeed, even in the seemingly trivial case of compact surfaces, producing an arithmetical triangulation based entirely on the given metric takes some $18$ Turing jumps [Reference Harrison-Trainor and Melnikov58]. It is believed that complexity is likely close to being optimal. In contrast, calculating Čech cohomology groups allows to completely avoid triangulation (that does not even have to exist, let alone an arithmetical triangulation). Some further discussion can be found in [Reference Harrison-Trainor and Melnikov58].

In the next subsection we discuss how Čech cohomology can be used to find a computably metrized space not homeomorphic to a computably compact one.

4.7. Computably metrized spaces not homeomorphic to computably compact ones

As we noted in the introduction, finding an example of a computably metrized compact space not isometric to a computably compact one is easy: just take $[0,\alpha ]$ for a left-c.e. non-computable real $\alpha $ . The situation is significantly more difficult if we want to work up to homeomorphism. For instance, we have seen that every computably metrized Stone space is homeomorphic to a computably compact one, so no such example can be found among totally disconnected compact Polish spaces.

It seems that constructing such an example necessarily requires some relatively advanced techniques. A few years ago, a closely related result was established by Bosserhoff and Hertling [Reference Bosserhoff and Hertling14]: For any $n\geq 2$ there exists a c.e. compact subset $C \subseteq \mathbb {R}^n$ such that $\phi (C)$ is not computable compact for any self-homeomorphism $\phi $ of $\mathbb {R}^n$ . However, the result and the techniques that were used to establish it are restricted to $\mathbb {R}^n$ . Hoyrup, Kihara, and Selivanov [Reference Hoyrup, Kihara and Selivanov62] were the first to announce a general construction of a computably metrized space that is not homeomorphic to any computably compact space. Using completely different techniques, a connected example has recently been suggested in [Reference Lupini, Melnikov and Nies91].

We outline two constructions of a compact computable space not homeomorphic to any computably compact space. The first proof is more similar to what Hoyrup, Kihara, and Selivanov [Reference Hoyrup, Kihara and Selivanov62] announced; it will be given in almost complete detail. The second proof can be found in [Reference Lupini, Melnikov and Nies91]. It produces a relatively natural example using Pontryagin–van Kampen duality; because too much background is necessary to fully explain the proof, we will only briefly sketch it here. Both proofs rely heavily on Čech cohomology. Finally, we will briefly discuss whether we can completely avoid cohomology to prove the theorem below.

Theorem 4.40. There exists a computably (completely) metrized compact Polish space not homeomorphic to any computably compact space.

First proof of Theorem 4.40

The proof is very similar to the one given in Hoyrup, Kihara, and Selivanov [Reference Hoyrup, Kihara and Selivanov62]. The proof that we give here replaces the most complex definability part of their proof with an argument that involves computability of Čech cohomology first established in [Reference Lupini, Melnikov and Nies91] and then improved in the proceeding subsection.

The definition below “encodes” a set into a space. We view an isolated point as a $0$ -sphere $S^0$ .

Definition 4.41. For a set $X \subseteq \omega $ , let $CP(X)$ be the one-point compactification of the disjoint union of spheres $S^k$ , with infinitely many copies for each $k \in X$ .

One way to think about $CP(X)$ is as follows. Fix a fishbone (a 1-atom) in the Cantor space $2^\omega $ in which every isolated path (an atom) is replaced with a copy of $S^k$ for some $k \geq 0$ .

Proposition 4.42.

  1. (1) X is $\Sigma ^0_3$ if, and only if, $CP(X)$ is computably (completely) metrizable.

  2. (2) X is $\Sigma ^0_2$ if, and only if, $CP(X)$ admits a computably compact presentation.

Proof (1) Recall that using a modulus of compactness we can find a split of a computable Polish space into two clopen subspaces, as explained in Section 4.4. Recall also that $0'$ can compute a modulus of compactness. Also, a space is connected if it does not have a non-trivial clopen split. Thus, $0"$ can produce a uniform list of computable indices of the clopen connected subspaces of $CP(X)$ . Each such index is a finite collection of (open or closed) open balls that contain (only) the component. For a (finite) simplicial complex, Čech cohomology groups are isomorphic with the respective simplicial cohomology groups (see the final chapter of [Reference Munkres108]). For the n-sphere we have:

$$ \begin{align*}H^p(S^n) \cong \mathbb{Z} \mbox { iff } p=0, n,\end{align*} $$

and it vanishes otherwise.

Suppose that we know that a computably mertrized M is homeomorphic to $S^k$ , $k>0$ , but we do not necessarily know what this k is. The modulus of compactness of each connected component of M is $0'$ -computable uniformly in the finite set of parameters that isolates this component. Since the Čech cohomology groups are uniformly $\Sigma ^0_2$ -presentable (by Theorem 4.37 relativized to $0'$ ), in this case $M \cong S^k$ is equivalent to saying that $\check {H}^k(M)$ contains at least one non-zero element, which is a $\Sigma ^0_3$ property (the equality in the group is $\Sigma ^0_2$ ). It follows that $0"$ can list the components for which the kth cohomology group is non-trivial, and it can also list such $k>0$ . The set of these k is equal to X.

Now we prove that, given $X \in \Sigma ^0_3$ , we can produce a computable metric on $CP(X)$ . Represent $\Sigma ^0_3$ as the set of all k such that $\exists x \exists ^\infty y R(x,y,k)$ , for some computable predicate $R \subseteq \omega ^3$ (see [Reference Rogers129]). Say we are testing whether $k \in X$ , $k>0$ . For each existential witness x corresponding to k, create a new component and do more steps in making it look like $S^k$ . This is done by enumerating more points into the components when more $ \exists ^\infty $ -witnesses are found for the given existential witness x; abandon the finitely many points until the next expansionary stage.

This gives a uniformly computable sequence of spaces; each space is either finite discrete or is equal to $S^k$ . We can make sure there are infinitely many copies $S^k$ for each $k \in X$ . Put them together (uniformly shrink the ith component by $2^{-i}$ and use an ultra-metric of the Cantor space to define the distance between different components).

(2) It follows from the material in Section 4.4 that, using computable compactness we can list indices (names) clopen connected components of a (compact) space using $0'$ . It also follows from Proposition 3.30 that each component can be viewed as a computable closed subset of M (being a finite union of computable sets), and thus it is also computably compact uniformly in its name.

Computable compactness makes the Čech cohomology groups uniformly c.e.-presented, and saying that it is not trivial is now merely $\Sigma ^0_2$ . This makes X a $\Sigma ^0_2$ -set.

For the other direction, given a $\Sigma ^0_2$ infinite X, represent it via $\exists \forall $ . Assume we are guessing whether $k \in X$ . For each $\exists $ -witness keep building a computably compact copy of $S^k$ unless a counterexample to the universal quantifier is found (in which case abandon the component). Then put the spaces together as before, but this time observe the space is computably compact since each component can be easily made uniformly computably compact.

It remains to fix a $\Sigma ^0_3$ -complete set X.

Corollary 4.43. Theorem 4.37 cannot be improved to state that the Čech cohomology groups are uniformly computably presented.

Proof Let X be $\Sigma ^0_2$ -complete and consider $CP(X)$ defined above. Then $CP(X)$ admits a computably compact presentation. In fact, the construction of $CP(X)$ is based on the uniform construction of a sequence of computably compact disjoint components, each being either $S^k$ or a finite union of isolated points.

Assume that the Čech cohomology groups were uniformly computably presented in general (and for these components in particular). It is well-known that the cohomology of a finite disjoint union is the direct sum of the cohomologies of the components; this follows from Mayer–Vietoris sequence calculations [Reference Munkres108]. Thus, the components that are a finite union of isolated points will have trivial cohomology groups for $i>0$ . Also, by assumption, saying that the ith computable cohomology group has a non-zero element is now $\Sigma ^0_1$ . Thus, to decide if $i \in X$ ( $i>0$ ) it is sufficient to ask whether there is a component whose ith cohomology group is non-trivial, and this is also $\Sigma ^0_1$ contradicting the choice of X.

As we already mentioned above, Khisamiev [Reference Khisamiev78] showed that every c.e. presented torsion-free abelian group has a computable presentation. All known proofs of this result are non-uniform, but the only non-uniformity comes from deciding whether there is a non-zero element on the group. As a biproduct of the proof of the corollary above, it follows that this obstacle cannot be circumvented.

The basic idea of the first proof above was to code information into connected components of the space. Producing a connected example seems to necessarily require some advanced techniques that are outside the scope of this paper. We outline an argument that relies on the recent results from [Reference Lupini, Melnikov and Nies91, Reference Melnikov96] and which gives a connected example of covering dimension 1. We leave many terms and notions undefined (see [Reference Lupini, Melnikov and Nies91, Reference Melnikov96] for the definitions and more explanation).

Second proof (sketch)

For a discrete torsion-free abelian group G, the first Čech cohomology group of the space of its compact connected Pontryagin–van Kampen dual $\widehat {G}$ is isomorphic to G (see, e.g., Part 5 of Chapter 8 of [Reference Hofmann and Morris61]). Using the aforementioned result of Khisamiev and two new computable versions of Pontryagin–van Kampen duality from [Reference Lupini, Melnikov and Nies91, Reference Melnikov96] we can conclude that, for some broad enough class of groups, namely q-divisible groups, G has a $\Delta ^0_2$ -presentation iff $\widehat {G}$ is computably metrizable, and G has a computable presentation iff $\widehat {G}$ has a computably compact presentation. As there are plenty of $\Delta ^0_2 \ q$ -divisible groups that have no computable presentation (including examples having X-computable copies iff X is non-low [Reference Melnikov93, Reference Melnikov96]), the result follows. Indeed, we can find a subgroup of the rationals with this property; this will give a connected example of a solenoid space that satisfies the theorem. In particular, there exist examples like that having covering dimension 1.

We conjecture that one can completely avoid using homological algebra to prove Theorem 4.40. We suspect that one way to do this would rely on a combinatorially involved construction similar to one that can be found in [Reference Harrison-Trainor, Melnikov and Ng59]. We outline a plan of this argument; a detailed verification would take too much space (if it works).

Cohomology-free proof idea (for Theorem 4.40)

An n-star is a Wedge sum of n-copies of the unit interval (identify the left most-points of n copies of $[0,1]$ ). The basic idea here is to replace n-spheres with n-stars in the previously discussed proof of Theorem 4.40. A $0$ -star is just an isolated point. One can use a fairly basic technique of $\epsilon $ -chains to produce a $\Sigma ^0_4$ -enumeration of the set of $n \in \mathbb {N}$ such that the space has an n-star component. As has been suggested by Ng (personal communication with the second author), under the assumption of computable compactness, this definition should become $\Sigma ^0_3$ . It remains to prove that, given a $\Sigma ^0_4$ -set, we can produce a computably metrized (compact) space that codes the set into its n-star components. This requires a relatively involved priority construction that can be viewed as a $0"'$ -argument (see [Reference Harrison-Trainor, Melnikov and Ng59]). In [Reference Harrison-Trainor, Melnikov and Ng59], we can find a construction of this sort that produces a locally compact space. As explained in [Reference Harrison-Trainor, Melnikov and Ng59], we can use the 1-point compactification of this space to produce a compact space.

It is not clear at all whether this approach (if it works) is any simpler than the approach that uses cohomology since it relies on a $0"'$ -argument.

4.8. Computable universality of $C[0,1]$

Fix the standard computable presentation of $C[0,1]$ under the supremum metric given by piecewise linear functions with finitely many rational breaking points. We should note that there are also “non-standard” computable presentations of this space that are isometric but not computably isometric to the standard one. We also cite [Reference Bazhenov, Harrison-Trainor and Melnikov8, Reference Melnikov and Ng98] for further results about the computability-theoretic aspects of this space. The theorem below has recently been established in [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5] using a direct combinatorial argument. We give a new proof that uses computable compactness to sort out the combinatorics.

Theorem 4.44. Every computably (completely) metrized Polish space can be computably isometrically embedded into $C[0,1]$ .

It is known that $C[0,1]$ is actually not computably unique up to computable linear isometry [Reference Melnikov94, Reference Melnikov and Ng98]. We prove the theorem for the “natural” computable presentation of the space given by, e.g., piecewise linear functions with rational parameters.

Proof It is sufficient to computably embed the Urysohn space $\mathbb {U}$ into the natural computable presentation of $C[0,1]$ . It is known (and is not hard to show) that it is computably universal in the sense that every computable Polish space can be computably isometrically embedded into the Urysohn space (see [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5, Reference Kamo77]). There is no ambiguity here because the Urysohn space admits a unique computable presentation, up to computable isometry [Reference Melnikov94]. It is also known that the original construction of Urysohn is actually primitively recursively universal [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5], but unfortunately the space is no longer primitively recursively unique (categorical). For the present proof, we shall only need the (general recursive, Turing) computable universality of $\mathbb {U}$ . For a related construction of the Urysohn metric space in constructive setting without choice principles, we cite [Reference Lešnik89].

We return to the proof. Recall that $\mathbb {QU} = (p_i)_i$ , the rational Urysohn space, is dense in $\mathbb {U}$ . It is also known that the distances between special points $p_i$ and $p_j$ are rational numbers uniformly computable from $i,j$ (as fractions).

In the Hilbert cube, basic open box is a product of intervals only finitely many of which are open rational sub-intervals of $[0,1]$ and the rest are $[0,1]$ . It is clear that basic open boxes are effectively open. We computably adjust the metric in the Hilbert cube and view it as $H = [-d(p_0, p_n),d(p_0, p_n)]^\omega $ , and thus adjust the notion of a basic open box accordingly.

Observe that

$$ \begin{align*} -d(p_{0},p_{n})\leq d(p,p_{n})-d(p,p_{0})\leq d(p_{0},p_{n}), \end{align*} $$

for any $p_n$ . Say that a point $\xi $ in $H = [-d(p_0, p_n),d(p_0, p_n)]^\omega $ corresponds to $p_j$ if the projections $\pi _n(\xi )$ of the point to the edges of the cube are exactly the

$$ \begin{align*}\gamma_n(p_j) = d(p_j, p_n) - d(p_j, p_0),\end{align*} $$

and let U be the collection of all such points. We can effectively enumerate U as a sequence of computable points.

Lemma 4.45. $P=cl(U)$ is computable closed.

Proof Since we can list U which is dense in $cl(U)$ , by Lemma 3.27 it is sufficient to show that $cl(U)$ is effectively closed. One way to do this is as follows.

Say that reals $d_1, ..., d_k$ are legit if there is a real d such that

$$ \begin{align*}\{ d(p_i, p_j), d, d_1+d, ..., d_k+d, i<j \leq k \}\end{align*} $$

is a diagram of a metric space (on points $p_i, p$ ), where $d_i = d(p, p_i) - d(p, p_0)$ and $d = d(p, p_0)$ . Recall also that $\mathbb {U}$ has the extension property; in other words if there is a finite metric space extending $p_0, \ldots , p_{k}$ then it is isometrically embeddable to $\mathbb {U}$ over $p_0, \ldots , p_{k}$ . The existence of a 1-point extension $p,p_0, \ldots , p_{k}$ is equivalent to saying that $d_0, \ldots , d_k$ are legit, where $d_i = d(p, p_i) - d(p, p_0)$ , as witnessed by $d = d(p, p_0)$ .

Claim 4. We can decide whether a given basic open box in H contains a legit tuple.

Proof There is a first-order formula in the language of $(R, +, \times , 0)$ that says that, for some real d and reals $d_1, \ldots , d_k $ that range between some fixed rational parameters (describing the intervals in a given open box), $\{d(p_i, p_j), d, d_1+d, ..., d_k+d: i, j <k\}$ is a diagram of a metric space. Recall that $d(p_i, p_j)$ are rational. Using Tarski’s elimination of quantifiers, we can computably find an equivalent quantifier-free formula with rational parameters. It follows that the property is decidable because equality and order are decidable for rational numbers.

Recall that $\mathbb {QU} = (p_i)_i$ , the rational Urysohn space, is dense in $\mathbb {U}$ . Since $\mathbb {QU}$ is dense in the Urysohn space, a basic open box of H (determined by the projection onto the first k coordinates) contains a tuple of legit reals if, and only if, it contains $d(p_j, p_i) - d(p_j, p_0)$ , where $p_j$ is sufficiently close to p, where $p \in \mathbb {U}$ are such that $d_i = d(p, p_i) - d(p, p_0)$ and $d = d(p, p_0)$ witness that the tuple is legit.

Since we can decide whether a basic open box is free of legit tuples, it follows that we can decide which basic open box contains no $(\gamma _i(p_j))_i$ for any j. Since the collection of such sequences U is dense in $cl(U)$ , and since basic open boxes are uniformly effectively open and form a basis of topology in H, we conclude that we can effectively enumerate the complement of $cl(U)$ .

We effectively identify $2^{\omega }$ with the ternary Cantor set $\mathcal {C}$ in $[0,1]$ (in the sense that we do not distinguish between these computably homeomorphic spaces; see also Theorem 3.33). This is where we get to use effective compactness (which is implied by Claim 4 and the effective compactness of the Hilbert cube). Using Theorem 3.40 and Proposition 3.29, fix a computable surjective $g:\mathcal {C} \rightarrow P$ , and let $g_i = \pi _i g$ , where $\pi _i$ is the ith projection in the cube. Define a computable $f_i$ to be equal to $g_i$ on the Cantor set, and to be linear otherwise (this standard technique was discussed in Section 4.1). We define a computable embedding of $\mathbb {U}$ into $C[0,1]$ by mapping $p_i$ into $f_i$ .

To show that the map $p_{n}\rightarrow f_{n}$ is isometric, first note that

$$ \begin{align*} d\left(p_{i},p_{k}\right)&= (d(p_k, p_i) - d(p_k, p_0)) - (d(p_k, p_k) - d(p_k, p_0))\\ &=\gamma_{i}\left(p_{k}\right)-\gamma_{k}\left(p_{k}\right)=f_{i}\left(t_{k}\right)-f_{k}\left(t_{k}\right), \end{align*} $$

where $t_k$ is any pre-image (under g) of the point in H corresponding to $p_k$ . It thus follows that

$$ \begin{align*} d\left(p_{i},p_{k}\right)\leq d_{sup}\left(f_{i},f_{k}\right). \end{align*} $$

On the other hand, for any $i,k\in \omega $ and any $t \in \mathcal {C}$ with $g(t) = \lim _j (\gamma _s(p_j))_s \in cl(U)$ , we have

$$ \begin{align*} f_{i}\left(t \right)-f_{k}\left(t \right)&= \pi_i (\lim_j (\gamma_s(p_j))_s ) - \pi_k (\lim_j (\gamma_s(p_j))_s )\\&= \lim _j \gamma_{i}\left(p_{j}\right)- \lim_j\gamma_{k}\left(p_{j}\right)=\lim_j (d\left(p_{j},p_{i}\right)-d\left(p_{j},p_{k}\right)). \end{align*} $$

By the triangle inequality we get $\left |d\left (p_{j},p_{i}\right )-d\left (p_{j},p_{k}\right )\right |\leq d\left (p_{i},p_{k}\right )$ for every j, and therefore

$$ \begin{align*} \left|f_{i}\left(t \right)-f_{k}\left(t \right)\right|\leq d\left(p_{i},p_{k}\right), \end{align*} $$

for any $t\in \mathcal {C}$ . By the definition of $f_{n}$ , any maximum difference must be attained on $\mathcal {C}$ . Thus

$$ \begin{align*} d_{sup}\left(f_{i},f_{k}\right)\leq d\left(p_{i},p_{k}\right). \end{align*} $$

Since the maps $p_i \rightarrow f_i$ are uniformly computable in i, it follows that the isometry defined above for $(p_i)_{i \in \omega }$ induces a computable isometric embedding $\mathbb {U} \rightarrow C[0,1]$ .

4.9. Covering dimension and embeddings into $\mathbb{R}^{n}$

Fix a compact Polish space M.

Definition 4.46. The covering dimension of M is the least $n \in \mathbb {N} \cup \{\infty \}$ such that every open cover of M has a refinement of order $n+1$ , i.e., each point belongs to at most $n+1$ sets.

We know that every compact space is homeomorphic to a subspace of the Hilbert cube $[0,1]^{\omega }$ , and we have seen that this also holds effectively. It is well-known that a compact space of covering dimension n can be homeomorphically embedded into $\mathbb {R}^{2n+1}$ (and indeed, into $[0,1]^{2n+1}$ ). Is this also computably true? One pleasant application of $\cap $ -decidable covers is the following theorem that answers the question in the affirmative:

Theorem 4.47. Let M be a computably compact Polish space of covering dimension n. Then there is a computable homeomorphic embedding of M into $\mathbb {R}^{2n+1}$ .

The proof is an improved version of a result of Melnikov and Harrison-Trainor [Reference Harrison-Trainor and Melnikov58] that states that every computably metrized compact Polish space of covering dimension n can be $0'$ -computably homeomorphically embedded into $\mathbb {R}^{2n+1}$ . The proof that we give below is more subtle and relies heavily on a classical argument from [Reference Pontryagin121] but with some modifications. It uses computability of nerves, so strictly speaking $**$ -computable compactness would be enough to run the proof.

Proof We say that a continuous $f:M \rightarrow \mathbb {R}^{2n+1}$ is an $\epsilon $ -homeomorphism if $f^{-1}(x)$ has diameter at most $\epsilon $ for every x in the range. We will need to prove a computable version of the following well-known fact:

Fact 4.48. The set of $\epsilon $ -homeomorphisms form a dense open set in $C[M,\mathbb {R}^{2n+1}]$ .

Let’s first explain how at least one $\epsilon $ -homomorphism can be found. The proof below is an adaptation of the argument that can be found in [Reference Pontryagin121] (see Theorems 4 and 5); however, our definition of an $\epsilon $ -homomorphism is a bit different.

Fix $\epsilon = 2^{-m}$ for some m. Construct a computable $\epsilon $ -homeomorphism of M to $\mathbb {R}^{2n+1}$ as follows. Use Theorem 3.16 and fix a strongly $\cap $ -decidable basis of computable balls K in M, recall that this means that the non-emptiness of intersection (of finite families) is decidable. (By Remark 3.18, we could alternatively use computable closed balls with the same centres and same radii.)

  1. (1) Find an open $\epsilon $ -cover $C_1, ..., C_k$ of M having order $n+1$ , where each $C_i$ is a finite union of open computable balls from K.

  2. (2) Compute the nerve N of $C_1, \ldots , C_k$ .

  3. (3) Find special points $c_1, ..., c_k$ in $\mathbb {R}^{2n+1}$ and a (geometrical) simplicial complex on vertices $c_1, ..., c_k$ isomorphic to N via a simplicial map which maps vertices to vertices.

  4. (4) Define $d_i(x)$ as follows. First, assume $C_i = \cup _{j \in J_i} B(k_{i,j}, r_{i, j})$ and set $d_{i,j}(x) = \sup \{ r_i - d(x,k_{i,j}), 0\}$ . (In Theorem 4 of [Reference Pontryagin121] Pontryagin uses the distance from x to the complement of $C_i$ .) Then define

    $$ \begin{align*}d_i(x) = \sup_{j \in J_i}d_i(x),\end{align*} $$
    let $u(x) = d_1(x) + \cdots +d_k(x)$ . Noting that u is strictly positive (because $C_1, \ldots , C_k$ cover the space), set $\theta _i(x) = d_i(x)/u(x) $ , and finally define
    $$ \begin{align*}f(x) = \sum_i \theta_i(x)c_i.\end{align*} $$

We will argue that f is an $\epsilon $ -homomorphism of M to $\mathbb {R}^{2n+1}$ with some additional properties. But first, we argue that the steps above can be performed computably. The first step is possible because some $\epsilon $ -cover $C^{\prime }_1, \ldots , C^{\prime }_r$ having order $n+1$ exists. By compactness, each $C^{\prime }_i$ can be replaced with a finite union $C_i$ of (closed or open) basic computable balls from K of radii at most $\epsilon $ and that are contained in $C^{\prime }_i$ , and so that together $C_1, \ldots , C_r$ cover the space. The new cover $C_1, \ldots , C_r$ has order at most the order of $C^{\prime }_1, \ldots , C^{\prime }_r$ because $C_i \subseteq C^{\prime }_i$ . We conclude that, in (1), such a cover exists among finite subsets of K. We can decide intersection for computable balls in K, and therefore we can also decide which finite families (representing $C_i$ ) intersect. The diameter of each $C_i$ can be easily computably estimated from above.Footnote 26 Together with $\cap $ -decidability of K this implies that, given $\epsilon = 2^{-m}$ , we can computably search for such an $\epsilon $ -cover satisfying $(1)$ . This also implies that the nerve formed in the second step is uniformly computable (as a finite object, i.e., is uniformly given by its strong index).

The third step is possible because in topology we prove that finite simplicial complexes are realizable in Euclidean spaces, this is done using points in a general position, and being in a general position is an open property.Footnote 27 If the (combinatorial) dimension of the simplex is n then this can be done in $\mathbb {R}^{2n+1}$ using points that are in general position, which is a c.e. property. See, e.g., Theorem 3 of [Reference Pontryagin121]. There is much freedom in the choice of points in general position, in particular, those can be found in any collection of open balls $V_1, \ldots , V_k$ in $\mathbb {R}^{2n+1}$ ; this is Theorem 2 of [Reference Pontryagin121]. Theorem 1 of [Reference Pontryagin121] also implies that $c_1, \ldots , c_k$ can be chosen special. Searching for a simplicial map is a finitistic task and can be done in finite time.

The third step uses elementary properties of computable functions to define a computable f.

The proof that f is an $\epsilon $ -homeomorphism is essentially literally the same as the proof of the analogous property of the $\epsilon $ -homeomorphism constructed in the proof of Theorem 4 of [Reference Pontryagin121], because our function satisfies the same properties (sufficient to prove that it is an $\epsilon $ -homeomorphism) as the function built in the proof of the aforementioned Theorem 4 of [Reference Pontryagin121]. More specifically, $\theta _i$ is continuous and has support $C_i$ , and also for every x we have that $\sum _i \theta _i(x) =1$ . For instance, it follows that a face in the nerve of the cover is mapped to the corresponding face in the geometric complex on $c_1,\ldots , c_k$ . We refer the reader to Theorem 4 of [Reference Pontryagin121] for further details.

It is rather important that in step (3) of the definition of f we only needed that $c_1, \ldots , c_k$ were in general position. By the aforementioned Theorem 2 of [Reference Pontryagin121], such points can be found in any collection of open neighbourhoods of $\mathbb {R}^{2n+1}$ . In particular, this is exploited in the proof of Theorem 5 of [Reference Pontryagin121] to show that the set of $\epsilon $ -homeomorphisms forms a dense open set in $C[M,\mathbb {R}^{2n+1}]$ . Although our definition of f is different from that in [Reference Pontryagin121], it shares all the properties needed from an $\epsilon $ -isomorphism in the proof of Theorem 5 of [Reference Pontryagin121]; in particular, all that is needed is that it maps a face of the nerve to the respective face of the geometric complex.

In other words, we have:

Fact 4.49. For every $g \in C[M,\mathbb {R}^{2n+1}]$ and every $m,k>0$ , there exists a computable $2^{-k}$ -homomorphism f such that

$$ \begin{align*}\sup_{x \in M} || f(x) - g(x)|| < 2^{-m}.\end{align*} $$

Such an f from the fact above will have a rather clear definition given by the construction described above, and for some specific choice of special points $c_1, \ldots , c_k$ .

We thus iterate this process. Given a $2^{-n}$ -homeomorphism $f_n$ , search for a $2^{-n-1}$ -homeomorphism $f_{n+1}$ (according to (1)–(4) above), such that $\sup _{x \in M} ||f_n(x) - f_{n+1}(x)||< 2^{-n}$ . The limit of the process exists and gives a computable injective continuous embedding of M into $\mathbb {R}^{2n+1}$ ; thus, it is a homeomorphic embedding (as injective continuous functions on compacta are homeomorphisms).

4.10. Probability spaces and Haar measure

For a computable compact space X, the space of all probability measures $\mathcal {P}(X)$ is a computably metrized space under the Wasserstein metric defined to be

$$ \begin{align*}d_w(\mu, \nu) = \sup |\int f d\mu - \int f d \nu|,\end{align*} $$

where the supremum is taken over all $1$ -Lipschitz functions upon X; that is, $|f(x) - f(y)| \leq d(x,y)$ for every $x,y \in X$ . The dense set is given by Dirac measures which are the probability measures concentrated at finitely many special points of X. We refer the reader to [Reference Hoyrup and Rojas63] for further background on computability of measure spaces. Gács [Reference Gács46] initiated a systematic investigation of the effective content of abstract probability and measure spaces in the context of algorithmic randomness.

Perhaps the first known construction of a surjective computable $\Phi :2^{\omega } \rightarrow \mathcal {P}(2^{\omega })$ can be found in Day and Miller [Reference Day and Miller33], but a very closely related argument can be found in the earlier paper [Reference Hoyrup and Rojas63]. Computable compactness of $\mathcal {P}(2^{\omega })$ was later used in [Reference Reimann and Slaman125]. Interestingly, this is a special case of Theorem 3.40 and the lemma below due to Marcone and Valenti [Reference Marcone and Valenti92]. We also note that in the special case of $\mathcal {P}(2^{\omega })$ the lemma essentially becomes a triviality; its two-line proof can be extracted from [Reference Day and Miller33].

Lemma 4.50 [Reference Marcone and Valenti92].

If X is computably compact then so is $\mathcal {P}(X)$ .

Proof To cover $\mathcal {P}(X)$ , take a finite $2^{-n}$ -cover of X and let $(x_i)$ be the finitely many centres of the open balls forming the cover. Say, there are N such balls. Take the finite collection of Dirac measures concentrated in the points $(x_i)$ and taking the values of the form $k\dfrac {2^{-n}}{N^2}$ , where $k \in \omega $ . There are only finitely many such measures, let D be the set of these measures. We claim that balls of radius $2^{-n+2}$ centred at these points cover the whole space.

Take any other Dirac measure $\mu $ concentrated at finitely many points $(y_j)$ . We can find, for each j, the least index $i = c(j)$ such that the ball centred at $x_i$ contains $y_j$ . For each i, let

$$ \begin{align*}C_i =\{y_j: c(j) =i\},\end{align*} $$

and note that $d(x_i, y_j)< 2^{-n}$ for every $y_j \in C_i$ . Define

$$ \begin{align*}\nu(x_i) = \sum_{j \in C_i} \mu(y_j),\end{align*} $$

and let $\rho \in D$ be a measure (from the fixed above finite set) that differs by at most $\dfrac {2^{-n}}{N}$ from $\nu $ at every $x_i$ . Fix any $1$ -Lipschitz function f and assume it takes value $0$ at $x_0$ (recall this means $|f(x) - f(y)| \leq d(x,y)$ ) and assume the diameter of the space X is $1$ , which makes the absolute value of f also bounded by $1$ . Then

$$ \begin{align*}\left|\int f d\nu - \int f d \rho\right|&= \left|\sum_{i <N} f(x_i) (\mu(x_i) - \rho(x_i))\right|\\ & \leq \left|\sum_{i <N} (\mu(x_i) - \rho(x_i)) \right| \leq N\dfrac{2^{-n}}{N} = 2^{-n}.\end{align*} $$

On the other hand,

$$ \begin{align*}\left|\int f d\mu - \int f d \nu\right| &= \left|\sum_{i<N} (\sum_{j \in C_i} f(y_j) \mu(y_j) - f(x_i) \nu(x_i))\right|\\& = \left|\sum_{i<N} \sum_{j \in C_i} (f(y_j) - f(x_i)) \mu(y_j)\right| ,\end{align*} $$

and noting that $d(x_i, y_j)< 2^{-n}$ for every $y_j \in C_i$ , this is bounded from above by $2^{-n} \sum _j \mu (y_j) = 2^{-n}$ . It follows that the distance between $\rho $ and $\mu $ is at most $2^{-n+1}$ . To finish the proof, recall that such Dirac measures are dense in the space, and the choice of $\mu $ was arbitrary.

A few years ago Jason Rute suggested the proof below in a personal communication with Melnikov and Nies. A proof sketch similar to the one that we give below can be found on the logic blog edited by Nies (see [Reference Nies112, Section 17]). Recently this result has been rediscovered in [Reference Pauly, Seon and Ziegler120] (see [Reference Pauly, Seon and Ziegler120] for a complete and detailed proof).

Theorem 4.51. For a compact computable group G, the Haar measure is computable iff G is computably compact.

Sketch.

Suppose G is computably compact. The property of being translation invariant is a $\Pi ^0_1$ property. So the Haar measure is contained in an effectively closed singleton of the computably compact (by Lemma 4.50) space $\mathcal {P}(G)$ . Therefore, the Haar measure is computable by Fact 3.25.

Now take a computable compact group G that has a computable Haar measure. We want to show it is computably compact. Replace $d(x,y)$ with the (integral) average of $d(gx,gy)$ , where the average is taken in the Haar measure as g varies across the group. This gives a computable G-invariant metric compatible with the original metric.

Now, to show that G is computably compact (in this new metric), it is enough for each rational k, to effectively find a finite set of points $a^k_0, ..., a^k_{n-1}$ for which every point in G is within distance $2^{-k}$ of one of these points. Fix k. Using our Haar measure find the measure of a ball of radius $2^{-(k+1)}$ . Call this measure $\delta $ . (Since the new distance is G-invariant, all balls of the same radius have the same measure.) Find a collection of balls $B_0, ..., B_{n-1}$ with radius $2^{-(k+1)}$ whose union $C = B_0 \cup \cdots \cup B_{n-1}$ has measure $> 1 - \delta $ ; recall that the measure is left-c.e. Now, consider any point x not in this union C. It has to be at distance $< 2^{-(k+1)}$ from the union. Otherwise, there would be a ball centred at x with radius $2^{-(k+1)}$ , and hence having measure $\delta $ , which is disjoint from the union C. But the union C has measure $> 1 - \delta $ , so this cannot happen. Therefore all points of G are within distance $2^{-k}$ of the centres of $B_0, ..., B_{n-1}$ . This algorithm shows that the space is computably compact in the new metric. To show it is computably compact in the original metric, for any finite list of rational balls in original metric, convert it to a list of balls in the new metric. Now, if this list of balls covers the space G, by computable compactness, we will eventually find this out.

It follows from Theorem 4.35 that a profinite group admits a recursive presentation iff it has a computably metrization with computable Haar measure iff it admits a computably compact presentation. (In the latter two cases we need to also assume the operations are computable.) It was established in [Reference Melnikov95] that recursive profinite groups are exactly the Pontryagin duals of computable torsion groups, and it is not difficult to construct an example of a procyclic, computably metrized group whose dual has no computable copy [Reference Melnikov95]. (A similar result has recently been established in [Reference Pauly, Seon and Ziegler120].) In the connected case, one of the proofs of Theorem 4.40 actually builds a computably metrized group with computable operations whose space is not homeomorphic to any computably compact space. We summarise this below:

Corollary 4.52 [Reference Lupini, Melnikov and Nies91, Reference Melnikov95].

In the classes of connected compact abelian and profinite abelian groups there exist examples of computably metrizable groups no computable metrization of which can compute Haar measure.

4.11. Some further open questions

In Section 4.4 we explained why the characterisation problem and the isometric isomorphism problem for compact sets are arithmetical, and also why the homeomorphism problem for compact Polish spaces is $\Sigma ^1_1$ -complete. Similar results for compact Polish groups can be found in [Reference Melnikov95]. The following related questions are left open:

Question 4.53.

  1. (1) (Melnikov and Harrison-TrainorFootnote 28 ) What is the complexity of the isomorphism problem for (not necessarily compact) Polish spaces? (Is the naive upper bound optimal?)

  2. (2) (Melnikov and Harrison-Trainor) What is the complexity of the characterisation problem $\{i: M_i \cong _{hom} S^3\}$ for the 3-sphere $S^3$ ? What about the 2-ball? More generally, is it true that the (topological) characterisation problem $\{i: M_i \cong _{hom} S\}$ for any compact manifold S is arithmetical?

It is known that the characterisation problem or every compact $2$ -surface (including the $2$ -sphere, obviously) is arithmetical [Reference Harrison-Trainor and Melnikov58]. They key step in their proof produces an arithmetical atlas of a given computable surface.

Question 4.54 (Melnikov and Harrison-Trainor [Reference Harrison-Trainor and Melnikov58]).

Suppose S is a computably compact manifold. Does S admit an arithmetical atlas?

We have already mentioned above that the index set approach has not yet been applied to the effective enumeration of all (partial) computably compact spaces. This seems reasonable assuming the thesis of the article (that computable compactness is a natural approach to computability in the compact case). Also, there are not many arithmetical completeness index set results in the literature (some can be found in [Reference Melnikov95]). The approach via computable compactness seems rather natural for such potential completeness results in the compact case (cf. Remark 4.31).

Question 4.55.

  1. (1) Develop the index set approach to classification using the enumeration of all (partial) computably compact spaces.

  2. (2) Prove completeness results for the arithmetical index set estimates stated above and also for other results that can be found in, e.g., [Reference Downey and Melnikov38, Reference Harrison-Trainor and Melnikov58, Reference Lupini, Melnikov and Nies91].

In Section 4.4 we also explained how to construct a compact computable Polish space not homeomorphic to any computably compact space; this is Theorem 4.40. We also conjectured that a $0"'$ proof can be used to replace algebraic topology, but this approach is by no means elementary (if it works). It is rather natural to ask whether there is a less involved proof of Theorem 4.40. The question below is, of course, loosely stated.

Question 4.56. Find an elementary (elegant?) proof of Theorem 4.40.

In Section 4.3 we discussed an application of computable compactness to constructing basic sequences in computable Banach spaces. Bosserhoff [Reference Bosserhoff13] constructed a computable Banach space with a Schauder basis and no computable Schauder basis, and Downey, Long, and Greenberg [Reference Long90] showed that the index set of computable Banach spaces with computable bases is $\Sigma _3^0$ complete. Using the characterisation of Schauder bases together with computable compactness, it is possible to show [Reference Long90] that having a basis is a $\Sigma _1^1$ property. The following question seems rather challenging.

Question 4.57. Is the complexity of the index set $\{i\mid W_i \mbox { is a computable} \mbox{Banach space with a Schauder basis}\} \ \Sigma _1^1$ complete?

There are many interesting open questions in the area of computable Banach spaces (see, e.g., [Reference Long90]). It is highly plausible that computable compactness can be used to attack some of these questions.

Algebraic topology has played a considerable role in many proofs throughout the paper. We believe that there is much more to be said about the algorithmic content of algebraic topology, so we state:

Problem 4.58. Develop a general theory of computable algebraic topology and computable homological algebra.

Classically, the class of locally compact spaces is perhaps the narrowest natural class that contains both compact and discrete spaces. There have been many attempts to define effective local compactness in the literature (e.g., [Reference Pauly119]). Nonetheless, it seems that there is no commonly accepted and robust notion that would be considered “standard.”

Problem 4.59. Suggest a robust (and useful) notion of effectively locally compact Polish space.

We of course do not exclude the possibility that some of the known definitions will already be good enough, but certainly we need to accumulate more results to draw any conclusions.

Our last problem is concerned with primitive recursive analysis. Historically a lot of elementary computable analysis was in fact developed primitively recursively (see, e.g., book [Reference Goodstein52]). However, gradually, primitive recursiveness was abandoned, perhaps because of technical difficulties that arise while dealing with primitive recursive procedures. Beginning with the 1980s pretty much all computable analysis has been done using general Turing computability (see [Reference Pour-El and Richards124, Reference Weihrauch146]). On the other hand, there has been an increasing interest in polynomial-time analysis of continuous functions (see book [Reference Ko81]). Recently in [Reference Downey, Melnikov and Ng39, Reference Selivanov and Selivanova131, Reference Selivanov and Selivanova132], it has been proposed to revive primitive recursive analysis using modern methods; this program could potentially serve as a link between abstract computable analysis and the more practical polynomial time and computational analysis.

For instance, say that a Polish space is punctual is the distances between special points are uniformly primitive recursive nonzero reals (to avoid dealing with equality). Some recent results about punctual spaces can be found in [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5]. The role of compactness in primitive recursive analysis is very poorly understood. For example, using computable compactness of $[0,1]$ , it is easy to show that every computable continuous function on $[0,1]$ is effectively uniformly continuous, i.e., has a computable modulus of uniform continuity. The last section of [Reference Downey, Melnikov and Ng39] outlines a primitive recursive version of this elementary fact. The proof also uses compactness, but it uses it rather differently from the usual proof. On the other hand, one of the main results in [Reference Bagaviev, Batyrshin, Bazhenov, Bushtets, Dorzhieva, Kornev, Melnikov, Ng and Koh5] relies on the standard computable compactness (in the sense of this paper) to establish a primitive recursive result. So perhaps more insight is needed to attack the following:

Problem 4.60. Give a robust (and useful) definition of a punctually compact space.

We suspect that there are several potentially useful definitions of a punctually compact space that are not equivalent. For instance, we would like to know whether the results discussed in this paper, especially Theorem 1.1, hold primitively recursively.

Acknowledgments

We thank our colleagues Arno Pauly, Victor Selivanov, and Andre Nies for providing us with many useful references. We also thank the two anonymous referees for many useful suggestions, comments, and further references.

Funding

Downey was partially supported by the Marsden Fund of New Zealand. Melnikov was supported by the Rutherford Discovery Fellowship (Wellington) RDF-MAU1905, Royal Society Te Aparangi.

Footnotes

1 There are various notions in the literature which do not assume the metric to be complete. For more details about these closely related notions of effective presentability, such as “recursive” and “computable” metric spaces, we cite [Reference Gregoriades, Kispéter and Pauly54, Reference Weihrauch147]. We note that the aforementioned two notions of “recursive” and “computable” spaces are equivalent up to scaling the metric by a computable real [Reference Gregoriades, Kispéter and Pauly54].

2 As of 2022, the survey is still available at the personal home page of Jason Rute.

3 While it is not central to this paper, $\Omega $ is the Lebesgue measure of the domain of a universal prefix-free Turing machine (see [Reference Downey and Hirschfeldt36]). It is a “natural” example of a left-c.e. real which is not computable, in the same way that the halting problem is a natural example of a c.e. non-computable set.

4 Such $\Pi ^0_1$ classes (with Ext $(T)$ computable) have been given several names historically: recursive, recursively closed, and decidable. See, e.g., [Reference Downey35, Reference La Roche127].

5 As was noted by one of the referees, it is not clear whether this observation holds in the absence of the metric. Specifically, it is not known whether $X^\omega $ is computably compact for an arbitrary computably compact represented space. For more about effective compactness in general represented spaces, we cite [Reference Pauly117].

6 In general, we should also include the moduli of uniform convergence into the definition of our formulae, but in the language of just pure metric this is not needed. Since M is compact, and indeed will be computably compact, we can potentially make the moduli implicit even in more general signatures.

7 Every point in $M \setminus B_i^c$ has the property $d(cntr(B_i), y)> r(B_i) =r$ , and if we take $B(y, q)$ where $0< q <\frac {d(cntr(B_i), y)- r(B_i)}{2}$ then $d(cntr(B_i), y)> r+q.$

8 Each such intersection is witnessed by a (special) point which must be at distance strictly less than $2\epsilon $ to all centres, say, $\gamma $ -less. If we shrink the radii by a value less than the minimum of these $\gamma $ (which is a positive value since there are only finitely many $B_i$ involved) then the inequalities will still hold. Another way to think about it is as follows: $B \cap D \neq \emptyset $ is an “open property” of the parameters (radii and centres), and a finite conjunction of open properties is also open because open sets are closed under taking finite intersections.

9 The radii can likely be made rational if necessary, but they will be represented via Cauchy sequences, not as a fraction.

10 As has been pointed out by one of the referees, this seemingly obvious and tame fact is indeed rather useful in many applications of effective compactness. We will discuss some of these applications in due course.

11 Note that $y_j$ does not have to be special in M, and thus basic open balls in C do not have to be basic open in M. Nonetheless, an open ball of M centred in a computable point y and having a computable (more generally, left-c.e.) radius r is effectively open:

$$ \begin{align*}B(y,r) = \bigcup \{B(x, q): d(x,y)+q< r\},\end{align*} $$

that is, $B(y,r) $ is the union of basic open balls formally contained in it. Note that effective openness of $B(y, r)$ is uniform in y and r.

12 This is because $d(x,y) +r_2 <r_1$ and $d(y,z) +r_3 <r_2$ (together with the triangle inequality) imply $d(x,z) +r_3 <r_1$ .

13 Issues of this sort are investigated in detail in [Reference Pauly119].

14 To see why, let c be the centre of $D^c$ and r its radius, and assume $d(c,x) = r+\delta $ . There must be a special $x_i$ such that $d(x_i, x)< \delta /2$ . Take the basic open ball $C = B(x_i, \delta /2)$ . Then the distance between their centres is $d(c, \alpha )> r +\delta -d(x_i, x) > r +\delta -\delta /2= r+ \delta /2$ , which is the sum of their radii. So the balls are formally disjoint.

15 For every open Z in X, its complement is closed and thus is compact. Since the continuous image of a compact set is compact and therefore closed, $f (X \setminus Z)$ is closed. Since f is a bijection, $f(X \setminus Z) = f(X) \setminus f(Z) = Y \setminus f(Z)$ , which makes $f(Z)$ open.

16 If it is $>1$ , then replace the metric with the new metric $\dfrac {1}{n}d(\cdot , \cdot )$ , where n is a large enough positive integer. You can also redefine the metric to be equal to one on a pair x and y if the original distance between x and y is greater than $1$ . The latter method is computably uniform and gives a metric computably compatible with the original one, i.e., the identity map is a computable homeomorphism between the old metrized space and the newly metrized one.

17 Every point in $K \setminus P$ is contained in a basic ball formally disjoint from some finite cover of P by basic open balls. If we take the collection of all such balls around all such $x \in K \setminus P$ of radius at most $\epsilon $ , then, together with any (finite) cover of P, they must cover the whole space K. Thus, there is a finite subcover in which we can keep all the finitely many $\epsilon $ -balls that cover P and intersect P. By our assumption, K is computably compact/computable closed, and thus all these conditions are c.e.; we just wait until such a finite $\epsilon $ -cover of K is found.

18 More formally, $Iso( X, Y)$ admits a natural representation as a $\Pi ^0_1$ class $[B]$ in the sense that there is a Turing functional turning infinite paths through B into isometries from X to Y, and so that every member $Iso( X, Y)$ has a code in $[B]$ .

19 As was pointed out by one of the referees, one of the many convenient features of computable compactness is that in certain scenarios quantification over a computably compact set can be treated as computably bounded search. For instance, c.e. openness (or being $\Pi ^0_1$ ) is typically preserved under such quantification.

20 Specifically, those with “monotone” or “shrinking” bases.

21 Meaning that each ball from the open cover of $C_{i+1}$ is formally included into some basic open ball in the fixed cover of $C_{i}$ . Similar for condition $(4)$ below.

22 Just take the radii of open balls much smaller than the pairwise distances between the finitely many clopen sets to see that it can be done. It is crucial here that the sets are clopen (see, e.g., Corollary 4.3 for a potential issue in general).

23 We are not really interested in the case when $i=0$ when $d_{-1}$ is not really defined; just assume $Im (d_{-1}) =\{0\}$ .

24 A solenoid (space) is a compact connected topological space which the inverse limit of a system $(S_i,f_i)$ with $f_i:S_{i+1}\to S_i$ , where each $S_i$ is a circle and $f_i$ is the map that uniformly wraps $S_{i+1} \ n_i\ge 2$ times around $S_i$ . These constructions are important in the area of hyperbolic dynamical systems.

25 Classically, classification of manifolds works via triangulations.

26 This can be done using, e.g., the distances between the centres and the radii. Alternatively, replace all computable balls in $C_i$ with the respective closed balls that are computable closed sets by Proposition 3.30. Then use that the union of finitely many computable closed sets is computable, and that the diameter is a supremum of a computable function defined on the computably compact space (see Proposition 3.5). This gives an arbitrary tight upper estimate on the diameter of $C_i$ , with all possible uniformity.

27 Points $c_1,\ldots , c_k \in \mathbb {R}^d$ are in general position if any subset of at most d-many points of $\{c_1,\ldots , c_k\}$ is linearly independent.

28 This question and question (2) below have been posed in [Reference Harrison-Trainor and Melnikov58] in a slightly different form.

References

Aberth, O., Computable Analysis , McGraw-Hill, New York, 1980.Google Scholar
Alexandroff, P., Untersuchungen über gestalt und Lage Abgeschlossener Mengen Beliebiger dimension . Annals of Mathematics. Second Series , vol. 30 (1928/29), nos. 1–4, pp. 101187.CrossRefGoogle Scholar
Ash, C. and Knight, J., Computable Structures and the Hyperarithmetical Hierarchy , Studies in Logic and the Foundations of Mathematics, vol. 144, North-Holland, Amsterdam, 2000.Google Scholar
Avigad, J. and Brattka, V., Computability and analysis: The legacy of Alan Turing , Turing’s Legacy: Developments from Turing’s Ideas in Logic (R. Downey, editor), Lecture Notes in Logic, vol. 42, Association for Symbolic Logic, La Jolla, 2014, pp. 147.Google Scholar
Bagaviev, R., Batyrshin, I., Bazhenov, N., Bushtets, D., Dorzhieva, M., Kornev, R., Melnikov, A., Ng, K. M., and Koh, H. T., Computably and punctually universal spaces, preprint, 2021.Google Scholar
Barrett, J., Downey, R., and Greenberg, N., Cousin’s lemma in second-order arithmetic. Proceedings of the American Mathematical Society Series B , vol. 9 (2022), pp. 111124.Google Scholar
Bazhenov, N., Downey, R., Kalimullin, I., and Melnikov, A., Foundations of online structure theory, this Journal, vol. 25 (2019), no. 2, pp. 141181.Google Scholar
Bazhenov, N., Harrison-Trainor, M., and Melnikov, A., Computable Stone spaces, preprint, 2021, arXiv:2107.01536.Google Scholar
Ben Yaacov, I., Berenstein, A., Henson, C. W., and Usvyatsov, A., Model theory for metric structures , Model Theory with Applications to Algebra and Analysis , vol. 2 (Z. Chatzidakis, D. Macpherson, A. Pillay, and A. Wilkie, editors), London Mathematical Society Lecture Note series, vol. 350, Cambridge University Press, Cambridge, 2008, pp. 315427.CrossRefGoogle Scholar
Ben Yaacov, I. and Pedersen, A. P., A proof of completeness for continuous first-order logic . Journal of Symbolic Logic , vol. 75 (2010), no. 1, pp. 168190.CrossRefGoogle Scholar
Bishop, E., Foundations of Constructive Analysis , McGraw-Hill, New York, 1967.Google Scholar
Borel, E., Le calcul des intégrales définies . Journal de Mathématiques Pures et Appliquées , vol. 8 (1912), pp. 159210.Google Scholar
Bosserhoff, V., On the effective existence of Schauder bases . Journal of Universal Computer Science , vol. 15 (2009), no. 6, pp. 11451161.Google Scholar
Bosserhoff, V. and Hertling, P., Effective subsets under homeomorphisms of ${\mathbb{R}}^n$ . Information and Computation , vol. 245 (2015), pp. 197212.CrossRefGoogle Scholar
Brattka, V., Computability of Banach Space Principles , FernUniversität Hagen, Fachbereich Informatik, Hagen, 2001.Google Scholar
Brattka, V., Borel complexity and computability of the Hahn–Banach theorem . Archive for Mathematical Logic , vol. 46 (2008), nos. 7–8, pp. 547564.CrossRefGoogle Scholar
Brattka, V., Plottable real number functions and the computable graph theorem . SIAM Journal on Computing , vol. 38 (2008), no. 1, pp. 303328.CrossRefGoogle Scholar
Brattka, V. and Dillhage, R.. Computability of compact operators on computable Banach spaces with bases . Mathematical Logic Quarterly , vol. 53 (2007), nos. 4–5, pp. 345364.CrossRefGoogle Scholar
Brattka, V. and Presser, G., Computability on subsets of metric spaces . Theoretical Computer Science , vol. 305 (2003), nos. 1–3, pp. 4376.CrossRefGoogle Scholar
Brattka, V., de Brecht, M., and Pauly, A., Closed choice and a uniform low basis theorem . Annals of Pure and Applied Logic , vol. 163 (2012), no. 8, pp. 9861008.CrossRefGoogle Scholar
Brattka, V., Le Roux, S., Miller, J. S., and Pauly, A., Connected choice and the Brouwer fixed point theorem . Journal of Mathematical Logic , vol. 19 (2019), no. 1, 1950004, 46 pp.CrossRefGoogle Scholar
Braverman, M. and Yampolsky, M., Computability of Julia Sets , Algorithms and Computation in Mathematics, vol. 23, Springer, Berlin, 2009.Google Scholar
de Brecht, M., Pauly, A., and Schröder, M., Overt choice . Computability , vol. 9 (2020), nos. 3–4, pp. 169191.CrossRefGoogle Scholar
Burnik, K. and Iljazović, Z., Computability of 1-manifolds . Logical Methods in Computer Science , vol. 10 (2014), no. 2:8, pp. 128.Google Scholar
Camrud, C., Goldbring, I., and McNicholl, T. H., On the complexity of the theory of a computably presented metric structure. Archive for Mathematical Logic , to appear, preprint, 2021, arXiv:2106.05372.Google Scholar
Carothers, N. L., A Short Course on Banach Space Theory , London Mathematical Society Student Texts, vol. 64, Cambridge University Press, Cambridge, 2005.Google Scholar
Ceitin, G. S., Algorithmic operators in constructive complete separable metric spaces . Doklady Akademii Nauk SSSR , vol. 128 (1959), pp. 4952.Google Scholar
Čelar, M. and Iljazović, Z., Computability of products of chainable continua . Theory of Computing Systems , vol. 65 (2021), no. 2, pp. 410427.CrossRefGoogle Scholar
Cenzer, D., ${\varPi}_1^0$ classes in computability theory , Handbook of Computability Theory (E. R. Griffor, editor), Studies in Logic and the Foundations of Mathematics, vol. 140, North-Holland, Amsterdam, 1999, pp. 3785.CrossRefGoogle Scholar
Cenzer, D. and Remmel, J. B., ${\varPi}_1^0$ classes in mathematics , Handbook of Recursive Mathematics , vol. 2 (Y. L. Ershov, S. S. Goncharov, A. Nerode, J. B. Remmel, and V. W. Marek, editors), Studies in Logic and the Foundations of Mathematics, vol. 139, North-Holland, Amsterdam, 1998, pages 623821.Google Scholar
Cholak, P., Coles, R., Downey, R., and Herrmann, E., Automorphisms of the lattice of ${\varPi}_1^0$ classes: Perfect thin classes and ANC degrees . Transactions of the American Mathematical Society , vol. 353 (2001), no. 12, pp. 48994924.Google Scholar
Couch, P. J., Daniel, B. D., and McNicholl, T. H., Computing space-filling curves . Theory of Computing Systems , vol. 50 (2012), no. 2, pp. 370386.CrossRefGoogle Scholar
Day, A. R. and Miller, J. S., Randomness for non-computable measures . Transactions of the American Mathematical Society , vol. 365 (2013), no. 7, pp. 35753591.CrossRefGoogle Scholar
Diamondstone, D. E., Dzhafarov, D. D., and Soare, R. I., ${\varPi}_1^0$ classes, Peano arithmetic, randomness, and computable domination . Notre Dame Journal of Formal Logic , vol. 51 (2010), no. 1, pp. 127159.CrossRefGoogle Scholar
Downey, R. G., Abstract dependence, recursion theory, and the lattice of recursively enumerable filters . Bulletin of the Australian Mathematical Society , vol. 27 (1983), no. 3, pp. 461464.CrossRefGoogle Scholar
Downey, R. and Hirschfeldt, D., Algorithmic Randomness and Complexity , Theory and Applications of Computability, Springer, New York, 2010.CrossRefGoogle Scholar
Downey, R. and Jockusch, C. G., Every low Boolean algebra is isomorphic to a recursive one . Proceedings of the American Mathematical Society , vol. 122 (1994), no. 3, pp. 871880.CrossRefGoogle Scholar
Downey, R. G. and Melnikov, A. G., Computable analysis and classification problems , Beyond the Horizon of Computability—16th Conference on Computability in Europe (M. Anselmo, G. D. Vedova, F. Manea, and A. Pauly, editors), Lecture Notes in Computer Science, vol. 12098, Springer, Cham, 2020, pp. 100111.CrossRefGoogle Scholar
Downey, R., Melnikov, A., and Ng, K. M., Foundations of online structure theory II: The operator approach . Logical Methods in Computer Science , vol. 17 (2021), no. 3, Paper no. 6, 35 pp.Google Scholar
Enflo, P., A counterexample to the approximation problem in Banach spaces . Acta Mathematica , vol. 130 (1973), pp. 309317.CrossRefGoogle Scholar
Ershov, Y. and Goncharov, S., Constructive Models , Siberian School of Algebra and Logic, Consultants Bureau, New York, 2000.CrossRefGoogle Scholar
Feiner, L., Hiearchies of Boolean algebras . Journal of Symbolic Logic , vol. 35 (1970), no. 3, pp. 365374.CrossRefGoogle Scholar
Franklin, J. N. Y. and McNicholl, T. H., Degrees of and lowness for isometric isomorphism . Journal of Logic and Analysis , vol. 12 (2020), Paper no. 6, 23 pp.CrossRefGoogle Scholar
Franklin, J. N. Y. and Turetsky, D., Taking the path computably traveled . Journal of Logic and Computation , vol. 29 (2019), no. 6, pp. 969973.CrossRefGoogle Scholar
Fuchs, L., Infinite Abelian Groups. Volume I , Pure and Applied Mathematics, vol. 36, Academic Press, New York, 1970.Google Scholar
Gács, P., Uniform test of algorithmic randomness over a general space . Theoretical Computer Science , vol. 341 (2005), nos. 1–3, pp. 91137.CrossRefGoogle Scholar
Gao, S., Invariant Descriptive Set Theory , Pure and Applied Mathematics, vol. 293, CRC Press, Boca Raton, 2009.Google Scholar
Gavruskin, A. and Nies, A., Universality for left-computably enumerable metric spaces . Lobachevskii Journal of Mathematics , vol. 35 (2014), no. 4, pp. 292294.CrossRefGoogle Scholar
Gherardi, G. and Marcone, A., How incomputable is the separable Hahn–Banach theorem? Notre Dame Journal of Formal Logic , vol. 50 (2010), no. 4, pp. 393425.Google Scholar
Goncharov, S., Countable Boolean Algebras and Decidability , Siberian School of Algebra and Logic, Consultants Bureau, New York, 1997.Google Scholar
Goncharov, S. and Knight, J., Computable structure and antistructure theorems . Algebra Logika , vol. 41 (2002), no. 6, pp. 639681, 757.Google Scholar
Goodstein, R., Recursive Analysis , Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1961.Google Scholar
Greenberg, N., Melnikov, A. G., Knight, J. F., and Turetsky, D., Uniform procedures in uncountable structures . Journal of Symbolic Logic , vol. 83 (2018), no. 2, pp. 529550.CrossRefGoogle Scholar
Gregoriades, V., Kispéter, T., and Pauly, A., A comparison of concepts from computable analysis and effective descriptive set theory . Mathematical Structures in Computer Science , vol. 27 (2017), no. 8, pp. 14141436.CrossRefGoogle Scholar
Grzegorczyk, A., Computable functionals . Fundamenta Mathematicae , vol. 42 (1955), pp. 168202.CrossRefGoogle Scholar
Grzegorczyk, A., On the definition of computable functionals . Fundamenta Mathematicae , vol. 42 (1955), pp. 232239.CrossRefGoogle Scholar
Grzegorczyk, A., On the definitions of computable real continuous functions . Fundamenta Mathematicae , vol. 44 (1957), pp. 6171.CrossRefGoogle Scholar
Harrison-Trainor, M. and Melnikov, A., An arithmetic analysis of closed surfaces. Transactions of the American Mathematical Society , to appear, https://doi.org/10.1090/tran/8915.CrossRefGoogle Scholar
Harrison-Trainor, M., Melnikov, A., and Ng, K. M., Computability of polish spaces up to homeomorphism . Journal of Symbolic Logic , vol. 85 (2020), pp. 16641686.CrossRefGoogle Scholar
Hewitt, E., The role of compactness in analysis . American Mathematical Monthly , vol. 67 (1960), no. 6, pp. 499516.Google Scholar
Hofmann, K. H. and Morris, S. A., The Structure of Compact Groups , De Gruyter Studies in Mathematics, vol. 25, De Gruyter, Berlin, 1998.Google Scholar
Hoyrup, M., Kihara, T., and Selivanov, V., Degree spectra of homeomorphism types of Polish spaces, preprint, 2020, arXiv:2004.06872.CrossRefGoogle Scholar
Hoyrup, M. and Rojas, C., Computability of probability measures and Martin–Löf randomness over metric spaces . Information and Computation , vol. 207 (2009), no. 7, pp. 830847.CrossRefGoogle Scholar
Iljazović, Z., Chainable and circularly chainable co-r.e. sets in computable metric spaces . Journal of Universal Computer Science , vol. 15 (2009), no. 6, pp. 12061235.Google Scholar
Iljazović, Z., Isometries and computability structures . Journal of Universal Computer Science , vol. 16 (2010), no. 18, pp. 25692596.Google Scholar
Iljazović, Z., Compact manifolds with computable boundaries . Logical Methods in Computer Science , vol. 9 (2013), 4, 4:19, 22 pp.Google Scholar
Iljazović, Z. and Kihara, T., Computability of subsets of metric spaces , Handbook of Computability and Complexity in Analysis (V. Brattka and P. Hertling, editors), Theory and Applications of Computability, Springer, Cham, 2021, pp. 2969.CrossRefGoogle Scholar
Iljazović, Z. and Sušić, I., Semicomputable manifolds in computable topological spaces . Journal of Complexity , vol. 45 (2018), pp. 83114.CrossRefGoogle Scholar
Iljazović, Z. and Validžić, L., Effective compactness and orbits of points under the isometry group . Annals of Pure and Applied Logic , vol. 174 (2023), no. 2, Paper no. 103198.CrossRefGoogle Scholar
Jockusch, C. G. Jr. and Soare, R. I., A minimal pair of ${\varPi}_1^0$ classes. Journal of Symbolic Logic, vol. 36 (1971), pp. 6678.CrossRefGoogle Scholar
Jockusch, C. G. Jr. and Soare, R. I., Degrees of members of ${\varPi}_1^0$ classes. Pacific Journal of Mathematics, vol. 40 (1972), pp. 605616.CrossRefGoogle Scholar
Jockusch, C. G. Jr. and Soare, R. I., ${\varPi}_1^0$ classes and degrees of theories . Transactions of the American Mathematical Society , vol. 173 (1972), pp. 3356.Google Scholar
Kalantari, I. and Weitkamp, G., Effective topological spaces. I. A definability theory . Annals of Pure and Applied Logic , vol. 29 (1985), no. 1, pp. 127.CrossRefGoogle Scholar
Kalantari, I. and Weitkamp, G., Effective topological spaces. II. A hierarchy . Annals of Pure and Applied Logic , vol. 29 (1985), no. 2, pp. 207224.CrossRefGoogle Scholar
Kalantari, I. and Weitkamp, G., Effective topological spaces. III. Forcing and definability . Annals of Pure and Applied Logic , vol. 36 (1987), no. 1, pp. 1727.CrossRefGoogle Scholar
Kalantari, I. and Welch, L., On Turing degrees of points in computable topology . Mathematical Logic Quarterly , vol. 54 (2008), no. 5, pp. 470482.CrossRefGoogle Scholar
Kamo, H., Computability in some fundamental theorems in functional analysis and general topology , Ph.D. thesis, Kyoto University, 2006.Google Scholar
Khisamiev, N., Hierarchies of torsion-free abelian groups . Algebra Logika , vol. 25 (1986), no. 2, pp. 205226, 244.CrossRefGoogle Scholar
Kleene, S. C., A note on computable functionals . Nederlandse Akademie van Wetenschappen. Proceedings. Series A , vol. 18 (1956), pp. 275280.Google Scholar
Knight, J. F. and Stob, M., Computable Boolean algebras . Journal of Symbolic Logic , vol. 65 (2000), no. 4, pp. 16051623.CrossRefGoogle Scholar
Ko, K.-I., Complexity Theory of Real Functions , Progress in Theoretical Computer Science, Birkhäuser, Boston, 1991.CrossRefGoogle Scholar
Ko, K.-I. and Friedman, H., Computational complexity of real functions . Theoretical Computer Science , vol. 20 (1982), no. 3, pp. 323352.CrossRefGoogle Scholar
Korovina, M. and Kudinov, O., Towards computability over effectively enumerable topological spaces , Proceedings of the Fifth International Conference on Computability and Complexity in Analysis (V. Brattka, R. Dillhage, T. Grubba, and A. Klutsch, editors), Electronic Notes in Theoretical Computer Science, vol. 221, Elsevier, Amsterdam, 2008, pp. 115125.Google Scholar
Korovina, M. and Kudinov, O., The Rice–Shapiro theorem in computable topology . Logical Methods in Computer Science , vol. 13 (2017), no. 4, Paper no. 30, 13 pp.Google Scholar
Korovina, M. and Kudinov, O., Highlights of the Rice–Shapiro theorem in computable topology , Perspectives of System Informatics (A. Pnueli, I. Virbitskaite, and A. Voronkov, editors), Lecture Notes in Computer Science, vol. 10742, Springer, Cham, 2018, pp. 241255.CrossRefGoogle Scholar
Kreisel, G., A variant to Hilbert’s theory of the foundations of arithmetic . British Journal for the Philosophy of Science , vol. 4 (1953), pp. 107129; errata and corrigenda, vol. 357 (1954).CrossRefGoogle Scholar
Kudinov, O. and Selivanov, V., First order theories of some lattices of open sets . Logical Methods in Computer Science , vol. 13 (2017), no. 3, Paper no. 16, 18 pp.Google Scholar
Lacombe, D., Quelques procédés de définition en topologie recursive , Constructivity in Mathematics: Proceedings of the Colloquium Held at Amsterdam, 1957 (A. Heyting, editor), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1959, pp. 129158.Google Scholar
Lešnik, D., Constructive Urysohn universal metric space . Journal of Universal Computer Science , vol. 15 (2009), no. 6, pp. 12361263.Google Scholar
Long, Q., Computability-theoretic complexity of effective Banach spaces , M.Sc. thesis, Victoria University of Wellington, 2021.Google Scholar
Lupini, M., Melnikov, A., and Nies, A., Computable topological abelian groups . Journal of Algebra , vol. 615 (2023), pp. 278327.CrossRefGoogle Scholar
Marcone, A. and Valenti, M., Effective aspects of Hausdorff and Fourier dimension . Computability , vol. 11 (2022), nos. 3–4, pp. 299333.CrossRefGoogle Scholar
Melnikov, A., Enumerations and completely decomposable torsion-free abelian groups . Theory of Computing Systems , vol. 45 (2009), no. 4, pp. 897916.CrossRefGoogle Scholar
Melnikov, A. G., Computably isometric spaces . Journal of Symbolic Logic , vol. 78 (2013), no. 4, pp. 10551085.CrossRefGoogle Scholar
Melnikov, A., Computable topological groups and Pontryagin duality . Transactions of the American Mathematical Society , vol. 370 (2018), no. 12, pp. 87098737.CrossRefGoogle Scholar
Melnikov, A., New degree spectra of polish spaces . Rossiyskaya Akademiya Nauk , vol. 62 (2021), no. 5, pp. 10911108.Google Scholar
Melnikov, A. and Montalbán, A., Computable polish group actions . Journal of Symbolic Logic , vol. 83 (2018), no. 2, pp. 443460.CrossRefGoogle Scholar
Melnikov, A. G. and Ng, K. M., Computable structures and operations on the space of continuous functions . Fundamenta Mathematicae , vol. 233 (2016), no. 2, pp. 101141.Google Scholar
Melnikov, A. G. and Nies, A., The classification problem for compact computable metric spaces , The Nature of Computation (P. Bonizzoni, V. Brattka, and B. Löwe, editors), Lecture Notes in Computer Science, vol. 7921, Springer, Heidelberg, 2013, pp. 320328.Google Scholar
Metakides, G. and Nerode, A., Recursively enumerable vector spaces . Annals of Mathematical Logic , vol. 11 (1977), no. 2, pp. 147171.CrossRefGoogle Scholar
Metakides, G. and Nerode, A., Effective content of field theory . Annals of Mathematical Logic , vol. 17 (1979), no. 3, pp. 289320.CrossRefGoogle Scholar
Metakides, G., Nerode, A., and Shore, R. A., Recursive limits on the Hahn–Banach theorem , Errett Bishop: Reflections on Him and His Research (M. Rosenbla, editor), Contemporary Mathematics, vol. 39, American Mathematical Society, Providence, 1985, pp. 8591.CrossRefGoogle Scholar
Miller, J. S., $\boldsymbol{\varPi}_{\boldsymbol{1}}^{\boldsymbol{0}}$ classes in computable analysis and topology , Ph.D. thesis, Cornell University, Ithaca, 2002.Google Scholar
Mori, T., Tsujii, Y., and Yasugi, M., Computability structures on metric spaces , Combinatorics, Complexity, and Logic (D. S. Bridges, C. S. Calude, J. Gibbons, S. Reeves, and I. H. Witten, editors), Discrete Mathematics and Theoretical Computer Science, vol. 1, Springer, Singapore, 1997, pp. 351362.Google Scholar
Moschovakis, Y. N., Recursive metric spaces . Fundamenta Mathematicae , vol. 55 (1964), pp. 215238.CrossRefGoogle Scholar
Moschovakis, Y. N., Descriptive Set Theory , second ed., Mathematical Surveys and Monographs, vol. 155, American Mathematical Society, Providence, 2009.CrossRefGoogle Scholar
Mummert, C., Reverse mathematics of MF spaces . Journal of Mathematical Logic , vol. 6 (2006), no. 2, pp. 203232.CrossRefGoogle Scholar
Munkres, J. R., Elements of Algebraic Topology , Addison-Wesley, Menlo Park, 1984.Google Scholar
Myhill, J., A recursive function, defined on a compact interval and having a continuous derivative that is not recursive . Michigan Mathematical Journal , vol. 18 (1971), no. 2, pp. 9798.CrossRefGoogle Scholar
Nerode, A. and Huang, W. Q., An application of pure recursion theory to recursive analysis . Acta Mathematica Sinica , vol. 28 (1985), no. 5, pp. 625636.Google Scholar
Neumann, E., On the computability of the set of automorphisms of the unit square . Theoretical Computer Science , vol. 903 (2022), pp. 7483.CrossRefGoogle Scholar
Nies, A. (editor), Logic Blog 2016, preprint available from arXiv:1703.01573.Google Scholar
Nies, A. and Solecki, S., Local compactness for computable Polish metric spaces is ${\varPi}_1^1$ -complete, Evolving Computability (A. Beckmann, V. Mitrana, and M. Soskova, editors), Proceedings of 11th Conference on Computability in Europe, CiE 2015, Bucharest, Romania, June 29-July 3, 2015, pp. 286290. Available at https://link.springer.com/book/10.1007/978-3-319-20028-6 CrossRefGoogle Scholar
Nogina, E. J., Effectively topological spaces . Doklady Akademii Nauk SSSR , vol. 169 (1966), pp. 2831.Google Scholar
Nogina, E. J., Correlations between certain classes of effectively topological spaces . Matematicheskie Zametki , vol. 5 (1969), pp. 483495.Google Scholar
Odintsov, S. P. and Selivanov, V. L., Arithmetic hierarchy and ideals of enumerated Boolean algebras . Siberian Mathematical Journal , vol. 30 (1989), no. 6, pp. 952960.CrossRefGoogle Scholar
Pauly, A., On the topological aspects of the theory of represented spaces . Computability , vol. 5 (2016), no. 2, pp. 159180.CrossRefGoogle Scholar
Pauly, A., Enumeration degrees and topology , Sailing Routes in the World of Computation (F. Manea, R. G. Miller, and D. Nowotka, editors), Lecture Notes in Computer Science, vol. 10936, Springer, Cham, 2018, pp. 328337.CrossRefGoogle Scholar
Pauly, A., Effective local compactness and the hyperspace of located sets, preprint, 2019, arXiv:1903.05490.Google Scholar
Pauly, A., Seon, D., and Ziegler, M., Computing Haar measures , 28th EACSL Annual Conference on Computer Science Logic (M. Fernández and A. Muscholl, editors), Leibniz International Proceedings in Informatics (LIPIcs), vol. 152, Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, Wadern, 2020, pp. 4:134:17.Google Scholar
Pontryagin, L. S., Foundations of Algebraic Topology , third ed., Nauka, Moscow, 1986.Google Scholar
Pour-El, M. B. and Caldwell, J., On a simple definition of computable function of a real variable—With applications to functions of a complex variable . Mathematical Logic Quarterly , vol. 21 (1975), no. 1, pp. 119.CrossRefGoogle Scholar
Pour-El, M. B. and Richards, I., Computability and noncomputability in classical analysis . Transactions of the American Mathematical Society , vol. 275 (1983), no. 2, pp. 539560.CrossRefGoogle Scholar
Pour-El, M. B. and Richards, J. I., Computability in Analysis and Physics , Perspectives in Mathematical Logic, Springer, Berlin, 1989.CrossRefGoogle Scholar
Reimann, J. and Slaman, T. A., Measures and their random reals . Transactions of the American Mathematical Society , vol. 367 (2015), no. 7, pp. 50815097.CrossRefGoogle Scholar
Rettinger, R., Compactness and the effectivity of uniformization , How the World Computes (S. B. Cooper, A. Dawar, and B. Löwe, editors), Lecture Notes in Computer Science, vol. 7318, Springer, Heidelberg, 2012, pp. 616625.CrossRefGoogle Scholar
La Roche, P. E., Contributions to recursive algebra , Ph.D. thesis, Cornell University, ProQuest LLC, Ann Arbor, 1978.Google Scholar
La Roche, P., Effective Galois theory . Journal of Symbolic Logic , vol. 46 (1981), no. 2, pp. 385392.CrossRefGoogle Scholar
Rogers, H.. Theory of Recursive Functions and Effective Computability , second ed., MIT Press, Cambridge, 1987.Google Scholar
Sagan, H., Space-Filling Curves , Universitext, Springer, New York, 1994.CrossRefGoogle Scholar
Selivanov, V. and Selivanova, S., Primitive recursive ordered fields and some applications. Computability , vol. 12 (2023), no. 1, pp. 7199.Google Scholar
Selivanov, V. L. and Selivanova, S., Primitive recursive ordered fields and some applications , Computer Algebra in Scientific Computing (F. Boulier, M. England, T. M. Sadykov, and E. V. Vorozhtsov, editors), Lecture Notes in Computer Science, vol. 12865, Springer, Cham, 2021, pp. 353369.CrossRefGoogle Scholar
Shoenfield, J. R., Degrees of models . Journal of Symbolic Logic , vol. 25 (1960), pp. 233237.CrossRefGoogle Scholar
Sierpiński, W., Sur un espace métrique séparable universel . Fundamenta Mathematicae , vol. 33 (1945), pp. 115122.CrossRefGoogle Scholar
Simpson, S., Subsystems of Second Order Arithmetic , second ed., Perspectives in Logic, Cambridge University Press, Cambridge, 2009.CrossRefGoogle Scholar
Smith, R. L., The theory of profinite groups with effective presentations , Ph.D. thesis, The Pennsylvania State University, ProQuest LLC, Ann Arbor, 1979.Google Scholar
Smith, R. L., Effective aspects of profinite groups . Journal of Symbolic Logic , vol. 46 (1981), no. 4, pp. 851863.CrossRefGoogle Scholar
Specker, E., Der Satz vom Maximum in der rekursiven Analysis , Constructivity in Mathematics: Proceedings of the Colloquium Held at Amsterdam, 1957 (A. Heyting, editor), Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1959, pp. 254265.Google Scholar
Spreen, D., A characterization of effective topological spaces , Recursion Theory Week (Oberwolfach, 1989) (K. Ambos-Spies, G. H. Müller, and G. E. Sacks, editors), Lecture Notes in Mathematics, vol. 1432, Springer, Berlin, 1990, pp. 363387.CrossRefGoogle Scholar
Spreen, D., Representations versus numberings: On the relationship of two computability notions . Theoretical Computer Science , vol. 262 (2001), nos. 1–2, pp. 473499.CrossRefGoogle Scholar
Spreen, D. and Young, P., Effective operators in a topological setting , Computation and Proof Theory (Aachen, 1983) (E. Börger, W. Oberschelp, M. M. Richter, B. Schinzel, and W. Thomas, editors), Lecture Notes in Mathematics, vol. 1104, Springer, Berlin, 1984, pp. 437451.CrossRefGoogle Scholar
Tran, Y.-Y., Computably enumerable Boolean algebras . Ph.D. thesis, Cornell, 2018. Available at https://ecommons.cornell.edu/handle/1813/59504 Google Scholar
Turing, A. M., On computable numbers, with an application to the Entscheidungsproblem . Proceedings of the London Mathematical Society , vol. 42 (1936), pp. 230265.Google Scholar
Turing, A. M., On computable numbers, with an application to the Entscheidungsproblem. A correction. Proceedings of the London Mathematical Society , vol. 43 (1937), pp. 544546.Google Scholar
Waterhouse, W. C., Profinite groups are Galois groups . Proceedings of the American Mathematical Society , vol. 42 (1974), pp. 639640.Google Scholar
Weihrauch, K., Computable Analysis: An Introduction , Texts in Theoretical Computer Science. An EATCS Series, Springer, Berlin, 2000.CrossRefGoogle Scholar
Weihrauch, K., Computational complexity on computable metric spaces . Mathematical Logic Quarterly , vol. 49 (2003), no. 1, pp. 321.CrossRefGoogle Scholar
Weihrauch, K. and Grubba, T., Elementary computable topology . Journal of Universal Computer Science , vol. 15 (2009), no. 6, pp. 13811422.Google Scholar
Zaslavskiĭ, I. D., Some properties of constructive real numbers and constructive functions . Trudy Matematicheskogo Instituta Imeni V. A. Steklova , vol. 67 (1962), pp. 385457.Google Scholar