Handbook of proof theory (Q1264579)

[The articles of this volume will be reviewed individually.] From the preface: ``Proof theory is the study of proofs as formal objects and is concerned with a broad range of related topics. It is one of the central topics of mathematical logic and has applications in many areas of mathematics, philosophy, and computer science. Historically, proof theory was developed by mathematicians and philosophers as a formalization for mathematical reasoning; however, proof theory has gradually become increasingly important for computer science, and nowadays proof theory and theoretical computer science are recognized as being very closely connected. This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists in proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. We have attempted to include many of the central topics in proof theory; but have opted to have self-contained expository articles, rather than to have encyclopedic coverage. Thus, a number of important topics have been largely omitted, but with the advantage that the included material is covered in more detail and at greater depth. The chapters are arranged so that the two introductory articles come first; these are then followed by articles from the core classical areas of proof theory; finally the handbook ends with articles that deal with topics closely related to computer science.'' Indexed articles: \textit{Buss, Samuel R.}, An introduction to proof theory, 1-78 [Zbl 0912.03024] \textit{Buss, Samuel R.}, First-order proof theory of arithmetic, 79-147 [Zbl 0911.03029] \textit{Fairtlough, Matt; Wainer, Stanley S.}, Hierarchies of provably recursive functions, 149-207 [Zbl 0961.03053] \textit{Pohlers, Wolfram}, Subsystems of set theory and second order number theory, 209-335 [Zbl 0940.03066] \textit{Avigad, Jeremy; Feferman, Solomon}, Gödel's functional (``Dialectica'') interpretation, 337-405 [Zbl 0913.03053] \textit{Troelstra, A. S.}, Realizability, 407-473 [Zbl 0911.03031] \textit{Japaridze, Giorgi; de Jongh, Dick}, The logic of provability, 475-546 [Zbl 0915.03019] \textit{Pudlák, Pavel}, The lengths of proofs, 547-637 [Zbl 0920.03056] \textit{Jäger, Gerhard; Stärk, Robert F.}, A proof-theoretic framework for logic programming, 639-682 [Zbl 0916.03036] \textit{Constable, Robert L.}, Types in logic, mathematics and programming, 683-786 [Zbl 0914.03056]