Proofs and Computations

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