Unprovability of consistency statements in fragments of bounded arithmetic Original Research Article

This paper deals with the weak fragments of arithmetic PV and S2i and their induction-free fragments PV− and S2−1. We improve the bootstrapping of S21, which allows us to show that the theory S21 can be axiomatized by the set of axioms BASIC together with any of the following induction schemas: ∑1b-PIND, ∑2b-LIND, Π1b-PIND or Π1b-LIND. We improve prior results of Pudlák, Buss and Takeuti establishing the unprovability of bounded consistency of S2−1 in S2 by showing that, if S2i proves ∀xϑ(x) with ϑ a ∑0b(∑bi)-formula, then S21 proves that each instance of ϑ(x) has a S2−1-proof in which only ∑0b(∑1b)-formulas occur. Finally, we show that the consistency of the induction-free fragment PV− of PV is not provable in PV.