Saul Kripke once noted that there is a tight connection between computation and de re knowledge of whatever the computation acts upon. For example, the Euclidean algorithm can produce knowledge of which number is the greatest common divisor of two numbers. Arguably, algorithms operate directly on syntactic items, such as strings, and on numbers and the like only via how the numbers are represented. So we broach matters of notation. The purpose of this article is to explore the relationship between (...) the notations acceptable for computation, the usual idealizations involved in theories of computability, flowing from Alan Turing’s monumental work, and de re propositional attitudes toward numbers and other mathematical objects. (shrink)

We consider the informal concept of "computability" or "effective calculability" and two of the formalisms commonly used to define it, "(Turing) computability" and "(general) recursiveness". We consider their origin, exact technical definition, concepts, history, general English meanings, how they became fixed in their present roles, how they were first and are now used, their impact on nonspecialists, how their use will affect the future content of the subject of computability theory, and its connection to other related areas. (...) After a careful historical and conceptual analysis of computability and recursion we make several recommendations in section §7 about preserving the intensional differences between the concepts of "computability" and "recursion." Specifically we recommend that: the term "recursive" should no longer carry the additional meaning of "computable" or "decidable;" functions defined using Turing machines, register machines, or their variants should be called "computable" rather than "recursive;" we should distinguish the intensional difference between Church's Thesis and Turing's Thesis, and use the latter particularly in dealing with mechanistic questions; the name of the subject should be "Computability Theory" or simply Computability rather than "Recursive Function Theory.". (shrink)

One recursively enumerable real α dominates another one β if there are nondecreasing recursive sequences of rational numbers (a[n] : n ∈ ω) approximating α and (b[n] : n ∈ ω) approximating β and a positive constant C such that for all n, C(α − a[n]) ≥ (β − b[n]). See [R. M. Solovay, Draft of a Paper (or Series of Papers) on Chaitin’s Work, manuscript, IBM Thomas J. Watson Research Center, Yorktown Heights, NY, 1974, p. 215] and [G. J. (...) Chaitin, IBM J. Res. Develop., 21 (1977), pp. 350–359]. We show that every recursively enumerable random real dominates all other recursively enumerable reals. We conclude that the recursively enumerable random reals are exactly the Ω-numbers [G. J. Chaitin, IBM J. Res. Develop., 21 (1977), pp. 350–359]. Second, we show that the sets in a universal Martin-Lof test for randomness have random measure, and every recursively enumerable random number is the sum of the measures represented in a universal Martin-Lof test. (shrink)

We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is ε X ", and (2) "If X is a well-ordering, then so is φ(α, X)", where α is a fixed computable ordinal and φ represents the two-placed Veblen function. For the former statement, we show that ω iterations of the Turing jump are necessary in the proof and that the statement is equivalent to ${\mathrm{A}\mathrm{C}\mathrm{A}}_{0}^{+}$ over RCA₀. To prove (...) the latter statement we need to use ω α iterations of the Turing jump, and we show that the statement is equivalent to ${\mathrm{\Pi }}_{{\mathrm{\omega }}^{\mathrm{\alpha }}}^{0}{-\mathrm{C}\mathrm{A}}_{0}$ . Our proofs are purely computability-theoretic. We also give a new proof of a result of Friedman: the statement "if x is a well-ordering, then so is φ(x, 0)" is equivalent to ATR₀ over RCA₀. (shrink)

Many philosophers contend that Turing’s work provides a conceptual analysis of numerical computability. In (Rescorla, 2007), I dissented. I argued that the problem of deviant notations stymies existing attempts at conceptual analysis. Copeland and Proudfoot respond to my critique. I argue that their putative solution does not succeed. We are still awaiting a genuine conceptual analysis.

In the last five years there have been a number of results about the computable content of the prime, saturated, or homogeneous models of a complete decidable theory T in the spirit of Vaught's "Denumerable models of complete theories" combined with computability methods for degrees d ≤ 0′. First we recast older results by Goncharov, Peretyat'kin, and Millar in a more modern framework which we then apply. Then we survey recent results by Lange, "The degree spectra of homogeneous models," (...) which generalize the older results and which include positive results on when a certain homogeneous model of T has an isomorphic copy of a given Turing degree. We then survey Lange's "A characterization of the 0-basis homogeneous bounding degrees" for negative results about when does not have such copies, generalizing negative results by Goncharov, Peretyat'kin, and Millar. Finally, we explain recent results by Csima, Harizanov, Hirschfeldt, and Soare, "Bounding homogeneous models," about degrees d that are homogeneous bounding and explain their relation to the PA degrees. (shrink)

