Provability, Computability and Reflection.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting (...) framework is intended as a setting for the logical and categorical study of relative computability. (shrink)

We study the fragment of Peano arithmetic formalizing the induction principle for the class of decidable predicates, $I\Delta_1$ . We show that $I\Delta_1$ is independent from the set of all true arithmetical $\Pi_2-sentences$ . Moreover, we establish the connections between this theory and some classes of oracle computable functions with restrictions on the allowed number of queries. We also obtain some conservation and independence results for parameter free and inference rule forms of $\Delta_1-induction$ . An open problem formulated by J. (...) Paris is whether $I\Delta_1$ proves the corresponding least element principle for decidable predicates, $L\Delta_1$ (or, equivalently. the $\Sigma_1-collection$ principle $B\Sigma_1$ ). We reduce this question to a purely computation-theoretic one. (shrink)

Computability and Logic has become a classic because of its accessibility to students without a mathematical background and because it covers not simply the staple topics of an intermediate logic course, such as Godel’s incompleteness theorems, but also a large number of optional topics, from Turing’s theory of computability to Ramsey’s theorem. Including a selection of exercises, adjusted for this edition, at the end of each chapter, it offers a new and simpler treatment of the representability of recursive functions, a (...) traditional stumbling block for students on the way to the Godel incompleteness theorems. (shrink)

The theme of this book is formed by a pair of concepts: the concept of formal language as carrier of the precise expression of meaning, facts and problems, and the concept of algorithm or calculus, i.e. a formally operating procedure for the solution of precisely described questions and problems. The book is a unified introduction to the modern theory of these concepts, to the way in which they developed first in mathematical logic and computability theory and later in automata theory, (...) and to the theory of formal languages and complexity theory. Apart from considering the fundamental themes and classical aspects of these areas, the subject matter has been selected to give priority throughout to the new aspects of traditional questions, results and methods which have developed from the needs or knowledge of computer science and particularly of complexity theory. It is both a textbook for introductory courses in the above-mentioned disciplines as well as a monograph in which further results of new research are systematically presented and where an attempt is made to make explicit the connections and analogies between a variety of concepts and constructions. (shrink)

The fundamental ideas concerning computation and recursion naturally find their place at the interface between logic and theoretical computer science. The contributions in this book, by leaders in the field, provide a picture of current ideas and methods in the ongoing investigations into the pure mathematical foundations of computability theory. The topics range over computable functions, enumerable sets, degree structures, complexity, subrecursiveness, domains and inductive inference. A number of the articles contain introductory and background material which it is hoped will (...) make this volume an invaluable resource for specialists and non-specialists alike. (shrink)

Recent new paradigms of computation, based on biological and physical models, address in a radically new way questions of efficiency and challenge assumptions ...

Together, Models and Computability and its sister volume Sets and Proofs will provide readers with a comprehensive guide to the current state of mathematical logic. All the authors are leaders in their fields and are drawn from the invited speakers at 'Logic Colloquium '97' (the major international meeting of the Association of Symbolic Logic). It is expected that the breadth and timeliness of these two volumes will prove an invaluable and unique resource for specialists, post-graduate researchers, and the informed and (...) interested nonspecialist. (shrink)

Topologists Nabutovsky and Weinberger discovered how to embed computably enumerable (c.e.) sets into the geometry of Riemannian metrics modulo diffeomorphisms. They used the complexity of the settling times of the c.e. sets to exhibit a much greater complexity of the depth and density of local minima for the diameter function than previously imagined. Their results depended on the existence of certain sequences of c.e. sets, constructed at their request by Csima and Soare, whose settling times had the necessary dominating properties. (...) Although these computability results had been announced earlier, their proofs have been deferred until this paper. Computably enumerable sets have long been used to prove undecidability of mathematical problems such as the word problem for groups and Hilbert's Tenth Problem. However, this example by Nabutovsky and Weinberger is perhaps the first example of the use of c.e. sets to demonstrate specific mathematical or geometric complexity of a mathematical structure such as the depth and distribution of local minima. (shrink)

