TY - BOOK ID - 67031438 TI - Proofs and computations AU - Schwichtenberg, Helmut AU - Wainer, Stanley S. PY - 2012 SN - 9780521517690 9781139220200 1139220209 9786613579836 6613579831 9781139223638 1139223631 9781139031905 1139031902 9781139217101 1139217100 0521517699 1107224284 1280484853 1139221922 1139214039 PB - Cambridge: Cambridge university press, DB - UniCat KW - Computable functions KW - Proof theory KW - Computable functions. KW - Proof theory. KW - Logic, Symbolic and mathematical KW - Computability theory KW - Functions, Computable KW - Partial recursive functions KW - Recursive functions, Partial KW - Constructive mathematics KW - Decidability (Mathematical logic) UR - https://www.unicat.be/uniCat?func=search&query=sysid:67031438 AB - Driven by the question, "What is the computational content of a (formal) proof ?", this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Π11-CA0. Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG. Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic. ER -