In this paper, the issues of computability and constructivity in the mathematics of physics are discussed. The sorts of questions to be addressed are those which might be expressed, roughly, as: Are the mathematical foundations of our current theories unavoidably non-constructive: or, Are the laws of physics computable?

This book constitutes the strictly refereed post-workshop proceedings of the 11th International Workshop on Computer Science Logic, CSL '97, held as the 1997 Annual Conference of the European Association on Computer Science Logic, EACSL, in Aarhus, Denmark, in August 1997. The volume presents 26 revised full papers selected after two rounds of refereeing from initially 92 submissions; also included are four invited papers. The book addresses all current aspects of computer science logics and its applications and thus presents the state (...) of the art in the area. (shrink)

Machine generated contents note: 1. The Computability Concept;2. General Recursive Functions;3. Programs and Machines;4. Recursive Enumerability;5. Connections to Logic;6. Degrees of Unsolvability;7. Polynomial-Time Computability;Appendix: Mathspeak;Appendix: Countability;Appendix: Decadic Notation;.

Several notions of computability-theoretic reducibility between [Formula: see text] principles have been studied. This paper contributes to the program of analyzing the behavior of versions of Ramsey’s Theorem and related principles under these notions. Among other results, we show that for each [Formula: see text], there is an instance of RT[Formula: see text] all of whose solutions have PA degree over [Formula: see text] and use this to show that König’s Lemma lies strictly between RT[Formula: see text] and RT[Formula: (...) see text] under one of these notions. We also answer two questions raised by Dorais, Dzhafarov, Hirst, Mileti, and Shafer on comparing versions of Ramsey’s Theorem and of the Thin Set Theorem with the same exponent but different numbers of colors. Still on the topic of the effect of the number of colors on the computable aspects of Ramsey-theoretic properties, we show that for each [Formula: see text], there is an [Formula: see text]-coloring [Formula: see text] of [Formula: see text] such that every [Formula: see text]-coloring of [Formula: see text] has an infinite homogeneous set that does not compute any infinite homogeneous set for [Formula: see text], and connect this result with the notion of infinite information reducibility introduced by Dzhafarov and Igusa. Next, we introduce and study a new notion that provides a uniform version of the idea of implication with respect to [Formula: see text]-models of RCA0, and related notions that allow us to count how many applications of a principle [Formula: see text] are needed to reduce another principle to [Formula: see text]. Finally, we fill in a gap in the proof of Theorem 12.2 in Cholak, Jockusch, and Slaman. (shrink)

Although Kurt Gödel does not figure prominently in the history of computabilty theory, he exerted a significant influence on some of the founders of the field, both through his published work and through personal interaction. In particular, Gödel’s 1931 paper on incompleteness and the methods developed therein were important for the early development of recursive function theory and the lambda calculus at the hands of Church, Kleene, and Rosser. Church and his students studied Gödel 1931, and Gödel taught a seminar (...) at Princeton in 1934. Seen in the historical context, Gödel was an important catalyst for the emergence of computability theory in the mid 1930s. (shrink)

We study the computational content of various theorems with reverse mathematical strength around Arithmetical Transfinite Recursion (ATR_0) from the point of view of computability-theoretic reducibilities, in particular Weihrauch reducibility. Our main result states that it is equally hard to construct an embedding between two given well-orderings, as it is to construct a Turing jump hierarchy on a given well-ordering. This answers a question of Marcone. We obtain a similar result for Fraïssé's conjecture restricted to well-orderings.

The study of ergodic theorems from the viewpoint of computable analysis is a rich field of investigation. Interactions between algorithmic randomness, computability theory and ergodic theory have recently been examined by several authors. It has been observed that ergodic measures have better computability properties than non-ergodic ones. In a previous paper we studied the extent to which non-ergodic measures inherit the computability properties of ergodic ones, and introduced the notion of an effectively decomposable measure. We asked the (...) following question: if the ergodic decomposition of a stationary measure is finite, is this decomposition effective? In this paper we answer the question in the negative. (shrink)

