Schwichtenberg H., Wainer S.S. Proofs and Computations

Cambridge University Press, 2012. — 482 p. — (Perspectives in Logic). — ISBN: 978-0-521-51769-0.This book is about the deep connections between proof theory and recursive function theory. Their interplay has continuously underpinned and motivated the more constructively orientated developments in mathematical logic ever since the pioneering days of Hilbert, Gӧdel, Church, Turing, Kleene, Ackermann, Gentzen, P´eter, Herbrand, Skolem, Malcev, Kolmogorov and others in the 1930s. They were all concerned in one way or another with the links between logic and computability. Gӧdel’s theorem utilized the logical representability of recursive functions in number theory; Herbrand’s theorem extracted explicit loop-free programs (sets of witnessing terms) from existential proofs in logic; Ackermann and Gentzen analysed the computational content of ε-reduction and cut-elimination in terms of transfinite recursion; Turing not only devised the classical machine-model of computation, but (what is less well known) already foresaw the potential of transfinite induction as a method for program verification; and of course the Herbrand–Gӧdel–Kleene equation calculus presented computability as a formal system of equational derivation (with call by value being modelled by a substitution rule which itself is a form of cut but at the level of terms).
That these two fields—proof and recursion—have developed side by side over the intervening seventy-five years so as to form now a cornerstone in the foundations of computer science, testifies to the power and importance of mathematical logic in transferring what was originally a body of philosophically inspired ideas and results, down to the frontiers of modern information technology. A glance through the contents of any good undergraduate text on the fundamentals of computing should lend conviction to this argument, but we hope also that some of the examples and applications in this book will support it further.
Our book is not about technology transfer however, but rather about a fundamental area of mathematical logic which underlies it. We would not presume to compete with classics in the field like Kleene’s [1952], Schütte’s [1960], Takeuti’s [1987], Girard’s [1987] or Troelstra and van Dalen’s [1988], but rather we aim to complement them and extend their range of proof-theoretic applications with a treatment of topics which reflect our own personal interests over many years and include some which have not previously been covered in textbook form. Our contribution could be seen as building on the books by Rose [1984] and Troelstra and Schwichtenberg [2000]. Thus the theory of proofs, recursions, provably recursive functions, their subrecursive hierarchy classifications, and the computational significance and application of these, will constitute the driving theme. The methods will be those now-classical ones of cut elimination, normalization, functional interpretations, program extraction and ordinal analyses, but restricted to the small-to-medium-sized range of mathematically significant proof systems between polynomial time arithmetic and (restricted) Π¹₁-comprehension or ID _∞. Within this range we hope to have something new to contribute. Beyond it, the outer limits of ordinal analysis and the emerging connections there with large cardinal theory are presently undergoing rapid and surprising development. Who knows where that will lead?—others are far better equipped to comment.Part I. Basic proof theory and computability
Logic
Recursion theory
Gӧdel’s theorems
Part II. Provable recursion in classical systems
The provably recursive functions of arithmetic
Accessible recursive functions, ID _∞ and Π¹₁-CA₀
Part III. Constructive logic and complexity
Computability in higher types
Extracting computational content from proofs
Linear two-sorted arithmetic