Preservation theorems and restricted consistency statements in bounded arithmetic Original Research Article

We define and study a new restricted consistency notion View the MathML source for bounded arithmetic theories T2j. It is the strongest ∀Π1b-statement over S21 provable in T2j, similar to Con(Gi) in Krajíček and Pudlák, (Z. Math. Logik Grundl. Math. 36 (1990) 29) or RCon(Ti1) in Krajı́ček and Takeuti (Ann. Math. Artificial Intelligence 6 (1992) 107). The advantage of our notion over the others is that View the MathML source can directly be used to construct models of T2j. We apply this by proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀Π1b-separation of bounded arithmetic theories S2i from T2j (1⩽i⩽j) is equivalent to the existence of a model of S2i which does not have a Δ0b-elementary extension to a model of T2j. More specific, let View the MathML source denote that there is a nonstandard element c in M such that the function View the MathML source is total in M. Let BLΣ1b be the bounded collection schema for Σ1b-formulas. We obtain the following preservation results: the ∀Π1b-separation of S2i from T2j (1⩽i⩽j) is equivalent to the existence of 1. a model of View the MathML source which is 1b-closed w.r.t. T2j, 2. a countable model of S2i+BLΣ1b without weak end extensions to models of T2j.