BIBLIOPOLIS, EDIZIONI DI FILOSOFIA E SCIENZE
Via Arangio Ruiz 83-80122 Napoli-Italy
Telephone +39-081-664606
Fax +39-081-7616273

S.R. Buss, Bounded Arithmetic, pp. X-222, 1986.
ISBN 88-7088-150-4     € 31,00
STUDIES IN PROOF THEORY - LECTURE NOTES 3

TABLE OF CONTENTS

Introduction

1.The Polynomial Hierarchy
1.1. Limited Iteration
1.2. Polynomial-time Computations
1.3. Bounded Quantifiers
1.4. The Polynomial Hierarchy
1.5. Eliminating PTC
1.6. Bounded Arithmetic Formulae
1.7. Relativization of the Polynomial Hierarchy
1.8. Appendix

2.Foundations of Bounded Arithmetic
2.1. The Language of Bounded Arithmetic
2.2. Axiomatizations of Bounded Arithmetic
2.3. Introducing Function and Predicate Symbols
2.4. Bootstrapping S12 - Phase l
2.5. Bootstrapping S12 - Phase 2
2.6. Bootstrapping T12
2.7. Replacement Axioms
2.8. Minimization Axioms
2.9. Summary of Axiomatizations of Bounded Arithmetic

3.Definability of Polynomial Hierarchy Functions

4.First-Order Natural Deduction Systems
4.1. Syntax and Rules of Natural Deduction
4.2. Bounded Arithmetic
4.3. Cut Elimination
4.4. Further Normal Forms for Proofs
4.5. Restricting by Parameter Variables
4.6. Polynomial Size, Induction Free Proofs
4.7. Parikh's Theorem

5.Computational Complexity of Definable Functions
5.1. Witnessing a Bounded Formula
5.2. The Main Proof
5.3. The Main Theorem for First Order Bounded Arithmetic
5.4. Relativization

6.Cook's Equational Theory PV ..............................................................
6.1. Preliminaries for PV and PVl ..............:......................................
6.2. S12 and the Language of PV .........................................................

6.3. Witnessing a Σb1 Formula
6.4. The Main Proof, revisited

7. Godel Incompleteness Theorems
7.1. Trees
7.2. Inductive Definitions
7.3. The Arithmetization of Metamathematics
7.4. When Truth Implies Provability
7.5. Godel Incompleteness Theorems
7.6. Further Incompleteness Results

8. A Proof-Theoretic Statement Equivalent to NP=co-NP

9. Foundations of Second Order Bounded Arithmetic
9.1. The Syntax of Second Order Bounded Arithmetic
9.2. Comprehension Axioms and Rules
9.3. Axiomatizations of Second Order Bounded Arithmetic
9.4. The Cut Elimination Theorem for Second Order Logic
9.5. Σ1,b1-Defined Functions and Δ1,b1-Defined Predicates
9.6. Σ1,b1Replacement
9.7. Cut Elimination in the Presence of Δ1,b1 -Comprehension

10. Definable Functions of Second Order Bounded Arithmetic
10.1. EXPTIME functions are Σ1,b1-definable in V12
10.2. PSPACE functions are Σ1,b1-definable in U12
10.3. Deterministic PSPACE Turing machines
10.4. Witnessing a -Formula Σ1,b1
10.5. Only PSP ACE is Σ1,b1-definable in U
10.6. Only EXPTIME is Σ1,b1 -definable in V
10.7. A Corollary about NEXPTIME∩ co-NEXPTIME
10.8. Variations, Complications and Open Questions

Postscript
References
Symbol Index
Subject Index