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
11 - Direct independence proofs
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
From Section 10.4 we know that all theories (R) and (R) are distinct. In this chapter we examine specific, more direct independence proofs for theories (R), (R), and(R), and we strengthen Corollary 10.4.3.
Herbrandization of induction axioms
In this section we shall examine the following idea for independence proofs: Take an induction axiom for a (α)-formula. It has the complexity (α). Introduce a new function symbol to obtain a Herbrand form of the axiom, as at the beginning of Section 7.3. But this time we reduce the axiom to an existential formula. This allows us to use a simpler witnessing theorem (Theorem 7.2.3) than the original form of the axiom would require.
Consider first the simplest case (which will turn out to be the only one for which the idea works). Let α(x, y) be a binary predicate. Then the herbrandization of the induction axiom for the formula A(a) ≔ ∃u ≥ a, α(u, a)
is the formula
Denote this formula JNDH(A(a)).
Theorem 11.1.1. The formula INDH(A(a)) is provable in (α, f) but not in (α, f). Hence (α, f) is not (α, f)-conservative over (α, f).
- Type
- Chapter
- Information
- Bounded Arithmetic, Propositional Logic and Complexity Theory , pp. 210 - 231Publisher: Cambridge University PressPrint publication year: 1995