Search

Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's claim is provable in Heyting arithmetic in all finite types (HA ω) for definable functions of the system. The proof does not rely on elaborate proof theoretic methods such as normalisation or ordinal analysis. Instead, we internalise in HA ω the dialogue tree interpretation of Gödel's system T due to Escardó (2013). The interpretation determines a syntactic translation of terms, which yields a neighbourhood function from a closed term of HA ω with the required property. As applications of this result, we prove some well-known properties of HA ω : uniform continuity of definable functions from N N to N on the Cantor space; closure under the rule of bar induction; and closure of bar recursion for the lowest type with a definable stopping function. [ABSTRACT FROM AUTHOR]

We compare Brouwer's bar theorem and Spector's bar recursion for the lowest type in the context of constructive reverse mathematics. To this end, we reformulate bar recursion as a logical principle stating the existence of a bar recursor for every function which serves as the stopping condition of bar recursion. We then show that the decidable bar induction is equivalent to the existence of a bar recursor for every continuous function from N N to N with a continuous modulus. We also introduce fan recursion, the bar recursion for binary trees, and show that the decidable fan theorem is equivalent to the existence of a fan recursor for every continuous function from { 0 , 1 } N to N with a continuous modulus. The equivalence for bar induction holds over the extensional version of intuitionistic arithmetic in all finite types augmented with the characteristic principles of Gödel's Dialectica interpretation. On the other hand, we show the equivalence for fan theorem without using such extra principles. [ABSTRACT FROM AUTHOR]

We give solutions to two of the questions in a paper by Brendle, Brooke-Taylor, Ng and Nies. Our examples derive from a 2014 construction by Khan and Miller as well as new direct constructions using martingales. At the same time, we introduce the concept of i.o. subuniformity and relate this concept to recursive measure theory. We prove that there are classes closed downwards under Turing reducibility that have recursive measure zero and that are not i.o. subuniform. This shows that there are examples of classes that cannot be covered with methods other than probabilistic ones. It is easily seen that every set of hyperimmune degree can cover the recursive sets. We prove that there are both examples of hyperimmune-free degree that can and that cannot compute such a cover. [ABSTRACT FROM AUTHOR]

The present work investigates inductive inference from the perspective of reverse mathematics. Reverse mathematics is a framework that allows gauging the proof strength of theorems and axioms in many areas of mathematics. The present work applies its methods to basic notions of algorithmic learning theory such as Angluin's tell-tale criterion and its variants for learning in the limit and for conservative learning, as well as to the more general scenario of partial learning. These notions are studied in the reverse mathematics context for uniformly and weakly represented families of languages. The results are stated in terms of axioms referring to induction strength and to domination of weakly represented families of functions. [ABSTRACT FROM AUTHOR]

Several extensions of Gödel's system T with new forms of recursion have been designed for the purpose of giving a computational interpretation to classical analysis. One can organise many of these extensions into two groups: those based on bar recursion , which include Spector's original bar recursion, modified bar recursion and the more recent products of selections functions, or those based on open recursion which in particular include the symmetric Berardi–Bezem–Coquand (BBC) functional. We relate these two groups by showing that both open recursion and the BBC functional are primitive recursively equivalent to a variant of modified bar recursion. Our results, in combination with existing research, essentially complete the classification up to primitive recursive equivalence of those extensions of system T used to give a direct computational interpretation to choice principles. [ABSTRACT FROM AUTHOR]

Abstract: The main topic of the present work is the relation that a set X is strongly hyperimmune-free relative to Y. Here X is strongly hyperimmune-free relative to Y if and only if for every partial X-recursive function p there is a partial Y-recursive function q such that every a in the domain of p is also in the domain of q and satisfies , that is, p is majorised by q. For X being hyperimmune-free relative to Y, one also says that X is pmaj-reducible to Y . It is shown that between degrees not above the Halting problem the pmaj-reducibility coincides with the Turing reducibility and that therefore only recursive sets have a strongly hyperimmune-free Turing degree while those sets Turing above the Halting problem bound uncountably many sets with respect to the pmaj-relation. So pmaj-reduction is identical with Turing reduction on a class of sets of measure 1. Moreover, every pmaj-degree coincides with the corresponding Turing degree. The pmaj-degree of the Halting problem is definable with the pmaj-relation. [Copyright &y& Elsevier]

