On a new notion of partial conservativity

Abstract

Roughly, a bounded formula Φ(x) is (2^C,c)-conservative if assuming Φ(2^C) gives no new bounded information on c (c being a constant for a non-standard element in Peano arithmetic PA). Similarly for iterated powers of 2. This notion is analyzed, various existence theorems are proved and, as a corollary, we obtain a strengthening of Second Gödel's Incompleteness Theorem saying that for each non-standard model M of PA and each non-standard element a ε M there is a model K of PA coinciding with M up to a and such that in K there is a very short proof of constradiction (bounded by 2 to the 2 to the 2 to the c).