Handbook of Proof Theory

Cover ......Page 1
Preface ......Page 6
List of Contributors ......Page 7
Chapter I. An Introduction to Proof Theory (Samuel R. Buss) ......Page 9
1. Proof theory of propositional logic ......Page 11
1.1. Frege proof systems ......Page 13
1.2. The propositional sequent calculus ......Page 18
1.3. Propositional resolution refutations ......Page 26
2.1. Syntax and semantics ......Page 34
2.2. Hilbert-style proof systems ......Page 37
2.3. The first-order sequent calculus ......Page 39
2.4. Cut elimination ......Page 44
2.5. Herbrand’s theorem, interpolation and definability theorems ......Page 56
2.6. First-order logic and resolution refutations ......Page 67
3.1. Intuitionistic logic ......Page 72
3.2. Linear logic ......Page 78
References ......Page 82
Chapter II. First-Order Proof Theory of Arithmetic (Samuel R. Buss) ......Page 87
1. Fragments of arithmetic ......Page 89
1.1. Very weak fragments of arithmetic ......Page 90
1.2. Strong fragments of arithmetic ......Page 91
1.3. Fragments of bounded arithmetic ......Page 105
1.4. Sequent calculus formulations of arithmetic ......Page 117
2. Gödel incompleteness ......Page 120
2.1. Arithmetization of metamathematics ......Page 121
2.2. The Gödel incompleteness theorems ......Page 126
3.1. Witnessing theorems ......Page 130
3.2. Witnessing theorem for S^i_2 ......Page 135
3.3. Witnessing theorems and conservation results for T^i_2 ......Page 138
3.4. Relationships between BΣn and IΣn ......Page 142
4. Strong incompleteness theorems for IΔ0 + exp ......Page 145
References ......Page 151
Chapter III. Hierarchies of Provably Recursive Functions (Matt Fairtlough, Stanley S. Wainer) ......Page 157
1. Introduction ......Page 158
2. Structured ordinals and associated hierarchies ......Page 161
3. Complete ω-arithmetic ......Page 172
4. Provably recursive functions of PA ......Page 183
5. Independence results for PA ......Page 198
6. The “true” ordinal of PA ......Page 201
7. Theories with transfinite induction ......Page 207
References ......Page 211
Chapter IV. Subsystems of Set Theory and Second Order Number Theory (Wolfram Pohlers) ......Page 217
1.1. Ordinals ......Page 218
1.2. Partial models for axiom systems of set theory ......Page 223
1.3. Connections to subsystems of second order number theory ......Page 227
1.4. Methods ......Page 238
2.1. Peano arithmetic ......Page 239
2.2. Peano arithmetic with additional transfinite induction ......Page 269
3. Impredicative systems ......Page 274
3.1. Some remarks on predicativity and impredicativity ......Page 275
3.2. Axiom systems for number theory ......Page 276
3.3. Axiom systems for set theory ......Page 287
3.4. Ordinal analysis for set-theoretic axioms systems ......Page 302
References ......Page 341
Chapter V. Gödel’s Functional (“Dialectica”) Interpretation (Jeremy Avigad, Solomon Feferman) ......Page 345
1. Introduction ......Page 346
2. The Dialectica interpretation of arithmetic ......Page 349
3. Consequences and benefits of the interpretation ......Page 359
4. Models of T, type structures, and normalizability ......Page 364
5. The interpretation of fragments of arithmetic ......Page 370
6. The interpretation of analysis ......Page 373
7. Conservation results for weak König’s lemma ......Page 379
8. Non-constructive interpretations and applications ......Page 385
9. The interpretation of theories of ordinals ......Page 394
10. Interpretations based on polymorphism ......Page 401
References ......Page 408
Chapter VI. Realizability (Anne S. Troelstra) ......Page 415
1. Numerical realizability ......Page 416
2. Abstract realizability and function realizability ......Page 430
3. Modified realizability ......Page 437
4. Derivation of the Fan Rule ......Page 442
5. Lifschitz realizability ......Page 445
6. Extensional realizability ......Page 447
7. Realizability for intuitionistic second-order arithmetic ......Page 449
8. Realizability for higher-order logic and arithmetic ......Page 453
9. Further work ......Page 466
References ......Page 470
Chapter VII. The Logic of Provability (Giorgi Japaridze, Dick de Jongh) ......Page 483
1. Introduction, Solovay’s theorems ......Page 484
2. Modal logic preliminaries ......Page 485
3. Proof of Solovay’s theorems ......Page 489
5. Propositional theories and Magari-algebras ......Page 492
6. The extent of Solovay’s theorems ......Page 494
7. Classification of provability logics ......Page 496
8. Bimodal and polymodal provability logics ......Page 499
9. Rosser orderings ......Page 504
10. Logic of proofs ......Page 505
11. Notions of interpretability ......Page 508
12.1nterpretability and partial conservativity ......Page 511
13. Axiomatization, semantics, modal completeness of ILM ......Page 522
14. Arithmetic completeness of ILM ......Page 529
15. Tolerance logic and other interpretability logics ......Page 536
16. Predicate provability logics ......Page 539
References ......Page 549
Chapter VIII. The Lengths of Proofs (Pavel Pudlák) ......Page 555
1. Introduction ......Page 556
2. Types of proofs and measures of complexity ......Page 557
3. Some short formulas and short proofs ......Page 563
4. More on the structure of proofs ......Page 572
5. Bounds on cut-elimination and Herbrand’s theorem ......Page 581
6. Finite consistency statements - concrete bounds ......Page 585
7. Speed-up theorems in first order logic ......Page 593
8. Propositional proof systems ......Page 598
9. Lower bounds on propositional proofs ......Page 613
10. Bounded arithmetic and propositional logic ......Page 627
11. Bibliographical remarks for further reading ......Page 635
References ......Page 637
Chapter IX. A Proof-Theoretic Framework for Logic Programming (Gerhard Jäger, Robert F. Stärk) ......Page 647
1. Introduction ......Page 648
2. Basic notions ......Page 649
3. Some model-theoretic properties of logic programs ......Page 658
4. Deductive systems for logic programs ......Page 663
5. SLDNF-resolution ......Page 669
6. Partiality in logic programming ......Page 680
7. Concluding remark ......Page 686
References ......Page 687
Chapter X. Types in Logic, Mathematics and Programming (Robert L. Constable) ......Page 691
1. Introduction ......Page 692
2. Typed logic ......Page 700
3. Type theory ......Page 734
4. Typed programming languages ......Page 762
5. Conclusion ......Page 774
6. Appendix ......Page 776
References ......Page 781
Name Index ......Page 795
Subject Index ......Page 805