It is shown that for compact metric spaces the following statements are pairwise equivalent: “X is Loeb”, “X is separable”, “X has a we ordered dense subset”, “X is second countable”, and “X has a dense set G = ∪{Gn : n ∈ ω}, ∣Gn∣ < ω, with limn→∞ diam = 0”. Further, it is shown that the statement: “Compact metric spaces are weakly Loeb” is not provable in ZF0 , the Zermelo-Fraenkel set theory without the (...) axiom of regularity, and that the countable axiom of choice for families of finite sets CACfin does not imply the statement “Compact metric spaces are separable”. (shrink)

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. (shrink)

Although classically every open subspace of a locally compact space is also locally compact, constructively this is not generally true. This paper provides a locally compact remetrization for an open set in a compact metric space and constructs a one-point compactification. MSC: 54D45, 03F60, 03F65.

We introduce a new Turing machine based concept of time complexity for functions on computable metric spaces. It generalizes the ordinary complexity of word functions and the complexity of real functions studied by Ko [19] et al. Although this definition of TIME as the maximum of a generally infinite family of numbers looks straightforward, at first glance, examples for which this maximum exists seem to be very rare. It is the main purpose of this paper to prove that, nevertheless, (...) the definition has a large number of important applications. Using the framework of TTE [40], we introduce computable metric spaces and computability on the compact subsets. We prove that every computable metric space has a c-proper c-admissible representation. We prove that Turing machine time complexity of a function computable relative to c-admissible c-proper representations has a computable bound on every computable compact subset. We prove that computably compact computable metric spaces have concise c-proper c-admissible representations and show by examples that many canonical representations are of this kind. Finally, we compare our definition with a similar one by Labhalla et al. [22]. Several examples illustrate the concepts. By these results natural and realistic definitions of computational complexity are now available for a variety of numerical problems such as image processing, integration, continuous Fourier transform or wave propagation. (shrink)

The localic completion of a metric space induces a canonical notion of continuous map between metric spaces. It is shown that these maps are continuous in the sense of Bishop constructive mathematics, i.e., uniformly continuous near every compact image.

We study Polish spaces for which a set of possible distances $A \subseteq R^+$ is fixed in advance. We determine, depending on the properties of A, the complexity of the collection of all Polish metric spaces with distances in A, obtaining also example of sets in some Wadge classes where not many natural examples are known. Moreover we describe the properties that A must have in order that all Polish spaces with distances in that set belong to a given (...) class, such as zero-dimensional, locally compact, etc. These results lead us to give a fairly complete description of the complexity, with respect to Borel reducibility and again depending on the properties of A, of the relations of isometry and isometric embeddability between these Polish spaces. (shrink)

In [14], we studied the computational behaviour of various first-order and modal languages interpreted in metric or weaker distance spaces. [13] gave an axiomatisation of an expressive and decidable metric logic. The main result of this paper is in showing that the technique of representing metric spaces by means of Kripke frames can be extended to cover the modal (hybrid) language that is expressively complete over metric spaces for the (undecidable) two-variable fragment of first-order logic with (...) binary pred-icates interpreting the metric. The frame conditions needed correspond rather directly with a Boolean modal logic that is, again, of the same expressivity as the two-variable fragment. We use this representation to derive an axiomatisation of the modal hybrid variant of the two-variable fragment, discuss the compactness property in distance logics, and derive some results on (the failure of) interpolation in distance logics of various expressive power. (shrink)

How are the various classically equivalent definitions of compactness for metric spaces constructively interrelated? This question is addressed with Bishop-style constructive mathematics as the basic system – that is, the underlying logic is the intuitionistic one enriched with the principle of dependent choices. Besides surveying today's knowledge, the consequences and equivalents of several sequential notions of compactness are investigated. For instance, we establish the perhaps unexpected constructive implication that every sequentially compact separable metric space is totally (...) bounded. As a by-product, the fan theorem for detachable bars of the complete binary fan proves to be necessary for the unit interval possessing the Heine-Borel property for coverings by countably many possibly empty open balls. (shrink)

We prove strong completeness results for some modal logics with the universal modality, with respect to their topological semantics over 0-dimensional dense-in-themselves metric spaces. We also use failure of compactness to show that, for some languages and spaces, no standard modal deductive system is strongly complete.

A metric space is said to be locally non-compact if every neighborhood contains a sequence that is eventually bounded away from every element of the space, hence contains no accumulation point. We show within recursive mathematics that a nonvoid complete metric space is locally non-compact iff it is without isolated points.The result has an interesting consequence in computable analysis: If a complete metric space has a computable witness that it is without (...) isolated points, then every neighborhood contains a computable sequence that is eventually computably bounded away from every computable element of the space. (shrink)

