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
14 - Hard tautologies and optimal proof 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
We shall study in this chapter the topic of hard tautologies: tautologies that are candidates for not having short proofs in a particular proof system. The closely related question is whether there is an optimal propositional proof system, that is, a proof system P such that no other system has more than a polynomial speed-up over P. We shall obtain a statement analogous to the NP-completeness results characterizing any propositional proof system as an extension of EF by a set of axioms of particular form. Recall the notions of a proof system and p-simulation from Section 4.1, the definitions of translations of arithmetic formulas into propositional ones in Section 9.2, and the relation between reflection principles (consistency statements) and p-simulations established in Section 9.3. We shall also use the notation previously used in Chapter 9.
Finitistic consistency statements and optimal proof systems
We shall denote by Taut (x) the formula Taut0 (x) from Section 9.3 defining the set of the (quantifierfree) tautologies, denoted TAUT itself.
Recall from Section 9.2 the definition of the translation
producing from a formula a sequence of propositional formulas (Definition 9.2.1, Lemma 9.2.2).
- Type
- Chapter
- Information
- Bounded Arithmetic, Propositional Logic and Complexity Theory , pp. 299 - 307Publisher: Cambridge University PressPrint publication year: 1995