General Recursion Theory Since their inception, the Perspectives in Logic and Lecture Notes in Logic series have published seminal works by leading logicians. Many of the original books in the series have been unavailable for years, but they are now in print once again. In this volume, the 10th publication in the Perspectives in Logic series, Jens Fenstad takes an axiomatic approach to present a unified and coherent account of the many and various parts of general recursion theory. The main core of the book gives an account of the general theory of computations. The author then moves on to show how computation theories connect with and unify other parts of general recursion theory. Some mathematical maturity is required of the reader, who is assumed to have some acquaintance with recursion theory. This book is ideal for a second course in the subject. JENS E. FENSTAD works in the Department of Mathematics at the University of Oslo. PERSPECTIVES IN LOGIC The Perspectives in Logic series publishes substantial, high-quality books whose central theme lies in any area or aspect of logic. Books that present new material not now available in book form are particularly welcome. The series ranges from introductory texts suitable for beginning graduate courses to specialized monographs at the frontiers of research. Each book offers an illuminating perspective for its intended audience. The series has its origins in the old Perspectives in Mathematical Logic series edited by the £2-Group for "Mathematische Logik" of the Heidelberger Akademie der Wissenschaften, whose beginnings date back to the 1960s. The Association for Symbolic Logic has assumed editorial responsibility for the series and changed its name to reflect its interest in books that span the full range of disciplines in which logic plays an important role. Arnold Beckmann, Managing Editor Department of Computer Science, Swansea University Editorial Board: Michael Benedikt Department of Computing Science, University of Oxford Elisabeth Bouscaren CNRS, Département de Mathématiques, Université Paris-Sud Steven A. Cook Computer Science Department, University of Toronto Michael Glanzberg Department of Philosophy, University of California Davis Antonio Montalban Department of Mathematics, University of Chicago Simon Thomas Department of Mathematics, Rutgers University For more information, see www.aslonline.org/books_perspectives.html PERSPECTIVES IN LOGIC General Recursion Theory An Axiomatic Approach JENS E. FENSTAD University of Oslo ASSOCIATION for symbolic logic CAMBRIDGE UNIVERSITY PRESS CAMBRIDGE UNIVERSITY PRESS University Printing House, Cambridge CB2 8BS, United Kingdom One Liberty Plaza, 20th Floor, New York, NY 10006, USA 477 Williamstown Road, Port Melbourne, VIC 3207, Australia 4843/24, 2nd Floor, Ansari Road, Daryaganj, Delhi - 110002, India 79 Anson Road, #06-04/06, Singapore 079906 Cambridge University Press is part of the University of Cambridge. It furthers the University's mission by disseminating knowledge in the pursuit of education, learning, and research at the highest international levels of excellence. www.cambridge.org Information on this title: www.cambridge.org/9781107168169 10.1017/9781316717073 First edition © 1980 Springer-Verlag Berlin Heidelberg This edition © 2016 Association for Symbolic Logic under license to Cambridge University Press. Association for Symbolic Logic Richard A. Shore, Publisher Department of Mathematics, Cornell University, Ithaca, NY 14853 http://www.aslonline.org This publication is in copyright. Subject to statutory exception and to the provisions of relevant collective licensing agreements, no reproduction of any part may take place without the written permission of Cambridge University Press. A catalogue record for this publication is available from the British Library. ISBN 978-1-107-16816-9 Hardback Cambridge University Press has no responsibility for the persistence or accuracy of URLs for external or third-party Internet Web sites referred to in this publication and does not guarantee that any content on such Web sites is, or will remain, accurate or appropriate. Preface to the Series On Perspectives. Mathematical logic arose from a concern with the nature and the limits of rational or mathematical thought, and from a desire to systematise the modes of its expression. The pioneering investigations were diverse and largely autonomous. As time passed, and more particularly in the last two decades, inter- connections between different lines of research and links with other branches of mathematics proliferated. The subject is now both rich and varied. It is the aim of the series to provide, as it were, maps or guides to this complex terrain. We shall not aim at encyclopaedic coverage; nor do we wish to prescribe, like Euclid, a definitive version of the elements of the subject. We are not committed to any particular philosophical programme. Nevertheless we have tried by critical discussion to ensure that each book represents a coherent line of thought; and that, by developing certain themes, // will be of greater interest than a mere assemblage of results and techniques. The books in the series differ in level: some are introductory some highly specialised. They also differ in scope: some offer a wide view of an area, others present a single line of thought. Each book is, at its own level, reasonably self con- tained. Although no book depends on another as prerequisite, we have encouraged authors to fit their book in with other planned volumes, sometimes deliberately seeking coverage of the same material from different points of view. We have tried to attain a reasonable degree of uniformity of notation and arrangement. However, the books in the series are written by individual authors, not by the group. Plans for books are discussed and argued about at length. Later, encouragement is given and revisions suggested. But it is the authors who do the work; if as we hope, the series proves of value, the credit will be theirs. History of the D-Group. During 1968 the idea of an integrated series of monographs on mathematical logic was first mooted. Various discussions led to a meeting at Oberwolfach in the spring of 1969. Here the founding members of the group (R. O. Gandy, A. Levy, G. H. Muller, G. E. Sacks, D. S. Scott) discussed the project in earnest and decided to go ahead with it. Professor F. K. Schmidt and Professor Hans Hermes gave us encouragement and support. Later Hans Hermes joined the group. To begin with all was fluid. How ambitious should we be ? Should we write the books ourselves ? How long would it take ? Plans for authorless books were promoted, savaged and scrapped. Gradually there emerged a form and a method. At the end of VI Preface to the Series an infinite discussion we found our name, and that of the series. We established our centre in Heidelberg. We agreed to meet twice a year together with authors, con- sultants and assistants, generally in Oberwolfach. We soon found the value of col- laboration: on the one hand the permanence of the founding group gave coherence to the over-all plans; on the other hand the stimulus of new contributors kept the project alive and flexible. Above all, we found how intensive discussion could modify the authors' ideas and our own. Often the battle ended with a detailed plan for a better book which the author was keen to write and which would indeed contribute a perspective. Acknowledgements. The confidence and support of Professor Martin Earner of the Mathematisches Forschungsinstitut at Oberwolfach and of Dr. Klaus Peters of Springer-Verlag made possible the first meeting and the preparation of a provisional plan. Encouraged by the Deutsche Forschungsgemeinschaft and the Heidelberger Akademie der Wissenschaften we submitted this plan to the Stiftung Volkswagenwerk where Dipl. Ing. Penschuck vetted our proposal; after careful investigation he became our adviser and advocate. We thank the Stiftung Volkswagenwerk for a generous grant (1970-73) which made our existence and our meetings possible. Since 1974 the work of the group has been supported by funds from the Heidelberg Academy; this was made possible by a special grant from the Kultusministerium von Baden-Wurttemberg (where Regierungsdirektor R. Goll was our counsellor). The success of the negotiations for this was largely due to the enthusiastic support of the former President of the Academy, Professor Wilhelm Doerr. We thank all those concerned. Finally we thank the Oberwolfach Institute, which provides just the right atmos- phere for our meetings, Drs. Ulrich Feigner and Klaus Glode for all their help, and our indefatigable secretary Elfriede Ihrig. Oberwolfach R. O. Gandy H. Hermes September 1975 A. Levy G. H. Muller G. E. Sacks D. S. Scott Author's Preface This book has developed over a number of years. The aim has been to give a unified and coherent account of the many and various parts of general recursion theory. I have not worked alone. The Recursion Theory Seminar in Oslo has for a number of years been a meeting place for an active group of younger people. Their work and enthusiasm have been an important part of the present project. I am happy to acknowledge my debts to Johan Moldestad, Dag Normann, Viggo Stoltenberg-Hansen and John Tucker. It has been a great joy for me to work together with them. But there are other debts to acknowledge. The Oslo group learned much of their recursion theory from Peter Hinman who spent the year 1971-72 in Oslo and Peter Aczel who was here for part of the year 1973. Robin Gandy, Yiannis Moschovakis and Gerald Sacks have also in many ways helped to shape our ideas about general recursion theory. I appreciate the invitation from the ^-group to write this book for their series. In particular, I would like to thank Gert Miiller for his friendship and helpfulness. Finally, I would like to thank Randi Moller for her expert typing of the manu- script, David Kierstead for his valuable help with the proof-reading, and the printers and publishers for the excellent production of this volume. Advice to the reader. The book is in principle self-contained, but we expect that any reader would have had some previous exposure to recursion theory, e.g. Rogers [136]. The books by Barwise [11], Hinman [61] and Moschovakis [115, 118] supplement our account, often from a different perspective. The exposition is organized around a main core which is reasonably complete. This is the general theory of computations. But the main core flowers into a number of side branches intended to show how computation theories connect with and unify other parts of general recursion theory. Here we are less complete and proofs may sometimes be more in the nature of a comment on the basic ideas involved. In the main body of the text and in an Epilogue we have tried to point beyond to open problems and areas of further research. Oslo, October 1979 Jens Erik Fenstad Table of Contents Pons Asinorum 1 Chapter 0. On the Choice of Correct Notions for the General Theory.... 3 0.1 Finite Algorithmic Procedures 3 0.2 FAP and Inductive Definability 7 0.3 FAP and Computation Theories 8 0.4 Platek's Thesis 11 0.5 Recent Developments in Inductive Definability 12 Part A. General Theory 17 Chapter 1. General Theory: Combinatorial Part 19 1.1 Basic Definitions 19 1.2 Some Computable Functions 22 1.3 Semicomputable Relations 25 1.4 Computing Over the Integers 27 1.5 Inductively Defined Theories 29 1.6 A Simple Representation Theorem 34 1.7 The First Recursion Theorem 38 Chapter 2. General Theory: Subcomputations 43 2.1 Subcomputations 43 2.2 Inductively Defined Theories 45 2.3 The First Recursion Theorem 48 2.4 Semicomputable Relations 50 2.5 Finiteness 52 2.6 Extension of Theories 54 2.7 Faithful Representation 57