# Proofs and Computations

- Length: 480 pages
- Edition: 1
- Language: English
- Publisher: Cambridge University Press
- Publication Date: 2012-01-16
- ISBN-10: 0521517699
- ISBN-13: 9780521517690
- Sales Rank: #1919906 (See Top 100 Books)

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.

### Table of Contents

Part 1: BASIC PROOF THEORY AND COMPUTABILITY

Chapter 1: LOGIC

Chapter 2: RECURSION THEORY

Chapter 3: G?DEL’S THEOREMS

Part 2: PROVABLE RECURSION IN CLASSICAL SYSTEMS

Chapter 4: THE PROVABLY RECURSIVE FUNCTIONS OF ARITHMETIC

Chapter 5: ACCESSIBLE RECURSIVE FUNCTIONS, ID<∞ AND Π11-CA0

Part 3: CONSTRUCTIVE LOGIC AND COMPLEXITY

Chapter 6: COMPUTABILITY IN HIGHER TYPES

Chapter 7: EXTRACTING COMPUTATIONAL CONTENT FROM PROOFS

Chapter 8: LINEAR TWO-SORTED ARITHMETIC

BIBLIOGRAPHY

INDEX