Abstract: We study the strength of , Rainbow Ramsey Theorem for colorings of triples, and prove that implies neither nor . To this end, we establish some recursion theoretic properties of cohesive sets and rainbows for colorings of pairs. We show that every sequence (2-bounded coloring of pairs) admits a cohesive set (infinite rainbow) of non-PA Turing degree; and that every -recursive sequence (2-bounded coloring of pairs) admits a cohesive set (infinite rainbow). [Copyright &y& Elsevier]

Abstract: We study the computably enumerable sets in terms of the: (a) Kolmogorov complexity of their initial segments; (b) Kolmogorov complexity of finite programs when they are used as oracles. We present an extended discussion of the existing research on this topic, along with recent developments and open problems. Besides this survey, our main original result is the following characterization of the computably enumerable sets with trivial initial segment prefix-free complexity. A computably enumerable set A is K-trivial if and only if the family of sets with complexity bounded by the complexity of A is uniformly computable from the halting problem. [Copyright &y& Elsevier]

We consider clopen game formulae , analogous to the open game formulae widely studied in admissible recursion theory. This leads to characterizing the locally countable Σ 1 1 -reflecting ordinals α as those for which, over L α , the clopen-game–definable relations are not precisely those which are both open-game and closed-game definable. [ABSTRACT FROM AUTHOR]

Abstract: This paper is divided into two parts. In Part I, we investigate the structure of honest elementary degrees, that is, the degree structure induced on the honest functions by the reducibility relation “being (Kalmar) elementary in”. In Part II, we generalise the degree theory found in Part I. We introduce the reducibility relation “being -elementary in”, where is an ordinal , and investigate the structure of honest -elementary degrees. Towards the end of the paper, we discuss relations between our degree theory and provability in Peano Arithmetic. [Copyright &y& Elsevier]

Abstract: We develop applications of selection functions to proof theory and computational extraction of witnesses from proofs in classical analysis. The main novelty is a translation of minimal logic plus Peirce law into minimal logic, which we refer to as Peirce translation, as it eliminates uses of Peirce law. When combined with modified realizability, this translation applies to full classical analysis, i.e. Peano arithmetic in the language of finite types extended with countable choice and dependent choice. A fundamental step in the interpretation is the realizability of a strengthening of the double-negation shift via the iterated product of selection functions. In a separate paper, we have shown that such a product of selection functions is equivalent, over system , to modified bar recursion. [Copyright &y& Elsevier]

Abstract: An implicit characterization of the class is given, without using any minimization scheme. This is the first purely recursion-theoretic formulation of . [Copyright &y& Elsevier]