Which function is computed by a Turing machine will depend on how the symbols it manipulates are interpreted. Further, by invoking bizarre systems of notation it is easy to define Turing machines that compute textbook examples of uncomputable functions, such as the solution to the decision problem for first-order logic. Thus, the distinction between computable and uncomputable functions depends on the system of notation used. This raises the question: which systems of notation are the relevant ones for determining whether a (...) function is computable? These are the acceptable notations. I argue for a use criterion of acceptability: the acceptable notations for a domain of objects D\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal {D}}$$\end{document} are the notations that we can use for the usual D\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal {D}}$$\end{document}-activities. Acceptable notations for natural numbers are ones that we can count with. Acceptable notations for logical formulas are the ones that we can use in inference and logical analysis. And so on. This criterion makes computability a relative notion—whether a function is computable depends on which notations are acceptable, which is relative to our interests and abilities. I argue that this is not a problem, however, since there is independent reason for taking the extension of computable function to be relative to contingent facts. Similarly, the fact that the use criterion makes a mathematical distinction depend on practical concerns is also not a problem because it dovetails with similar phenomena in other areas of computability theory, namely the roles of notation in computation over real numbers and of Extended Church’s Thesis in complexity theory. (shrink)

We study computable Polish spaces and Polish groups up to homeomorphism. We prove a natural effective analogy of Stone duality, and we also develop an effective definability technique which works up to homeomorphism. As an application, we show that there is a $\Delta ^0_2$ Polish space not homeomorphic to a computable one. We apply our techniques to build, for any computable ordinal $\alpha $, an effectively closed set not homeomorphic to any $0^{}$-computable Polish space; this answers a question of Nies. (...) We also prove analogous results for compact Polish groups and locally path-connected spaces. (shrink)

This work is an attempt to lay foundations for a theory of interactive computation and bring logic and theory of computing closer together. It semantically introduces a logic of computability and sets a program for studying various aspects of that logic. The intuitive notion of computational problems is formalized as a certain new, procedural-rule-free sort of games between the machine and the environment, and computability is understood as existence of an interactive Turing machine that wins the game against (...) any possible environment. The formalism used as a specification language for computational problems, called the universal language, is a non-disjoint union of the formalisms of classical, intuitionistic and linear logics, with logical operators interpreted as certain—most basic and natural—operations on problems. Validity of a formula is understood as being “always computable”, and the set of all valid formulas is called the universal logic. The name “universal” is related to the potential of this logic to integrate, on the basis of one semantics, classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. In particular, the classical notion of truth turns out to be nothing but computability restricted to the formulas of the classical fragment of the universal language, which makes classical logic a natural syntactic fragment of the universal logic. The same appears to be the case for intuitionistic and linear logics . Unlike classical logic, these two do not have a good concept of truth, and the notion of computability restricted to the corresponding two fragments of the universal language, based on the intuitions that it formalizes, can well qualify as “intuitionistic truth” and “linear-logic truth”. The paper also provides illustrations of potential applications of the universal logic in knowledgebase, resourcebase and planning systems, as well as constructive applied theories. The author has tried to make this article easy to read. It is fully self-contained and can be understood without any specialized knowledge of any particular subfield of logic or computer science. (shrink)

It is time for a new paper about open questions in the currently very active area of randomness and computability. Ambos-Spies and Kučera presented such a paper in 1999 [1]. All the question in it have been solved, except for one: is KL-randomness different from Martin-Löf randomness? This question is discussed in Section 6.Not all the questions are necessarily hard—some simply have not been tried seriously. When we think a question is a major one, and therefore likely to be (...) hard, we indicate this by the symbol ▶, the criterion being that it is of considerable interest and has been tried by a number of researchers. Some questions are close contenders here; these are marked by ▷. With few exceptions, the questions are precise. They mostly have a yes/no answer. However, there are often more general questions of an intuitive or even philosophical nature behind. We give an outline, indicating the more general questions.All sets will be sets of natural numbers, unless otherwise stated. These sets are identified with infinite strings over {0, 1}. Other terms used in the literature are sequence and real. (shrink)

I develop a theory of counterfactuals about relative computability, i.e. counterfactuals such as 'If the validity problem were algorithmically decidable, then the halting problem would also be algorithmically decidable,' which is true, and 'If the validity problem were algorithmically decidable, then arithmetical truth would also be algorithmically decidable,' which is false. These counterfactuals are counterpossibles, i.e. they have metaphysically impossible antecedents. They thus pose a challenge to the orthodoxy about counterfactuals, which would treat them as uniformly true. What’s more, (...) I argue that these counterpossibles don’t just appear in the periphery of relative computability theory but instead they play an ineliminable role in the development of the theory. Finally, I present and discuss a model theory for these counterfactuals that is a straightforward extension of the familiar comparative similarity models. (shrink)

