Mathematical Logic

R.O. Gandy,C.E.M. Yates

• Editore: North Holland
• Anno: 2001
• ISBN:
  9780080535920
• Argomento: Informatik
• Categoria: Informatik Allgemein

Mathematical Logic is a collection of the works of one of the leading figures in 20th-century science. This collection of A.M. Turing's works is intended to include all his mature scientific writing, including a substantial quantity of unpublished material. His work in pure mathematics and mathematical logic extended considerably further; the work of his last years, on morphogenesis in plants, is also of the greatest originality and of permanent importance. This book is divided into three parts. The first part focuses on computability and ordinal logics and covers Turing's work between 1937 and 1938. The second part covers type theory; it provides a general introduction to Turing's work on type theory and covers his published and unpublished works between 1941 and 1948. Finally, the third part focuses on enigmas, mysteries, and loose ends. This concluding section of the book discusses Turing's Treatise on the Enigma, with excerpts from the Enigma Paper. It also delves into Turing's papers on programming and on minimum cost sequential analysis, featuring an excerpt from the unpublished manuscript. This book will be of interest to mathematicians, logicians, and computer scientists.

Part I

Computability and Ordinal Logics

Introduction to: Computability and Ordinal Logics

The historical introduction which opens Part I has been adapted from Feferman’s excellent paper [1988]: ‘Turing in the Land of O(z)’. The editor wishes to reiterate his gratitude to both Professor Feferman and Oxford University Press, the original publisher of the volume Herken [1988] which includes that paper.

Historical Introduction

Solomon Feferman

The story of how Turing came to write his papers on computable numbers and ordinal logics is contained in Andrew Hodges’ excellent biography, Alan Turing, The Enigma [1983]. It is retold in the following in condensed form, drawing extensively on Hodges for the relevant biographical details, as well as Kleene [1981] and Feferman [1986] for the development of logic and recursion theory in this period.

Paper 1. On Computable Numbers with an Application to the Entscheidungsproblem

The story begins with Turing’s major achievement, his work on computability, carried out in 1935-6 soon after he became a fellow of King’s College Cambridge at the age of 23. In the Spring of 1935 Turing attended a course on the Foundations of Mathematics given by the topologist M.H.A. Newman. Among other things, Newman explained Hubert’s problems concerning consistency, completeness and decidability of various axiomatic systems, as well as Gödel’s incompleteness results for sufficiently strong such systems. Turing had already been interested in mathematical logic but had been working primarily on other areas of mathematics, especially group theory. Newman’s course served to focus his interests in logic; in particular, Turing became intrigued by the Entscheidungsproblem (decision problem) for the first order predicate (or functional) calculus, and this came to dominate his thought from the summer of 1935 on (Hodges [1983], p. 94). In grappling with this problem he was led to conclude that the solution must be negative; but in order to demonstrate that, he would have to give an exact mathematical analysis of the informal concept of computability by a strictly mechanical process. This Turing achieved by mid-April 1936, when he delivered a draft of Paper 1 to Newman. At first Newman was skeptical of Turing’s analysis, thinking that nothing so straightforward in its basic conception as the Turing machines could be used to answer this outstanding problem. However, he finally satisfied himself that Turing’s notion did indeed provide the most general explanation of finite mechanical process, and he encouraged the paper’s publication.

Neither Newman nor Turing were then aware that the question of analyzing the notion of effective calculability had occupied the attention of Gödel, Herbrand, and especially Church since the early 1930’s. This side of the story is well-told in Kleene [1981], on the origins of recursive function theory.¹ Kleene was a Ph.D. student of Church from 1931 to 1933 (along with Rosser). Church was promoting a universal system for logic and mathematics in the framework of the lambda (λ)-symbolism for defining functions, and set Kleene the problem of developing the theory of positive integers in his formalism, using an identification of the integers with certain λ -terms. The initial steps were rather difficult (even the predecessor function posed a problem), but once the first hurdles were cleared, Kleene was able to show more and more number-theoretic functions definable by the conversion processes of λ -terms. But Church’s original system was shown before long (by Kleene and Rosser in 1934) to be inconsistent, and attention was then narrowed to a demonstrably consistent subsystem, which came to be called the λ -calculus.² The consistency of this subsystem was established by C...

Indice dei contenuti

• Cover image
• Title page
• Table of Contents
• Collected Works of A.M. Turing
• Copyright
• Dedication
• ACKNOWLEDGEMENTS
• PREFACE
• ALAN MATHISON TURING – CHRONOLOGY
• PREFACE TO THIS VOLUME
• Part I: Computability and Ordinal Logics
• Part II: Type Theory
• Part III: The Enigma, Mysteries and Loose Ends
• BIBLIOGRAPHY
• CONTENTS OF OTHER VOLUMES
• APPENDIX: MATTERS ARISING FROM EARLIER VOLUMES