Handbook of Proof Theory

Preface......Page 6
Contents......Page 10
I. An Introduction to Proof Theory - Buss......Page 12
1. Proof theory of propositional logic......Page 14
1. Frege proof systems......Page 16
2. The propositional sequent calculus......Page 21
3. Propositional resolution refutations......Page 29
1. Syntax and semantics......Page 37
2. Hilbert-style proof systems......Page 40
3. The first-order sequent calculus......Page 42
4. Cut elimination......Page 47
5. Herbrand's theorem, interpolation and definability theorems......Page 59
6. First-order logic and resolution refutations......Page 70
1. Intuitionistic logic......Page 75
2. Linear logic......Page 81
References......Page 85
II. First-Order Proof Theory of Arithmetic - Buss......Page 90
1. Fragments of arithmetic......Page 92
1. Very weak fragments of arithmetic......Page 93
2. Strong fragments of arithmetic......Page 94
3. Fragments of bounded arithmetic......Page 108
4. Sequent calculus formulations of arithmetic......Page 120
2. Gödel incompleteness......Page 123
1. Arithmetization of metamathematics......Page 124
2. The Gödel incompleteness theorems......Page 129
1. Witnessing theorems......Page 133
2. Witnessing theorem for S^i_2......Page 138
3. Witnessing theorems and conservation results for T^i_2......Page 141
4. Relationships between BΣ_n and IΣ_n......Page 145
1.......Page 148
2.......Page 149
3. A theorem of Wilkie and Paris......Page 150
References......Page 154
III. Hierarchies of Provably Recursive Functions - Fairtlough & Wainer......Page 160
1. Introduction......Page 161
2. Structured ordinals and associated hierarchies......Page 164
3. Complete ω-arithmetic......Page 175
4. Provably recursive functions of PA......Page 186
5. Independence results for PA......Page 201
6. The "true" ordinal of PA......Page 204
7. Theories with transfinite induction......Page 210
References......Page 214
IV. Subsystems of Set Theory and Second Order Number Theory - Pohlers......Page 220
1. Ordinals......Page 221
2. Partial models for axiom systems of set theory......Page 226
3. Connections to subsystems of second order number theory......Page 230
4. Methods......Page 241
1. Peano arithmetic......Page 242
2. An upper bound for spec_{Π^1_1}(NT)......Page 243
3. Lower bounds for spec_{Π^1_1}(NT)......Page 248
4. Computational complexity of Π^0_2-sentences......Page 252
5. Computational complexity of Π^0_2-sentences revisited......Page 264
1. The theories NT_< and their Π^0_2-spectra......Page 272
2. Significance of the theories NT_<......Page 274
3. Impredicative systems......Page 277
1. Some remarks on predicativity and impredicativity......Page 278
2. Axiom systems for number theory......Page 279
1. The theory ID_1......Page 280
2. Iterated inductive definitions......Page 281
3. Iterated inductive definitions in second order......Page 282
4. Π^1_1-comprehension and beyond......Page 287
1. The axiom system KP_ω......Page 290
2. The theory KPI......Page 294
3. The quantifier theorem and axiom β......Page 297
4. The theories KPi and KPβ......Page 300
5. Theories of iterated admissibility......Page 302
1. Ramified set theory......Page 305
2. A semi-formal calculus for ramified set theory......Page 309
3. Operator-controlled derivations......Page 311
4. Collapsing functions......Page 315
5. The collapsing theorem......Page 320
6. Controlling operators for axiom systems of set theory......Page 325
References......Page 344
V. Gödel's Functional ("Dialectica") Interpretation - Avigad & Feferman......Page 348
1. Functional interpretations......Page 349
2. Historical background......Page 350
3. An overview of this chapter......Page 351
1. Theories of arithmetic and the double-negation interpretation......Page 352
2. The primitive recursive functionals of finite type......Page 353
3. The Dialectica interpretation......Page 357
4. Verifying the axioms of arithmetic......Page 358
5. Equality at higher types......Page 361
1. Higher type arithmetic......Page 362
2. Some consequences of the D-interpretation......Page 364
3. Benefits of the D-interpretation......Page 366
1. Functional models......Page 367
2. Normalization and the term model......Page 368
3. Strong normalization for T......Page 370
4. Infinitely long terms......Page 371
1. IΣ_1 and the primitive recursive functions......Page 373
2. S^1_2 and the polynomial-time computable functions......Page 375
1. Towards the interpretation of stronger theories......Page 376
2. Analysis and higher type extensions......Page 377
3. The principle of bar induction......Page 378
4. The interpretation of bar induction using bar recursion......Page 379
5. Interpreting PA^ω + (AC_00)......Page 380
6. Evaluation of Spector's interpretation......Page 381
1. The theory WKL_0......Page 382
2. Hereditary majorizability......Page 384
3. Reducing WKL_0 to HA^# + (WKL')......Page 385
4. Reducing HA^# + (WKL') to HA^#......Page 386
1. Overview of the section; general pattern......Page 388
2. Finite type systems with non-constructive μ-operator etc......Page 389
3. Functional interpretations using the (μ) operator......Page 392
4. Functional interpretations using the Kleene basis operator......Page 395
1. A classical theory of countable tree ordinals......Page 397
2. The classical system ID_1 of one arithmetical inductive definition......Page 398
3. Translation of ID_1 into OR^ω_1......Page 399
4. Models of T_Ω + (μ)......Page 401
6. Functional interpretation of a constructive theory of countable tree ordinals......Page 402
8. Discussion......Page 403
1. Transfinite types and polymorphism......Page 404
2. The second-order polymorphic λ-calculus, F......Page 405
3. The interpretation of analysis......Page 406
4. Strong normalization for F......Page 408
5. Theories based on predicative polymorphism......Page 409
6. The interpretation of predicative theories of analysis......Page 410
References......Page 411
VI. Realizability - Troelstra......Page 418
1. Introduction......Page 419
2. Formalizing realizability in HA......Page 420
3. Intuitionisitic predicate logic with partial terms LPT......Page 422
5. Formalizing elementary recursion theory in HA*......Page 423
6. Formalizing rn-realizability in HA*......Page 424
8. Strong soundness theorem......Page 425
11. Axiomatizing provable realizability......Page 426
12. Extensions of HA*......Page 428
17. Notes......Page 431
2. Abstract realizability and function realizability......Page 433
3. The model of the partial recursive operations PRO......Page 435
5. Partial continuous function application......Page 436
6. The model of the partial continuous operations PCO......Page 437
10. Notes......Page 439
1. Description of intuitionistic finite-type arithmetic HA^ω......Page 440
3. Models of HA^ω......Page 441
9. Concrete forms of modified realizability......Page 444
4. Derivation of the Fan Rule......Page 445
5. Lifschitz realizability......Page 448
6. Extensional realizability......Page 450
1. The system HAS......Page 452
5. rnt-realizability for HAS*......Page 453
7. Second-order extensions of other types of realizability......Page 454
8. Realizability as a truth-value semantics......Page 455
1. Formulation of HAH......Page 456
3. Numerical realizability for many-sorted logic......Page 457
16. Products, powersets and exponentials......Page 462
31. Notes......Page 468
2. Comparison with functional interpretations......Page 469
4. Completeness questions for realizabilities......Page 470
5. Realizability for subsystems of intuitionistic arithmetic......Page 471
8. Applications to Computer Science......Page 472
References......Page 473
VII. The Logic of Provability - Japaridze & de Jongh......Page 486
1. Introduction to Solovay's theorems......Page 487
2. Modal logic preliminaries......Page 488
3. Proof of Solovay's theorems......Page 492
5. Propositional theories and Magari-algebras......Page 495
6. The extent of Solovay's theorems......Page 497
7. Classification of provability logics......Page 499
8. Bimodal and polymodal provability logics......Page 502
9. Rosser orderings......Page 507
10. Logic of proofs......Page 508
11. Notions of interpretability......Page 511
12. Interpretability and partial conservativity......Page 514
13. Axiomatization, semantics, modal completeness of ILM......Page 525
14. Arithmetic completeness of ILM......Page 532
15. Tolerance logic and other interpretability logics......Page 539
16. Predicate provability logics......Page 542
References......Page 552
VIII. The Lengths of Proofs - Pudlak......Page 558
1. Introduction......Page 559
2. Types of proofs and measures of complexity......Page 560
3. Some short formulas and short proofs......Page 566
4. More on the structure of proofs......Page 575
5. Bounds on cut-elimination and Herbrand's theorem......Page 584
6. Finite consistency statements - concrete bounds......Page 588
7. Speed-up theorems in first order logic......Page 596
8. Propositional proof systems......Page 601
9. Lower bounds on propositional proofs......Page 616
10. Bounded arithmetic and propositional logic......Page 630
11. Bibliographical remarks for further reading......Page 638
References......Page 640
IX. A Proof-Theoretic Framework for Logic Programming - Jager & Stark......Page 650
1. Introduction......Page 651
1. Syntactic framework......Page 652
2. Two-valued, three-valued and four-valued structures......Page 654
3. Four-valued versus two-valued structures......Page 657
4. Logical consequences......Page 658
5. Clark's equational theory......Page 659
6. Logic programs and their completions......Page 660
1. Adequate structures......Page 661
2. Envelopes generated by logic programs......Page 662
3. Least adequate structures......Page 663
4. The finite stages of least adequate structures......Page 665
1. The calculi R(P)......Page 666
2. Identity-free derivations in R(P)......Page 668
3. Cut elimination for identity-free derivations......Page 671
1. Negation as failure......Page 672
2. Mode assignments......Page 676
3. Soundness and completeness of SLDNF-resolution......Page 680
1. The partial completion of logic programs......Page 683
2. The calculi ∂(P)......Page 684
3. The inductive extension of logic programs......Page 686
7. Concluding remark......Page 689
References......Page 690
X. Types in Logic, Mathematics and Programming - Constable......Page 694
1. Introduction......Page 695
2. Typed logic......Page 703
1. Propositions......Page 705
2. Judgments and proofs......Page 709
3. Pure propositions......Page 711
4. Formulas......Page 712
5. Formal proofs......Page 715
6. Proof expressions and tactics......Page 719
7. Natural numbers......Page 722
8. Lists......Page 724
9. Functions......Page 725
10. Set types and local set theories......Page 729
11. Quotient types......Page 730
12. Theory structure......Page 731
13. Proofs as objects......Page 733
14. Heyting's semantics......Page 735
1. Introduction......Page 737
2. Small fragment - arithmetic......Page 741
3. First extenstions......Page 744
4. Functions......Page 749
5. Duality and disjoint unions......Page 750
7. Inductive type classes and large types......Page 752
8. Universes......Page 755
9. Semantics: PER models......Page 756
10. Using type systems to model type theories......Page 760
11. A semantics of proofs......Page 762
1. Background......Page 765
2. Type ∈ type and domain theory......Page 770
3. Recursive types......Page 771
4. Dependent records and very dependent types......Page 775
5. A very small type theory......Page 776
5. Conclusion......Page 777
6. Appendix......Page 779
References......Page 784
Name index......Page 798
Subject index......Page 808