We study the isomorphism relation on Borel classes of locally compact Polish metric structures. We prove that isomorphism on such classes is always classifiable by countable structures (equivalently: Borel reducible to graph isomorphism), which implies, in particular, that isometry of locally compact Polish metric spaces is Borel reducible to graph isomorphism. We show that potentially $\boldsymbol {\Pi }^{0}_{\alpha + 1}$ isomorphism relations are Borel reducible to equality on hereditarily countable sets of rank $\alpha $, $\alpha \geq (...) 2$. We also study approximations of the Hjorth-isomorphism game, and formulate a condition ruling out classifiability by countable structures. (shrink)

In a previous paper we constructed a full and faithful functor ℳ from the category of locally compact metric spaces to the category of formal topologies . Here we show that for a real-valued continuous function f, ℳ factors through the localic positive reals if, and only if, f has a uniform positive lower bound on each ball in the locally compact space. We work within the framework of Bishop constructive mathematics, where the latter notion is (...) strictly stronger than point-wise positivity. (shrink)

We show that the set of points of an overt closed subspace of a metric completion of a Bishop-locally compact metric space is located. Consequently, if the subspace is, moreover, compact, then its collection of points is Bishop-compact. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

The paper introduces a broad family of metrics applicable to finite and countably infinite strings, or, by extension, to formal structures serving as semantics for countable languages. The main focus is on applications to sets of pointed Kripke models, a semantics for modal logics. For the resulting metric spaces, the paper classifies topological properties including which metrics are topologically equivalent, providing sufficient conditions for compactness, characterizing clopen sets and isolated points, and characterizing the metrical topologies by a concept of (...) logical convergence. We then apply the approach to maps from dynamic epistemic logic, showing that product updates with action models yield continuous maps, hence allowing for an interpretation of the iterated updates as discrete time dynamical systems. (shrink)

Dini's theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of real-valued continuous functions whose limit is continuous. By showing that Dini's theorem is equivalent to Brouwer's fan theorem for detachable bars, we provide Dini's theorem with a classification in the recently established constructive reverse mathematics propagated by Ishihara. As a complement, Dini's theorem is proved to be equivalent to the analogue of the fan theorem, weak König's (...) lemma, in the original classical setting of reverse mathematics started by Friedman and Simpson. (shrink)

For a signature L with at least one constant symbol, an L‐structure is called minimal if it has no proper substructures. Let be the set of isomorphism types of minimal L‐structures. The elements of can be identified with ultrafilters of the Boolean algebra of quantifier‐free L‐sentences, and therefore one can define a Stone topology on. This topology on generalizes the topology of the space of n‐marked groups. We introduce a natural ultrametric on, and show that the Stone topology on (...) coincides with the topology of the ultrametric space iff the ultrametric space is compact iff L is locally finite (that is, L contains finitely many n‐ary symbols for any ). As one of the applications of compactness of the Stone topology on, we prove compactness of certain classes of metric spaces in the Gromov‐Hausdorff topology. This slightly refines the known result based on Gromov's ideas that any uniformly totally bounded class of compact metric spaces is precompact. (shrink)

It is folklore that if a continuous function on a complete metric space has approximate roots and in a uniform manner at most one root, then it actually has a root, which of course is uniquely determined. Also in Bishop's constructive mathematics with countable choice, the general setting of the present note, there is a simple method to validate this heuristic principle. The unique solution even becomes a continuous function in the parameters by a mild modification of the (...) uniqueness hypothesis. Moreover, Brouwer's fan theorem for decidable bars turns out to be equivalent to the statement that, for uniformly continuous functions on a compact metric space, the crucial uniform “at most one” condition follows from its non-uniform counterpart. This classification in the spirit of the constructive reverse mathematics, as propagated by Ishihara and others, sharpens an earlier result obtained jointly with Berger and Bridges. (shrink)

This paper studies the metric structure of the space Hr of absolutely summable sequences of real numbers with at most r nonzero terms. Hr is complete, and is located and nowhere dense in the space of all absolutely summable sequences. Totally bounded and compact subspaces of Hr are characterized, and large classes of located, totally bounded, compact, and locally compact subspaces are constructed. The methods used are constructive in the strict sense. MSC: 03F65, 54E50.

