In finite type arithmetic, the real numbers are represented by rapidly converging Cauchy sequences of rational numbers. Ulrich Kohlenbach introduced abstract types for certain structures such as metric spaces, normed spaces, Hilbert spaces, etc. With these types, the elements of the spaces are given directly, not through the mediation of a representation. However, these abstract spaces presuppose the real numbers. In this paper, we show how to set up an abstract type for the real numbers. The appropriateness of our construction (...) works in tandem with the bounded functional interpretation. (shrink)

The computability of reals was introduced by Alan Turing [20] by means of decimal representations. But the equivalent notion can also be introduced accordingly if the binary expansion, Dedekind cut or Cauchy sequence representations are considered instead. In other words, the computability of reals is independent of their representations. However, as it is shown by Specker [19] and Ko [9], the primitive recursiveness and polynomial time computability of the reals do depend on the representation. In this paper, we explore how (...) the weak computability of reals depends on the representation. To this end, we introduce three notions of weak computability in a way similar to the Ershov's hierarchy of Δ02-sets of natural numbers based on the binary expansion, Dedekind cut and Cauchy sequence, respectively. This leads to a series of classes of reals with different levels of computability. We investigate systematically questions as on which level these notions are equivalent. We also compare them with other known classes of reals like c. e. and d-c. e. reals. (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 present finitary formulations of two well known results concerning infinite series, namely Abel's theorem, which establishes that if a series converges to some limit then its Abel sum converges to the same limit, and Tauber's theorem, which presents a simple condition under which the converse holds. Our approach is inspired by proof theory, and in particular Gödel's functional interpretation, which we use to establish quantitative versions of both of these results.

For the computability of subsets of real numbers, several reasonable notions have been suggested in the literature. We compare these notions in a systematic way by relating them to pairs of ‘basic’ ones. They turn out to coincide for full-dimensional convex sets; but on the more general class of regular sets, they reveal rather interesting ‘weaker/stronger’ relations. This is in contrast to single real numbers and vectors where all ‘reasonable’ notions coincide.

Let h : ℕ → ℚ be a computable function. A real number x is called h-monotonically computable if there is a computable sequence of rational numbers which converges to x h-monotonically in the sense that h|x – xn| ≥ |x – xm| for all n andm > n. In this paper we investigate classes h-MC of h-mc real numbers for different computable functions h. Especially, for computable functions h : ℕ → ℚ, we show that the class h-MC coincides (...) with the classes of computable and semi-computable real numbers if and only if Σi∈ℕ) = ∞and the sum Σi∈ℕ) is a computable real number, respectively. On the other hand, if h ≥ 1 and h converges to 1, then h-MC = SC no matter how fast h converges to 1. Furthermore, for any constant c > 1, if h is increasing and converges to c, then h-MC = c-MC. Finally, if h is monotone and unbounded, then h-MC contains all ω-mc real numbers which are g-mc for some computable function g. (shrink)

Specker sequences are constructive, increasing, bounded sequences of rationals that do not converge to any constructive real. A sequence is said to be a strong Specker sequence if it is Specker and eventually bounded away from every constructive real. Within Bishop's constructive mathematics we investigate non-decreasing, bounded sequences of rationals that eventually avoid sets that are unions of sequences of intervals with rational endpoints. This yields surprisingly straightforward proofs of certain basic results fromconstructive mathematics. Within Russian constructivism, we show how (...) to use this general method to generate Specker sequences. Furthermore, we show that any nonvoid subset of the constructive reals that has no isolated points contains a strictly increasing sequence that is eventually bounded away from every constructive real. If every neighborhood of every point in the subset contains a rational number different from that point, the subset contains a strong Specker sequence. (shrink)

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)

In the informal setting of Bishop-style constructive reverse mathematics we discuss the connection between the antithesis of Specker’s theorem, Ishihara’s principle BD-N, and various types of equicontinuity. In particular, we prove that the implication from pointwise equicontinuity to uniform sequential equicontinuity is equivalent to the antithesis of Specker’s theorem; and that, for a family of functions on a separable metric space, the implication from uniform sequential equicontinuity to uniform equicontinuity is equivalent to BD-N.

Working within Bishop’s constructive framework, we examine the connection between a weak version of the Heine–Borel property, a property antithetical to that in Specker’s theorem in recursive analysis, and the uniform continuity theorem for integer-valued functions. The paper is a contribution to the ongoing programme of constructive reverse mathematics.

Area number x is called k-monotonically computable , for constant k > 0, if there is a computable sequence n ∈ ℕ of rational numbers which converges to x such that the convergence is k-monotonic in the sense that k · |x — xn| ≥ |x — xm| for any m > n and x is monotonically computable if it is k-mc for some k > 0. x is weakly computable if there is a computable sequence s ∈ ℕ of (...) rational numbers converging to x such that the sum equation image|xs — xs + 1| is finite. In this paper we show that a mc real numbers are weakly computable but the converse fails. Furthermore, we show also an infinite hierarchy of mc real numbers. (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)

Vann McGee has argued that, given certain background assumptions and an ought-implies-can thesis about norms of rationality, Bayesianism conflicts globally with computationalism due to the fact that Robinson arithmetic is essentially undecidable. I show how to sharpen McGee's result using an additional fact from recursion theory—the existence of a computable sequence of computable reals with an uncomputable limit. In conjunction with the countable additivity requirement on probabilities, such a sequence can be used to construct a specific proposition to which Bayesianism (...) requires an agent to assign uncomputable credence—yielding a local conflict with computationalism. (shrink)