What can computers do in principle? What are their inherent theoretical limitations? These are questions to which computer scientists must address themselves. The theoretical framework which enables such questions to be answered has been developed over the last fifty years from the idea of a computable function: intuitively a function whose values can be calculated in an effective or automatic way. This book is an introduction to computability theory (or recursion theory as it is traditionally known to mathematicians). Dr Cutland (...) begins with a mathematical characterisation of computable functions using a simple idealised computer (a register machine); after some comparison with other characterisations, he develops the mathematical theory, including a full discussion of non-computability and undecidability, and the theory of recursive and recursively enumerable sets. The later chapters provide an introduction to more advanced topics such as Gildel's incompleteness theorem, degrees of unsolvability, the Recursion theorems and the theory of complexity of computation. Computability is thus a branch of mathematics which is of relevance also to computer scientists and philosophers. Mathematics students with no prior knowledge of the subject and computer science students who wish to supplement their practical expertise with some theoretical background will find this book of use and interest. (shrink)

Classic text considersgeneral theory of computability, computable functions, operations on computable functions, Turing machines self-applied, unsolvable decision problems, applications of general theory, mathematical logic, Kleene hierarchy, computable functionals, classification of unsolvable decision problems and more.

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)

In recent years it has been convincingly argued that the Church-Turing thesis concerns the bounds of human computability: The thesis was presented and justified as formally delineating the class of functions that can be computed by a human carrying out an algorithm. Thus the Thesis needs to be distinguished from the so-called Physical Church-Turing thesis (or Thesis M), according to which all physically computable functions are Turing computable. The latter is often claimed to be false, or, if true, contingently so. (...) On all accounts, though, thesis M is not easy to give counterexamples to, but it is never asked why—how come that a thesis that transfers a notion from the strictly human domain to the general physical domain just happens to be so difficult to falsify (or even to be true). In this paper I articulate this question and consider several tentative answers to it. (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;.

• What’s essential to Newcomb’s problem? 1. You must choose between two particular acts: A1 = you take just the opaque box; A2 = you take both boxes, where the two states of nature are: S 1 = there’s $1M in the opaque box, S2 = there’s $0 in the opaque box.

We propose the notion of partial recursiveness and strong partial recursiveness for fuzzy maps. We prove that a fuzzy map f is partial recursive if and only if it is computable by a Turing fuzzy machine and that f is strongly partial recursive and deterministic if and only if it is computable via a deterministic Turing fuzzy machine. This gives a simple and manageable tool to investigate about the properties of the fuzzy machines.

We investigate Turing's contributions to computability theory for real numbers and real functions presented in [22, 24, 26]. In particular, it is shown how two fundamental approaches to computable analysis, the so-called ‘Type-2 Theory of Effectivity' (TTE) and the ‘realRAM machine' model, have their foundations in Turing's work, in spite of the two incompatible notions of computability they involve. It is also shown, by contrast, how the modern conceptual tools provided by these two paradigms allow a systematic interpretation of Turing's (...) pioneering work in the subject. (shrink)

The chapters of this volume all have their own level of presentation. The topics have been chosen based on the active research interest associated with them. Since the interest in some topics is older than that in others, some presentations contain fundamental definitions and basic results while others relate very little of the elementary theory behind them and aim directly toward an exposition of advanced results. Presentations of the latter sort are in some cases restricted to a short survey of (...) recent results (due to the complexity of the methods and proofs themselves). Hence the variation in level of presentation from chapter to chapter only reflects the conceptual situation itself. One example of this is the collective efforts to develop an acceptable theory of computation on the real numbers. The last two decades has seen at least two new definitions of effective operations on the real numbers. (shrink)

In ‘Infinitism Regained’, Jeanne Peijnenburg argues for a version of infinitism wherein ‘beliefs may be justified by an infinite chain of reasons that can be actually completed’. I argue that Peijnenburg has not successfully argued for this claim, but rather has shown that certain infinite series can be computed.

It is well understood and appreciated that Gödel’s Incompleteness Theorems apply to sufficiently strong, formal deductive systems. In particular, the theorems apply to systems which are adequate for conventional number theory. Less well known is that there exist algorithms which can be applied to such a system to generate a gödel-sentence for that system. Although the generation of a sentence is not equivalent to proving its truth, the present paper argues that the existence of these algorithms, when conjoined with Gödel’s (...) results and accepted theorems of recursion theory, does provide the basis for an apparent paradox. The difficulty arises when such an algorithm is embedded within a computer program of sufficient arithmetic power. The required computer program (an AI system) is described herein, and the paradox is derived. A solution to the paradox is proposed, which, it is argued, illuminates the truth status of axioms in formal models of programs and Turing machines. (shrink)

The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability theory, and (...) model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course. (shrink)

A true Turing machine (TM) requires an infinitely long paper tape. Thus a TM can be housed in the infinite world of Newtonian spacetime (the spacetime of common sense), but not necessarily in our world, because our world-at least according to our best spacetime theory, general relativity-may be finite. All the same, one can argue for the "existence" of a TM on the basis that there is no such housing problem in some other relativistic worlds that are similar ("close") to (...) our world. But curiously enough-and this is the main point of this paper-some of these close worlds have a special spacetime structure that allows TMs to perform certain Turing unsolvable tasks. For example, in one kind of spacetime a TM can be used to solve first-order predicate logic and the halting problem. And in a more complicated spacetime, TMs can be used to decide arithmetic. These new computers serve to show that Church's thesis is a thoroughly contingent claim. Moreover, since these new computers share the fundamental properties of a TM in ordinary operation (e.g. intuitive, finitely programmed, limited in computational capability), a computability theory based on these non-Turing computers is no less worthy of investigation than orthodox computability theory. Some ideas about this new mathematical theory are given. (shrink)

It has been argued that neural networks and other forms of analog computation may transcend the limits of Turing-machine computation; proofs have been offered on both sides, subject to differing assumptions. In this article I argue that the important comparisons between the two models of computation are not so much mathematical as epistemological. The Turing-machine model makes assumptions about information representation and processing that are badly matched to the realities of natural computation (information representation and processing in or inspired by (...) natural systems). This points to the need for new models of computation addressing issues orthogonal to those that have occupied the traditional theory of computation. (shrink)

We show that there is a structure of countably infinite signature with $P = N_{2}P$ and a structure of finite signature with $P = N_{1}P$ and $N_{1}P \neq N_{2}P$ . We give a further example of a structure of finite signature with $P \neq N_{1}P$ and $N_{1}P \neq N_{2}P$ . Together with a result from [10] this implies that for each possibility of P versus NP over structures there is an example of countably infinite signature. Then we show that for (...) some finite ℒ the class of ℒ-structures with $P = N_{1}P$ is not closed under ultraproducts and obtain as corollaries that this class is not $\delta$ -elementary and that the class of ᵍ-structures with $P \neq N_{1}P$ is not elementary. Finally we prove that for all f dominating all polynomials there is a structure of finite signature with the following properties: $P \neq N_{1}P$ . $N_{1}P \neq N_{2}P$ , the levels $N_{2}TIME(n^{i})$ of $N_{2}P$ and the levels $N_{1}TIME(n^{i})$ of $N_{1}P$ are different for different i, indeed $DTIME(n^{i'}) \nsubseteq N_{2}TIME(n^{i})$ if $i' \textgreater i$ ; $DTIME(f) \nsubseteq N_{2}P$ , and $N_{2}P \nsubseteq DEC$ . DEC is the class of recognizable sets with recognizable complements. So this is an example where the internal structure of $N_{2}P$ is analyzed in a more detailed way. In our proofs we use methods in the style of classical computability theory to construct structures except for one use of ultraproducts. (shrink)

Daniele Mundici and Wilfred Sieg. Computability Theory.

We review some of the history of the computability theory of functionals of higher types, and we will demonstrate how contributions from logic and theoretical computer science have shaped this still active subject.

We show that to every recursive total continuous functional Φ there is a PCF-definable representative Ψ of Φ in the hierarchy of partial continuous functionals, where PCF is Plotkin's programming language for computable functionals. PCF-definable is equivalent to Kleene's S1-S9-computable over the partial continuous functionals.

Abstract State Machines (ASMs) provide a formal method for transparent design and specification of complex dynamic systems. They combine advantages of informal and formal methods. Applications of this method motivate a number of computability and decidability problems connected to ASMs. Such problems result for example from the area of verifying properties of ASMs. Their high expressive power leads rather directly to undecidability respectively uncomputability results for most interesting problems in the case of unrestricted ASMs. Consequently, it is rather natural to (...) ask whether there exist expressive classes of ASMs for which we can prove positive decidability and computability results. In this work, we introduce such a class of ASMs. The concept is similar to the one of the guarded fragment of first-order logic. We analyze the expressive power of this class and prove that it is stronger than Datalog LITE and the guarded fragment of first-order fixed point logic. Some decidability and computability results have been proven in earlier works. (shrink)

Church's thesis asserts that a number-theoretic function is intuitively computable if and only if it is recursive. A related thesis asserts that Turing's work yields a conceptual analysis of the intuitive notion of numerical computability. I endorse Church's thesis, but I argue against the related thesis. I argue that purported conceptual analyses based upon Turing's work involve a subtle but persistent circularity. Turing machines manipulate syntactic entities. To specify which number-theoretic function a Turing machine computes, we must correlate these syntactic (...) entities with numbers. I argue that, in providing this correlation, we must demand that the correlation itself be computable. Otherwise, the Turing machine will compute uncomputable functions. But if we presuppose the intuitive notion of a computable relation between syntactic entities and numbers, then our analysis of computability is circular. (shrink)

The purpose of this article is to examine aspects of the development of the concept and theory of computability through the theory of recursive functions. Following a brief introduction, Section 2 is devoted to the presuppositions of computability. It focuses on certain concepts, beliefs and theorems necessary for a general property of computability to be formulated and developed into a mathematical theory. The following two sections concern situations in which the presuppositions were realized and the theory of computability was developed. (...) It is suggested in Section 3 that a central item was the problem of generalizing Gödel's incompleteness theorem. It is shown that this involved both the characterization of recursiveness and the attempt to clarify and formulate the notion of an effective process as it relates to the syntax of deductive systems. Section 4 concerns the decision problems which grew from the Hilbert program. Section 5 is devoted to the development of an informal' technique in the theory of computability often called ?argument by Church's thesis? (shrink)

Church's and Turing's theses dogmatically assert that an informal notion of effective calculability is adequately captured by a particular mathematical concept of computability. I present an analysis of calculability that is embedded in a rich historical and philosophical context, leads to precise concepts, but dispenses with theses.To investigate effective calculability is to analyze symbolic processes that can in principle be carried out by calculators. This is a philosophical lesson we owe to Turing. Drawing on that lesson and recasting work of (...) Gandy, I formulate boundedness and locality conditions for two types of calculators, namely, human computing agents and mechanical computing devices (discrete machines). The distinctive feature of the latter is that they can carry out parallel computations. The analysis leads to axioms for discrete dynamical systems (representing human and machine computations) and allows the reduction of models of these axioms to Turing machines. Cellular automata and a variety of artificial neural nets can be shown to satisfy the axioms for machine computations. (shrink)

criticism defend the idea that an individual reader's understanding of a text can be a factor in determining the meaning of what is written in that text, and hence must play a part in determining the very identity conditions of works of literary art. We examine some accounts that have been given of the type of readerly ‘competence’ that a reader must have in order for her responses to a text to play this sort of constitutive role. We argue that (...) the analogy drawn by Stanley Fish and Jonathan Culler between literary and linguistic competence is philosophically flawed and explanatorily unfruitful, and that a better way of understanding the notion of literary competence can be constructed by appeal to some limitation results in formal logic and computability theory. (shrink)

The Kripke-completeness and incompleteness of some intermediate predicate logics is established. In particular, we obtain a Kripke-incomplete logic (H* +A+D+K) where H* is the intuitionistic predicate calculus, A is a disjunction-free propositional formula, D = x(P(x) V Q) xP(x) V Q, K = ¬¬x(P(x) V ¬P(x)) (the negative answer to a question of T. Shimura).

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)

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)