A weak constructive sequential compactness property of metric spaces is introduced. It is proved that for complete, totally bounded metric spaces this property is equivalent to Brouwer's fan theorem for detachable bars. Our results form a part of constructive reverse mathematics.

Let X be a compact metric space. A closed set K $\subseteq$ X is located if the distance function d(x, K) exists as a continuous real-valued function on X; weakly located if the predicate d(x, K) $>$ r is Σ 0 1 allowing parameters. The purpose of this paper is to explore the concepts of located and weakly located subsets of a compact separable metric space in the context of subsystems of second order arithmetic (...) such as RCA 0 , WKL 0 and ACA 0 . We also give some applications of these concepts by discussing some versions of the Tietze extension theorem. In particular we prove an RCA 0 version of this result for weakly located closed sets. (shrink)

We develop measure theory in the context of subsystems of second order arithmetic with restricted induction. We introduce a combinatorial principleWWKL (weak-weak König's lemma) and prove that it is strictly weaker thanWKL (weak König's lemma). We show thatWWKL is equivalent to a formal version of the statement that Lebesgue measure is countably additive on open sets. We also show thatWWKL is equivalent to a formal version of the statement that any Borel measure on a compact metric space (...) is countably additive on open sets. (shrink)

We study the role that the axiom of choice plays in Tychonoff's product theorem restricted to countable families of compact, as well as, Lindelöf metric spaces, and in disjoint topological unions of countably many such spaces.

It is shown constructively that, on a metric space that is dense in itself, if every pointwise continuous, real-valued function is uniformly sequentially continuous, then the space has the anti-Specker property. The converse is also discussed. Finally, we show that the anti-Specker property implies a restricted form of countable compactness.

In this note we show that the Axiom of Countable Choice is equivalent to two statements from the theory of pseudometric spaces: the first of them is a well-known characterization of uniform continuity for functions between metric spaces, and the second declares that sequentially compact pseudometric spaces are \—meaning that all real valued, continuous functions defined on these spaces are necessarily uniformly continuous.

We generalize the model theory of small profinite structures developed by Newelski to the case of compact metric spaces considered together with compact groups of homeomorphisms and satisfying the existence of m-independent extensions (we call them compact e-structures). We analyze the relationships between smallness and different versions of the assumption of the existence of m-independent extensions and we obtain some topological consequences of these assumptions. Using them, we adopt Newelski's proofs of various results about small profinite (...) structures to compact e-structures. In particular, we notice that a variant of the group configuration theorem holds in this context. A general construction of compact structures is described. Using it, a class of examples of compact e-structures which are not small is constructed. It is also noticed that in an m-stable compact e-structure every orbit is equidominant with a product of m-regular orbits. (shrink)

The research presented in this paper was motivated by our aim to study a problem due to J. Bourgain [3]. The problem in question concerns the uniform boundedness of the classical separation rank of the elements of a separable compact set of the first Baire class. In the sequel we shall refer to these sets (separable or non-separable) as Rosenthal compacta and we shall denote by ∝(f) the separation rank of a real-valued functionfinB1(X), withXa Polish space. Notice that (...) in [3], Bourgain has provided a positive answer to this problem in the case ofKsatisfyingwithXa compact metric space. The key ingredient in Bourgain's approach is that whenever a sequence of continuous functions pointwise converges to a functionf, then the possible discontinuities of the limit function reflect a local ℓ1-structure to the sequence (fn)n. More precisely the complexity of this ℓ1-structure increases as the complexity of the discontinuities offdoes. This fruitful idea was extensively studied by several authors (c.f. [5], [7], [8]) and for an exposition of the related results we refer to [1]. It is worth mentioning that A.S. Kechris and A. Louveau have invented the rank rND(f) which permits the link between thec0-structure of a sequence (fn)nof uniformly bounded continuous functions and the discontinuities of its pointwise limit. Rosenthal'sc0-theorem [11] and thec0-index theorem [2] are consequences of this interaction.Passing to the case where either (fn)nare not continuous orXis a non-compact Polish space, this nice interaction is completely lost. (shrink)

We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non-compact (...) CSM. Both results rely on having careful constructive formulations of the concepts involved.As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from X to ℝ are continuous”, when X is an inhabited CSM without isolated points, and when X is an inhabited locally non-compact CSM. One situation in which the latter case applies is in models based on “domain realizability”, in which the failure of the continuity principle for any inhabited locally non-compact CSM, X, generalizes a result previously obtained by Escardó and Streicher in the special case X = C[0, 1].As a second application, we show that, when the notion of inhabited complete separable metric space without isolated points is interpreted in a recursion-theoretic setting, then, for any such space X, there exists a Banach-Mazur computable function from X to the computable real numbers that is not Markov computable. This generalizes a result obtained by Hertling in the special case that X is the space of computable real numbers. (shrink)