Abstract: The larger project broached here is to look at the generally sentence “if is well-ordered then is well-ordered”, where is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded -models for a particular theory whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function . To illustrate this theme, we prove in this paper that the statement “if is well-ordered then is well-ordered” is equivalent to . This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search (deduction chains) [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a (small) fragment of . [Copyright &y& Elsevier]

Abstract: We generalize standard Turing machines, which work in time on a tape of length , to -machines with time and tape length , for some limit ordinal. We show that this provides a simple machine model adequate for classical admissible recursion theory as developed by G. Sacks and his school. For an admissible ordinal, the basic notions of -recursive or -recursively enumerable are equivalent to being computable or computably enumerable by an -machine, respectively. We emphasize the algorithmic approach to admissible recursion theory by indicating how the proof of the Sacks–Simpson theorem, i.e., the solution of Post’s problem in -recursion theory, could be based on -machines, without involving constructibility theory. [Copyright &y& Elsevier]

Abstract: We give an introduction to Turing categories, which are a convenient setting for the categorical study of abstract notions of computability. The concept of a Turing category first appeared (albeit not under that name or at the level of generality we present it here) in the work of Longo and Moggi; later, Di Paolo and Heller introduced the closely related recursion categories. One of the purposes of Turing categories is that they may be used to develop categorical formulations of recursion theory, but they also include other notions of computation, such as models of (partial) combinatory logic and of the (partial) lambda calculus. In this paper our aim is to give an introduction to the basic structural theory, while at the same time illustrating how the notion is a meeting point for various other areas of logic and computation. We also provide a detailed exposition of the connection between Turing categories and partial combinatory algebras and show the sense in which the study of Turing categories is equivalent to the study of PCAs. [Copyright &y& Elsevier]

Abstract: In this paper, the notions of -categorical and -categorical structures are introduced by choosing the isomorphism such that the function itself or its graph sits on the -th level of the Ershov hierarchy, respectively. Separations obtained by natural graphs which are the disjoint unions of countably many finite graphs. Furthermore, for size-bounded graphs, an easy criterion is given to say when it is computable-categorical and when it is only -categorical; in the latter case it is not -categorical for any recursive ordinal . [Copyright &y& Elsevier]

Abstract: Say a set is 1-generic if for any , there is a string such that or . It is known that can be split into two 1-generic degrees. In this paper, we generalize this and prove that any nonzero computably enumerable degree can be split into two 1-generic degrees. As a corollary, no two computably enumerable degrees bound the same class of 1-generic degrees. [Copyright &y& Elsevier]

This paper is a culmination of our new foundations for recursive analysis through recursive topology as reported in Kalantari and Welch (Ann Pure Appl. Logic 93 (1998) 125; 98 (1999) 87). While in those papers we developed groundwork for an approach to point free analysis and applied recursion theory, in this paper we blend techniques of recursion theory with those of topology to establish new findings. We present several new techniques different from existing ones which yield interesting results. Incidental to our work is a unifying explanation of various schools of study for recursive analysis. [Copyright &y& Elsevier]

We prove the existence of a perfect Π01 set of reals such that the uniform join of any of its infinite subsets is above 0′. We explain a couple of ways in which this demonstrates the optimality of the Low Basis Theorem. [Copyright &y& Elsevier]

This paper considers reductions between types of numberings; these reductions preserve the Rogers Semilattice of the numberings reduced and also preserve the number of minimal and positive degrees in their semilattice. It is shown how to use these reductions to simplify some constructions of specific semilattices. Furthermore, it is shown that for the basic types of numberings, one can reduce the left-r.e. numberings to the r.e. numberings and the k -r.e. numberings to the (k + 1) -r.e. numberings; all further reductions are obtained by concatenating these reductions. [ABSTRACT FROM AUTHOR]

Compactness is one of the core notions of analysis: it connects local properties to global ones and makes limits well-behaved. We study the computational properties of the compactness of Cantor space 2 N for uncountable covers. The most basic question is: how hard is it to compute a finite sub-cover from such a cover of 2 N ? Another natural question is: how hard is it to compute a sequence that covers 2 N minus a measure zero set from such a cover ? The special and weak fan functionals respectively compute such finite sub-covers and sequences. In this paper, we establish the connection between these new fan functionals on one hand, and various well-known comprehension axioms on the other hand, including arithmetical comprehension, transfinite recursion, and the Suslin functional. In the spirit of Reverse Mathematics , we also analyse the logical strength of compactness in Nonstandard Analysis. Perhaps surprisingly, the results in the latter mirror (often perfectly) the computational properties of the special and weak fan functionals. In particular, we show that compactness (nonstandard or otherwise) readily brings us to the outer edges of Reverse Mathematics (namely Π 2 1 - CA 0), and even into Schweber's higher-order framework (namely Σ 1 2 -separation). [ABSTRACT FROM AUTHOR]