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éter, 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.