Let X be a Polish space and a separable compact subset of the first Baire class on X. For every sequence dense in , the descriptive set-theoretic properties of the set are analyzed. It is shown that if is not first countable, then is -complete. This can also happen even if is a pre-metric compactum of degree at most two, in the sense of S. Todorčević. However, if is of degree exactly two, then is always Borel. A (...) deep result of G. Debs implies that contains a Borel cofinal set and this gives a tree-representation of . We show that classical ordinal assignments of Baire-1 functions are actually -ranks on . We also provide an example of a Ramsey-null subset A of for which there does not exist a Borel set BA such that the difference BA is Ramsey-null. (shrink)

Given a finite lexicon L of relational symbols and equality, one may view the collection of all L-structures on the set of natural numbers ω as a space in several different ways. We consider it as: (i) the space of outcomes of certain infinite two-person games; (ii) a compact metric space; and (iii) a probability measure space. For each of these viewpoints, we can give a notion of relative ubiquity, or largeness, for invariant sets (...) of structures on ω. For example, in every sense of relative ubiquity considered here, the set of dense linear orderings on ω is ubiquitous in the set of linear orderings on ω. (shrink)

Families of Borel equivalence relations and quasiorders that are cofinal with respect to the Borel reducibility ordering, ≤B, are constructed. There is an analytic ideal on ω generating a complete analytic equivalence relation and any Borel equivalence relation reduces to one generated by a Borel ideal. Several Borel equivalence relations, among them Lipschitz isomorphism of compact metric spaces, are shown to be Kσ complete.

We prove constructively that, in order to derive the uniform continuity theorem for pointwise continuous mappings from a compact metric space into a metric space, it is necessary and sufficient to prove any of a number of equivalent conditions, such as that every pointwise continuous mapping of [0, 1] into R is bounded. The proofs are analytic, making no use of, for example, fan-theoretic ideas.

The classical Hahn–Banach Theorem states that any linear bounded functional defined on a linear subspace of a normed space admits a norm-preserving linear bounded extension to the whole space. The constructive and computational content of this theorem has been studied by Bishop, Bridges, Metakides, Nerode, Shore, Kalantari Downey, Ishihara and others and it is known that the theorem does not admit a general computable version. We prove a new computable version of this theorem without unrolling the classical proof (...) of the theorem itself. More precisely, we study computability properties of the uniform extension operator which maps each functional and subspace to the set of corresponding extensions. It turns out that this operator is upper semi-computable in a well-defined sense. By applying a computable version of the Banach–Alaoglu Theorem we can show that computing a Hahn–Banach extension cannot be harder than finding a zero in a compact metric space. This allows us to conclude that the Hahn–Banach extension operator is ${\bf {\Sigma^{0}_{2}}}$ -computable while it is easy to see that it is not lower semi-computable in general. Moreover, we can derive computable versions of the Hahn–Banach Theorem for those functionals and subspaces which admit unique extensions. (shrink)

Suppose that fn is a sequence of nonnegative functions with compact support on a locally compact metric space, that T is a nonnegative linear functional, and that equation imageT fn < T f0. A result of Bishop, foundational to a constructive theory of functional analysis, asserts the existence of a point x such that equation imagefn < f0. This paper extends this result to arbitrary Hausdorff spaces, and gives short proofs using nonstandard analysis. While such arguments (...) used are not themselves constructive, they can illuminate where the difficulty lies in finding the point x. An algorithm for constructing x is then given, with a nonstandard proof that the algorithm converges to a correct value. (shrink)

This paper develops a general theory of uniform probability for compact metric spaces. Special cases of uniform probability include Lebesgue measure, the volume element on a Riemannian manifold, Haar measure, and various fractal measures (all suitably normalized). This paper first appeared fall of 1990 in the Journal of Theoretical Probability, vol. 3, no. 4, pp. 611—626. The key words by which this article was indexed were: ε-capacity, weak convergence, uniform probability, Hausdorff dimension, and capacity dimension.