This paper presents a soundness and completeness proof for propositional intuitionistic calculus with respect to the semantics of computability logic. The latter interprets formulas as interactive computational problems, formalized as games between a machine and its environment. Intuitionistic implication is understood as algorithmic reduction in the weakest possible — and hence most natural — sense, disjunction and conjunction as deterministic-choice combinations of problems , and “absurd” as a computational problem of universal strength.

Computability logic (CL) is a recently launched program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic has more traditionally been. Formulas in it represent computational problems, "truth" means existence of an algorithmic solution, and proofs encode such solutions. Within the line of research devoted to finding axiomatizations for ever more expressive fragments of CL, the present paper introduces a new deductive system CL12 and proves its soundness and (...) completeness with respect to the semantics of CL. Conservatively extending classical predicate calculus and offering considerable additional expressive and deductive power, CL12 presents a reasonable, computationally meaningful, constructive alternative to classical logic as a basis for applied theories. To obtain a model example of such theories, this paper rebuilds the traditional, classical-logic-based Peano arithmetic into a computability-logic-based counterpart. Among the purposes of the present contribution is to provide a starting point for what, as the author wishes to hope, might become a new line of research with a potential of interesting findings—an exploration of the presumably quite unusual metatheory of CL-based arithmetic and other CL-based applied systems. (shrink)

It is often helpful in metaphysics to reflect upon the principles that govern how existence claims are made in logic and mathematics. Consider, for example, the different ways in which mathematicians construct inductive definitions. In order to provide an inductive definition of a class of mathematical entities, one must first define a base class and then stipulate further conditions for inclusion by reference to the properties of members of the base class. These conditions can be deflationary, so that the target (...) class is a subclass of the base class, or inflationary, so that the base class is an important subclass of the target class. For example, in defining the set of well-formed sentences of first order logic, one can begin with the set of all possible strings and, in a deflationary manner, exclude the nonsentences. Or one can begin with the set of atomic formulae, and in an inflationary manner, build more complicated sentences out of the atomic formulae. (shrink)

The connections between mathematical logic and combinatorics have a rich history. This paper focuses on one aspect of this relationship: understanding the strength, measured using the tools of computability theory and reverse mathematics, of various partition theorems. To set the stage, recall two of the most fundamental combinatorial principles, König's Lemma and Ramsey's Theorem. We denote the set of natural numbers by ω and the set of finite sequences of natural numbers by ω<ω. We also identify each n ∈ (...) ω with its set of predecessors, so n = {0, 1, 2, …, n − 1}. (shrink)

A problem is a multivalued function from a set of instances to a set of solutions. We consider only instances and solutions coded by sets of integers. A problem admits preservation of some computability-theoretic weakness property if every computable instance of the problem admits a solution relative to which the property holds. For example, cone avoidance is the ability, given a noncomputable set A and a computable instance of a problem ${\mathsf {P}}$, to find a solution relative to which (...) A is still noncomputable.In this article, we compare relativized versions of computability-theoretic notions of preservation which have been studied in reverse mathematics, and prove that the ones which were not already separated by natural statements in the literature actually coincide. In particular, we prove that it is equivalent to admit avoidance of one cone, of $\omega $ cones, of one hyperimmunity or of one non- $\Sigma ^{0}_1$ definition. We also prove that the hierarchies of preservation of hyperimmunity and non- $\Sigma ^{0}_1$ definitions coincide. On the other hand, none of these notions coincide in a nonrelativized setting. (shrink)

Church's Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turing-computable numeric functions. The Abstract State Machine Theorem states that every classical algorithm is behaviorally equivalent to an abstract state machine. This theorem presupposes three natural postulates about algorithmic computation. Here, we show that augmenting those postulates with an additional requirement regarding basic operations gives a natural axiomatization of computability and a proof of (...) Church's Thesis, as Gödel and others suggested may be possible. In a similar way, but with a different set of basic operations, one can prove Turing's Thesis, characterizing the effective string functions, and--in particular--the effectively-computable functions on string representations of numbers. (shrink)