We study some representations of real numbers. We compare these representations, on the one hand from the viewpoint of recursive functionals, and of complexity on the other hand.The impossibility of obtaining some functions as recursive functionals is, in general, easy. This impossibility may often be explicited in terms of complexity: - existence of a sequence of low complexity whose image is not a recursive sequence, - existence of objects of low complexity but whose images have arbitrarily high time- complexity .Moreover, (...) some representations of real numbers that are equivalent from the viewpoint of recursive functionals, are very distinct from the viewpoint of complexity.We make a particular study of representations via continued fractions . We precise exactly what part of information available in the x's dfc is equivalent to the information available in its Dedekinds cut. We show that the sum of two reals whose dfcs are polynomial-time computable may be a real whose dfc has time complexity arbitrarily high.This work confirms that the unique representation of real numbers suitable for the ordinary calculus is via explicit Cauchy sequences of rationals.RésuméNous étudions différentes manières de présenter les nombres réels. Nous comparons ces présentations du point de vue des fonctionnelles récursives d'une part, et de celui des classes de complexité d'autre part.L'impossibilité d'obtenir certaines fonctions sous forme de fonctionnelles récursives est en général facile à établir. Cette impossiblité peut souvent être explicitée en termes de complexité: - il existe une suite de faible complexité dont l'image est une suite non récursive, - il existe des objets de faible complexité mais dont les images sont des objets de complexité arbitrairement grande .En outre, certaines présentations des réels équivalentes du point de vue des fonctionnelles récursives se distinguent nettement du point de vue de la complexité.Nous faisons une étude particulière concernant les développements en fraction continue . Nous précisions exactement quelle est la partie de l'information disponible dans le dfc d'un réel x qui équivaut à l'information disponible dans sa coupure de Dedekind. Nous montrons également que la somme de deux réels dont le dfc est calculable en temps polynomial peut être un réel dont le dfc est de complexité arbitrairement grande.Ce travail confirme que seule une présentation des réels via des suites de rationnels explicitement de Cauchy est adaptée aux calculs avec les réels. (shrink)

This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...) . In fact, it corresponds to rates of metastability of a particular simple form. Moreover, if a certain gap condition is satisfied, then B and L yield a bound on the number of possible fluctuations. We explain recent applications of proof mining to ergodic theory in terms of these results. (shrink)

A theory of approximation to measurable sets and measurable functions based on the concepts of recursion theory and discrete complexity theory is developed. The approximation method uses a model of oracle Turing machines, and so the computational complexity may be defined in a natural way. This complexity measure may be viewed as a formulation of the average-case complexity of real functions—in contrast to the more restrictive worst-case complexity. The relationship between these two complexity measures is further studied and compared with (...) the notion of the distribution-free probabilistic computation. The computational complexity of the Lebesgue integral of polynomial-time approximable functions is studied and related to the question “FP = ♯P?”. (shrink)

In this paper we continue our work of Kalantari and Welch . There we introduced machinery to produce a point-free approach to points and functions on topological spaces and found conditions for both which lend themselves to effectivization. While we studied recursive points in that paper, here, we present two useful classes of recursive functions on topological spaces, apply them to the reals, and find precise accounting for the nature of the properties of some examples that exist in the literature. (...) We end with a construction of a recursive function on a small subset of the unit interval which is strongly nonextendible. (shrink)

The content of existence theorems in the calculus of variations has been explored and an effective treatment of semi-continuity has been achieved. An algorithm has been developed which captures the natural algorithmic content of the notion of a semi-continuous function and this is used to obtain an effective version of the “chattering lemma” of control theory and ordinary differential equations. This lemma reveals the main computational content of the theory of relaxed optimal control.

In 1952, Heinrich Scholz published a question in The Journal of Symbolic Logic asking for a characterization of spectra, i.e., sets of natural numbers that are the cardinalities of finite models of first order sentences. Günter Asser in turn asked whether the complement of a spectrum is always a spectrum. These innocent questions turned out to be seminal for the development of finite model theory and descriptive complexity. In this paper we survey developments over the last 50-odd years pertaining to (...) the spectrum problem. Our presentation follows conceptual developments rather than the chronological order. Originally a number theoretic problem, it has been approached by means of recursion theory, resource bounded complexity theory, classification by complexity of the defining sentences, and finally by means of structural graph theory. Although Scholz' question was answered in various ways, Asser's question remains open. (shrink)

It is shown that a principle, which can be seen as a constructivised version of sequential compactness, is equivalent to a form of Brouwer’s fan theorem. The complexity of the latter depends on the geometry of the spaces involved in the former.

In mathematics, various representations of real numbers have been investigated. All these representations are mathematically equivalent because they lead to the same real structure – Dedekind-complete ordered field. Even the effective versions of these representations are equivalent in the sense that they define the same notion of computable real numbers. Although the computable real numbers can be defined in various equivalent ways, if “computable” is replaced by “primitive recursive” , these definitions lead to a number of different concepts, which we (...) compare in this article. We summarize the known results and add new ones. In particular we show that there is a proper hierarchy among p. r. real numbers by nested interval representation, Cauchy representation, b -adic expansion representation, Dedekind cut representation, and continued fraction expansion representation. Our goal is to clarify systematically how the primitive recursiveness depends on the representations of the real numbers. (shrink)

Gödel's Incompleteness Theorems have the same scientific status as Einstein's principle of relativity, Heisenberg's uncertainty principle, and Watson and Crick's double helix model of DNA. Our aim is to discuss some new faces of the incompleteness phenomenon unveiled by an information-theoretic approach to randomness and recent developments in quantum computing.

Working within Bishop-style constructive mathematics, we examine some of the consequences of the anti-Specker property, known to be equivalent to a version of Brouwer's fan theorem. The work is a contribution to constructive reverse mathematics.

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that (...) is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED. We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them. (shrink)