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)

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.

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?

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)

Several results about the game of cops and robbers on infinite graphs are analyzed from the perspective of computability theory. Computable robber-win graphs are constructed with the property that no computable robber strategy is a winning strategy, and such that for an arbitrary computable ordinal \, any winning strategy has complexity at least \}\). Symmetrically, computable cop-win graphs are constructed with the property that no computable cop strategy is a winning strategy. Locally finite infinite trees and graphs are explored. (...) The Turing computability of a binary relation used to classify cop-win graphs is studied, and the computational difficulty of determining the winner for locally finite computable graphs is discussed. (shrink)

This paper concerns “human symbolic output,” or strings of characters produced by humans in our various symbolic systems; e.g., sentences in a natural language, mathematical propositions, and so on. One can form a set that consists of all of the strings of characters that have been produced by at least one human up to any given moment in human history. We argue that at any particular moment in human history, even at moments in the distant future, this set is finite. (...) But then, given fundamental results in recursion theory, the set will also be recursive, recursively enumerable, axiomatizable, and could be the output of a Turing machine. We then argue that it is impossible to produce a string of symbols that humans could possibly produce but no Turing machine could. Moreover, we show that any given string of symbols that we could produce could also be the output of a Turing machine. Our arguments have implications for Hilbert’s sixth problem and the possibility of axiomatizing particular sciences, they undermine at least two distinct arguments against the possibility of Artificial Intelligence, and they entail that expert systems that are the equals of human experts are possible, and so at least one of the goals of Artificial Intelligence can be realized, at least in principle. (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;.

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)

Let M be a smooth, compact manifold of dimension n ≥ 5 and sectional curvature | K | ≤ 1. Let Met (M) = Riem(M)/Diff(M) be the space of Riemannian metrics on M modulo isometries. Nabutovsky and Weinberger studied the connected components of sublevel sets (and local minima) for certain functions on Met (M) such as the diameter. They showed that for every Turing machine T e , e ∈ ω, there is a sequence (uniformly effective in e) of homology (...) n-spheres {P k e } k ∈ ω which are also hypersurfaces, such that P k e is diffeomorphic to the standard n-sphere S n (denoted P k e ≈ diff S n ) iff T e halts on input k, and in this case the connected sum N k e =M ♯ P k e ≈ diff M , so N k e ∈ Met(M), and N k e is associated with a local minimum of the diameter function on Met(M) whose depth is roughly equal to the settling time σ e (k) of T e on inputs y i } ∈ ω of c.e. sets so that for all i the settling time of the associated Turing machine for A i dominates that for A i + 1 , even when the latter is composed with an arbitrary computable function. From this, Nabutovsky and Weinberger showed that the basins exhibit a "fractal" like behavior with extremely big basins, and very much smaller basins coming off them, and so on. This reveals what Nabutovsky and Weinberger describe in their paper on fractals as "the astonishing richness of the space of Riemannian metrics on a smooth manifold, up to reparametrization." From the point of view of logic and computability, the Nabutovsky-Weinberger results are especially interesting because: (1) they use c.e. sets to prove structural complexity of the geometry and topology, not merely undecidability results as in the word problem for groups, Hilbert's Tenth Problem, or most other applications; (2) they use nontrivial information about c.e. sets, the Soare sequence {A i } i ∈ ω above, not merely G öodel's c.e. noncomputable set K of the 1930's; and (3) without using computability theory there is no known proof that local minima exist even for simple manifolds like the torus T 5 (see §). (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)

According to information processing models of cognition, such as Chomsky's, the set of well-formed formulae of any natural language must be recursively enumerable (RE), otherwise, human learning language is impossible. I argue that there is nothing unlearnable about languages that are not RE. Insofar as natural languages turn out to be RE, this is to be accounted for on grounds of simplicity and not by appeal to the mistaken claim that nonRE languages are ruled out a priori. A consequence of (...) this position is that grammars will be somewhat depsychologized, and the acquisition of competence will come to be seen as a matter of degree - perhaps admitting of refinement and improvement without end. (shrink)

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)