In a previous paper-[17]-we characterized strong measure zero sets of reals in terms of a Ramseyan partition relation on certain subspaces of the Alexandroff duplicate of the unit interval. This framework gave only indirect access to the relevant sets of real numbers. We now work more directly with the sets in question, and since it costs little in additional technicalities, we consider the more general context of metric spaces and prove: 1. If a metric space has a (...) covering property of Hurewicz and has strong measure zero, then its product with any strong measure zero metric space is a strong measure zero metric space (Theorem 1 and Lemma 3). 2. A subspace X of a σ-compact metric space Y has strong measure zero if, and only if, a certain Ramseyan partition relation holds for Y (Theorem 9). 3. A subspace X of a σ-compact metric space Y has strong measure zero in all finite powers if, and only if, a certain Ramseyan partition relation holds for Y (Theorem 12). Then 2 and 3 yield characterizations of strong measure zeroness for σ-totally bounded metric spaces in terms of Ramseyan theorems. (shrink)

The anti-Specker property, a constructive version of sequential compactness, is used to prove constructively that a pointwise continuous, order-dense preference relation on a compact metric space is uniformly sequentially continuous. It is then shown that Ishihara's principle BD-ℕ implies that a uniformly sequentially continuous, order-dense preference relation on a separable metric space is uniformly continuous. Converses of these two theorems are also proved.

We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non‐ (...) class='Hi'>compact CSM. Both results rely on having careful constructive formulations of the concepts involved.As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from X to ℝ are continuous”, when X is an inhabited CSM without isolated points, and when X is an inhabited locally non‐compact CSM. One situation in which the latter case applies is in models based on “domain realizability”, in which the failure of the continuity principle for any inhabited locally non‐compact CSM, X, generalizes a result previously obtained by Escardó and Streicher in the special case X = C[0, 1].As a second application, we show that, when the notion of inhabited complete separable metric space without isolated points is interpreted in a recursion‐theoretic setting, then, for any such space X, there exists a Banach‐Mazur computable function from X to the computable real numbers that is not Markov computable. This generalizes a result obtained by Hertling in the special case that X is the space of computable real numbers. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

Let H be an infinite-dimensional (real or complex) Hilbert space, viewed as a metric structure in its natural signature. We characterize the definable linear operators on H as exactly the "scalar plus compact" operators.

We prove two embedding and extension theorems in the context of the constructive theory of metric spaces. The first states that Cantor space embeds in any inhabited complete separable metric space (CSM) without isolated points, X, in such a way that every sequentially continuous function from Cantor space to ℤ extends to a sequentially continuous function from X to ℝ. The second asserts an analogous property for Baire space relative to any inhabited locally non‐ (...) class='Hi'>compact CSM. Both results rely on having careful constructive formulations of the concepts involved.As a first application, we derive new relationships between “continuity principles” asserting that all functions between specified metric spaces are pointwise continuous. In particular, we give conditions that imply the failure of the continuity principle “all functions from X to ℝ are continuous”, when X is an inhabited CSM without isolated points, and when X is an inhabited locally non‐compact CSM. One situation in which the latter case applies is in models based on “domain realizability”, in which the failure of the continuity principle for any inhabited locally non‐compact CSM, X, generalizes a result previously obtained by Escardó and Streicher in the special case X = C[0, 1].As a second application, we show that, when the notion of inhabited complete separable metric space without isolated points is interpreted in a recursion‐theoretic setting, then, for any such space X, there exists a Banach‐Mazur computable function from X to the computable real numbers that is not Markov computable. This generalizes a result obtained by Hertling in the special case that X is the space of computable real numbers. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

Yu, X., Riesz representation theorem, Borel measures and subsystems of second-order arithmetic, Annals of Pure and Applied Logic 59 65-78. Formalized concept of finite Borel measures is developed in the language of second-order arithmetic. Formalization of the Riesz representation theorem is proved to be equivalent to arithmetical comprehension. Codes of Borel sets of complete separable metric spaces are defined and proved to be meaningful in the subsystem ATR0. Arithmetical transfinite recursion is enough to prove the measurability of Borel sets (...) for any finite Borel measure on a compact complete separable metric space. (shrink)

Computability theoretic aspects of Polish metric spaces are studied by adapting notions and methods of computable structure theory. In this dissertation, we mainly investigate index sets and classification problems for computably presentable Polish metric spaces. We find the complexity of a number of index sets, isomorphism problems, and embedding problems for computably presentable metric spaces. We also provide several computable structure theory results related to some classical Polish metric spaces such as the Urysohn space $\mathbb (...) {U}$, the Cantor space $2^{\mathbb {N}}$, the Baire space $\mathbb {N}^{\mathbb {N}}$, and spaces of continuous functions.Abstract prepared by Teerawat Thewmorakot.E-mail: [email protected]. (shrink)

