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
13 - Bounds for Frege and extended Frege systems
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
In this chapter we shall discuss the complexity of Frege systems without any restrictions on the depth. There is some nontrivial information, in particular nontrivial upper bounds, but no nontrivial lower bounds are known at present (only bounds from Lemma 4.4.12).
Counting in Frege systems
Theorems 9.1.5 and 9.1.6 are useful sufficient conditions guaranteeing the existence of the polynomial size EF-proofs and of quasipolynomial size F-proofs, respectively. For example, U11 proves the pigeonhole principle PHP(R) and hence there are quasipolynomial size F-proofs of PHPn. A subtheory of corresponding to the polynomial size F-proofs, based on a version of inductive definitions, was considered by Arai (1991); see Section 9.6. Its axiomatization however, stresses a logical construction, whereas we would like a theory based on a more combinatorial principle.
The most important property of a Frege system relevant for the upper bounds is that it can count. We shall make this precise by showing that F simulates an extension of I△0(α) by counting functions, and that F p-simulates a propositional proof system cutting planes.
Definition 13.1.1.
(a) Let L0 be the language of the second order bounded arithmetic but without the symbol #.
- Type
- Chapter
- Information
- Bounded Arithmetic, Propositional Logic and Complexity Theory , pp. 279 - 298Publisher: Cambridge University PressPrint publication year: 1995