Book contents
- Frontmatter
- Contents
- Preface
- Acknowledgments
- 1 Introduction
- 2 Preliminaries
- 3 Basic complexity theory
- 4 Basic propositional logic
- 5 Basic bounded arithmetic
- 6 Definability of computations
- 7 Witnessing theorems
- 8 Definability and witnessing in second order theories
- 9 Translations of arithmetic formulas
- 10 Finite axiomatizability problem
- 11 Direct independence proofs
- 12 Bounds for constant-depth Frege systems
- 13 Bounds for Frege and extended Frege systems
- 14 Hard tautologies and optimal proof systems
- 15 Strength of bounded arithmetic
- References
- Subject index
- Name index
- Symbol index
Preface
Published online by Cambridge University Press: 02 December 2009
- Frontmatter
- Contents
- Preface
- Acknowledgments
- 1 Introduction
- 2 Preliminaries
- 3 Basic complexity theory
- 4 Basic propositional logic
- 5 Basic bounded arithmetic
- 6 Definability of computations
- 7 Witnessing theorems
- 8 Definability and witnessing in second order theories
- 9 Translations of arithmetic formulas
- 10 Finite axiomatizability problem
- 11 Direct independence proofs
- 12 Bounds for constant-depth Frege systems
- 13 Bounds for Frege and extended Frege systems
- 14 Hard tautologies and optimal proof systems
- 15 Strength of bounded arithmetic
- References
- Subject index
- Name index
- Symbol index
Summary
The central problem of complexity theory is the relation of deterministic and nondeterministic computations: whether P equals NP, and generally whether the polynomial time hierarchy PH collapses. The famous P versus NP problem is often regarded as one of the most important and beautiful open problems in contemporary mathematics, even by nonspecialists (see, for example, Smale [1992]).
The central problem of bounded arithmetic is whether it is a finitely axiomatizable theory. That amounts to deciding whether there is a model of the theory in which the polynomial time hierarchy does not collapse.
The central problem of propositional logic is whether there is a proof system in which every tautology has a proof of size polynomial in the size of the tautology. In this generality the question is equivalent to asking whether the class NP is closed under complementation. Particular cases of the problem, to establish lower bounds for usual calculi, are analogous to constructing models of associated systems of bounded arithmetic in which NP ≠ coNP.
Notions, problems, and results about complexity (of predicates, functions, proofs, …) are deep-rooted in mathematical logic, and (good) theorems about them are among the most profound results in the field. Bounded arithmetic and propositional logic are closely interrelated and have several explicit and implicit connections to the computational complexity theory around the P versus NP problem.
- Type
- Chapter
- Information
- Bounded Arithmetic, Propositional Logic and Complexity Theory , pp. xiii - xvPublisher: Cambridge University PressPrint publication year: 1995