We study the complexity of isomorphism of classes of metric structures using methods from infinitary continuous logic. For Borel classes of locally compact structures, we prove that if the equivalence relation of isomorphism is potentially $\mathbf {\Sigma }^0_2$, then it is essentially countable. We also provide an equivalent model-theoretic condition that is easy to check in practice. This theorem is a common generalization of a result of Hjorth about pseudo-connected metric spaces and a result of Hjorth–Kechris about (...) discrete structures. As a different application, we also give a new proof of Kechris’s theorem that orbit equivalence relations of actions of Polish locally compact groups are essentially countable. (shrink)

"The last remnant of physical objectivity of space-time" is disclosed, beyond the Leibniz equivalence, in the case of a continuous family of spatially non-compact models of general relativity. The physical individuation of point-events is furnished by the intrinsic degrees of freedom of the gravitational field, (viz, the "Dirac observables") that represent - as it were - the "ontic" part of the metric field. The physical role of the "epistemic" part (viz. the "gauge" variables) is likewise clarified. At (...) the end, a peculiar four-dimensional "holistic and structuralist" view of space-time emerges which includes elements common to the tradition of both substantivalism and relationism. The observables of our models undergo real "temporal change" and thereby provide a counter-example to the thesis of the "frozen-time" picture of evolution. (shrink)

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of (...) a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. ‘Bishop compact’ is translated as compact and overt. We propose a definition of locatedness on subspaces of a formal topology, and prove that a closed subspace of a compact regular formal space is located iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact — that is, totally bounded and complete — iff its localic completion is compact overt.Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales.We work constructively, predicatively and avoid the use of the axiom of countable choice. (shrink)

In this paper we study a reducibility that has been introduced by Klaus Weihrauch or, more precisely, a natural extension for multi-valued functions on represented spaces. We call the corresponding equivalence classes Weihrauch degrees and we show that the corresponding partial order induces a lower semi-lattice. It turns out that parallelization is a closure operator for this semi-lattice and that the parallelized Weihrauch degrees even form a lattice into which the Medvedev lattice and the Turing degrees can be embedded. The (...) importance of Weihrauch degrees is based on the fact that multi-valued functions on represented spaces can be considered as realizers of mathematical theorems in a very natural way and studying the Weihrauch reductions between theorems in this sense means to ask which theorems can be transformed continuously or computably into each other. As crucial corner points of this classification scheme the limited principle of omniscience LPO, the lesser limited principle of omniscience LLPO and their parallelizations are studied. It is proved that parallelized LLPO is equivalent to Weak Kőnig's Lemma and hence to the Hahn—Banach Theorem in this new and very strong sense. We call a multi-valued function weakly computable if it is reducible to the Weihrauch degree of parallelized LLPO and we present a new proof, based on a computational version of Kleene's ternary logic, that the class of weakly computable operations is closed under composition. Moreover, weakly computable operations on computable metric spaces are characterized as operations that admit upper semi-computable compact-valued selectors and it is proved that any single-valued weakly computable operation is already computable in the ordinary sense. (shrink)

We present a survey of the recent applications of continuous domains for providing simple computational models for classical spaces in mathematics including the real line, countably based locally compact spaces, complete separable metric spaces, separable Banach spaces and spaces of probability distributions. It is shown how these models have a logical and effective presentation and how they are used to give a computational framework in several areas in mathematics and physics. These include fractal geometry, where new results on (...) existence and uniqueness of attractors and invariant distributions have been obtained, measure and integration theory, where a generalization of the Riemann theory of integration has been developed, and real arithmetic, where a feasible setting for exact computer arithmetic has been formulated. We give a number of algorithms for computation in the theory of iterated function systems with applications in statistical physics and in period doubling route to chaos; we also show how efficient algorithms have been obtained for computing elementary functions in exact real arithmetic. (shrink)

Kohlenbach, U., Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation, Annals of Pure and Applied Logic 64 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical (...) assumptions x εXy ε Yx z ε Z = 0) only , then we can extract from the proof of → an effective modulus of uniqueness, which depends on u, k but not on v1,v2, i.e., u ε U, v1, v2 ε Vu, k εG, G 2-φuk→dv2-itk). Such a modulus φ can e.g. be used to give a finite algorithm which computes the zero of G on Vu with prescribed precision if it exists classically.The extraction of φ uses a proof-theoretic combination of functional interpretation and pointwise majorization. If the proof of → uses only simple instances of induction, then φ is a simple mathematical operation. (shrink)