In the area of strong fragments of arithmetic, it proved fruitful to study—along with the usual fragments IΣ_i—also theories axiomatized by parameter-free induction schemata, and by the closely related induction inference rules.These received much less attention in bounded arithmetic. Apart from early work of Kaye on fragments IE_i⁻ of IΔ₀, and a mention by Bloch, the first systematic investigation in the context of Buss’s theories was done by Cordón-Franco, Fernández-Margarit and Lara-Martín, who proved conservation results for Σ_i^b-induction rules and parameter-free schemata. Many basic questions remained unanswered; most importantly, nothing was published so far on Π_i^b-induction rules and parameter-free schemata.

We will have a look at some aspects of parameter-free and inference rule versions of the theories T₂ⁱ and S₂ⁱ: that is, Σ_i^b-IND⁻, Π_i^b-IND⁻, Σ_i^b-IND^R, Π_i^b-IND^R, and the corresponding variants of PIND. We are particularly interested in reductions (implications) between the fragments, conservation results, results on the number of instances (nesting) of rules, and connections to propositional reflection principles.

We will present a new witnessing theorem for (unbounded) ∀∃∀Π_i^b-consequences and ∀∃∀Π_i+1^b-consequences of the theories T₂ⁱ and S₂ⁱ, which is at the heart of some of our conservation results.