This paper shows that the basic logic induced by the parallel recurrence $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ of computability logic (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}},\hspace {-2pt}\mbox {\raisebox {0.12cm}{\@setfontsize \small {7}{8}$\vee$}\hspace {-3.6pt}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ) is a proper superset of the basic logic induced by the branching recurrence $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ (i.e., the one in the signature $\{\neg,$\wedge$,\vee,\mbox {\raisebox {-0.05cm}{$\circ$}\hspace (...) {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}},\mbox {\raisebox {0.12cm}{$\circ$}\hspace {-0.115cm}\raisebox {0.02cm}{\tiny $\mid$}\hspace {2pt}}\}$ ). The latter is known to be precisely captured by the cirquent calculus system CL15 , conjectured by Japaridze to remain sound—but not complete—with $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ instead of $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ . The present result is obtained by positively verifying that conjecture. A secondary result of the paper is showing that $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}$ is strictly weaker than $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}$ in the sense that, while $\mbox {\raisebox {-0.05cm}{$\circ$}\hspace {-0.11cm}\raisebox {3.1pt}{\tiny $\mid$}\hspace {2pt}}F$ logically implies $\hspace {-2pt}\mbox {\raisebox {-0.01pt}{\@setfontsize \small {7}{8}$\wedge$}\hspace {-3.55pt}\raisebox {4.5pt}{\tiny $\mid$}\hspace {2pt}}F$ , the reverse does not hold. (shrink)

The Lovász local lemma (LLL) is a technique from combinatorics for proving existential results. There are many different versions of the LLL. One of them, the lefthanded local lemma, is particularly well suited for applications to two player games. There are also constructive and computable versions of the LLL. The chief object of this thesis is to prove an effective version of the lefthanded local lemma and to apply it to effectivise constructions of non-repetitive sequences.The second goal of this thesis (...) is to categorize some classes of cohesive powers. We completely describe both the isomorphism types of cohesive powers of equivalence structures and injection structures, as well as clarify the relationship between these cohesive powers and their original structures. We also describe the finite condensation of cohesive powers of computable copies of the integers as a linear order by cohesive sets whose complement are computably enumerable.Finally, we investigate the possibility of decomposing problems in the Weihrauch degrees into a product of first order part and second order part. We give a preliminary result in this direction.Abstract prepared by Daniel Mourad.E-mail: daniel.mourad@uconn.eduURL: https://daniel-mourad.scholar.uconn.edu/wp-content/uploads/sites/2530/2023/06/ThesisFinalWithRevisio ns-2.pdf. (shrink)

Lattice representations are an important tool for computability theorists when they embed nondistributive lattices into degree-theoretic structures. In this expository paper, we present the basic definitions and results about lattice representations needed by computability theorists. We define lattice representations both from the lattice-theoretic and computability-theoretic points of view, give examples and show the connection between the two types of representations, discuss some of the known theorems on the existence of lattice representations that are of interest to (...) class='Hi'>computability theorists, and give a simple example of the use of lattice representations in an embedding result. (shrink)

This book presents a set of historical recollections on the work of Martin Davis and his role in advancing our understanding of the connections between logic, computing, and unsolvability. The individual contributions touch on most of the core aspects of Davis’ work and set it in a contemporary context. They analyse, discuss and develop many of the ideas and concepts that Davis put forward, including such issues as contemporary satisfiability solvers, essential unification, quantum computing and generalisations of Hilbert’s tenth problem. (...) The book starts out with a scientific autobiography by Davis, and ends with his responses to comments included in the contributions. In addition, it includes two previously unpublished original historical papers in which Davis and Putnam investigate the decidable and the undecidable side of Logic, as well as a full bibliography of Davis’ work. As a whole, this book shows how Davis’ scientific work lies at the intersection of computability, theoretical computer science, foundations of mathematics, and philosophy, and draws its unifying vision from his deep involvement in Logic. (shrink)

This paper constructs a cirquent calculus system and proves its soundness and completeness with respect to the semantics of computability logic. The logical vocabulary of the system consists of negation ${\neg}$ , parallel conjunction ${\wedge}$ , parallel disjunction ${\vee}$ , branching recurrence ⫰, and branching corecurrence ⫯. The article is published in two parts, with (the present) Part I containing preliminaries and a soundness proof, and (the forthcoming) Part II containing a completeness proof.

The identification of an informal concept of ‘effective calculability’ with a rigorous mathematical notion like ‘recursiveness’ or ‘Turing computability’ is still viewed as problematic, and I think rightly so. I analyze three different and conflicting perspectives Gödel articulated in the three decades from 1934 to 1964. The significant shifts in Gödel's position underline the difficulties of the methodological issues surrounding the Church-Turing Thesis.