JAF25/CMFBD2006 On the Schemes of Induction and Collection up to Definable Elements

The fragments of Peano Arithmetic IΣn and BΣn (n ≥ 0) are first order theories in the language of arithmetic L = {0, S, +, ·, ≤} axiomatized, respectively, by the induction scheme ϕ(0, �v) ∧ ∀x (ϕ(x, �v) → ϕ(Sx, �v)) → ∀x ϕ(x, �v) for every Σn–formula ϕ(x, �v); and by the collection scheme ∀x ∃y θ(x, y, �v) → ∀z ∃u ∀x ≤ z ∃y ≤ u θ(x, y, �v) for every Σn–formula θ(x, y, �v). Our work is devoted to the study of variants of these fragments where the parameters �v occurring in the previous schemes are restricted to belong to certain subsets of elements of the model. Concretely, we restrict the parameters to the class of the Σn–definable elements of the model, or to the initial segment determined by the Σn–definable elements (we say that an element a is Σn–definable in a model if there exists some Σn–formula δ(v) such that a is the only element of the model satisfying the property δ(v)). From our results on these fragments up to definable elements we obtain: (i) a (nice) axiomatization of the Σn+2–consequences of BΣn+1, and (ii) a new conservation result stating that BΣn+1 is Σn+2–conservative over IΠ − n+1, the scheme of induction for parameter free Πn+1–formulas