Computability theory is the mathematical theory of algorithms, which explores the power and limitations of computation. Classical computability theory formalized the intuitive notion of an algorithm and provided a theoretical basis for digital computers. It also demonstrated the limitations of algorithms and showed that most sets of natural numbers and the problems they encode are not decidable (Turing computable). Important results of modern computability theory include the classification of the computational difficulty of sets and problems. Arithmetical and (...) hyperarithmetical hierarchies and the Turing degrees provide important measures of the level of such difficulty. There are uncountably many Turing degrees and they are partially ordered. These classifications are used in contemporary research to investigate the complexity of problems in modern computable mathematics, for example, regarding structures and their properties. (shrink)

We analyse Kreisel’s notion of human-effective computability. Like Kreisel, we relate this notion to a concept of informal provability, but we disagree with Kreisel about the precise way in which this is best done. The resulting two different ways of analysing human-effective computability give rise to two different variants of Church’s thesis. These are both investigated by relating them to transfinite progressions of formal theories in the sense of Feferman.

Computable model theory, also called effective or recursive model theory, studies algorithmic properties of mathematical structures, their relations, and isomorphisms. These properties can be described syntactically or semantically. One of the major tasks of computable model theory is to obtain, whenever possible, computability-theoretic versions of various classical model-theoretic notions and results. For example, in the 1950's, Fröhlich and Shepherdson realized that the concept of a computable function can make van der Waerden's intuitive notion of an explicit field precise. This (...) led to the notion of a computable structure. In 1960, Rabin proved that every computable field has a computable algebraic closure. However, not every classical result “effectivizes”. Unlike Vaught's theorem that no complete theory has exactly two nonisomorphic countable models, Millar's and Kudaibergenov's result establishes that there is a complete decidable theory that has exactly two nonisomorphic countable models with computable elementary diagrams. In the 1970's, Metakides and Nerode [58], [59] and Remmel [71], [72], [73] used more advanced methods of computability theory to investigate algorithmic properties of fields, vector spaces, and other mathematical structures. (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)

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)

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)

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)

It is shown that there exist subsets A and B of the real line which are recursively constructible such that A has a nonrecursive Hausdorff dimension and B has a recursive Hausdorff dimension but has a finite, nonrecursive Hausdorff measure. It is also shown that there exists a polynomial-time computable curve on the two-dimensional plane that has a nonrecursive Hausdorff dimension between 1 and 2. Computability of Julia sets of computable functions on the real line is investigated. It is (...) shown that there exists a polynomial-time computable function f on the real line whose Julia set is not recurisvely approximable. (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)

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)

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.

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)

Ranging from Alan Turing’s seminal 1936 paper to the latest work on Kolmogorov complexity and linear logic, this comprehensive new work clarifies the relationship between computability on the one hand and constructivity on the other. The authors argue that even though constructivists have largely shed Brouwer’s solipsistic attitude to logic, there remain points of disagreement to this day. Focusing on the growing pains computability experienced as it was forced to address the demands of rapidly expanding applications, the content (...) maps the developments following Turing’s ground-breaking linkage of computation and the machine, the resulting birth of complexity theory, the innovations of Kolmogorov complexity and resolving the dissonances between proof theoretical semantics and canonical proof feasibility. Finally, it explores one of the most fundamental questions concerning the interface between constructivity and computability: whether the theory of recursive functions is needed for a rigorous development of constructive mathematics. This volume contributes to the unity of science by overcoming disunities rather than offering an overarching framework. It posits that computability’s adoption of a classical, ontological point of view kept these imperatives separated. In studying the relationship between the two, it is a vital step forward in overcoming the disagreements and misunderstandings which stand in the way of a unifying view of logic. (shrink)

By language we understand a lower predicate calculus with identity and (perhaps) relation and function symbols. It is convenient to allow for more than one sort of variable. Now each individual constant (if there are any) is of a specified sort, the formal expressions R(t1, … tn), f(t1,…, tn) are well formed only if the terms t1, …, tn are of specified sorts determined by the relation symbol R and the function symbol f, and the term f(t1, …, tn) (if (...) well formed) is of a sort determined by f. We admit s = t as well formed, no matter what the sorts of s and t. (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.

We examine the reverse mathematics and computability theory of a form of Ramsey's theorem in which the linear n-tuples of a binary tree are colored.