The strength of replacement in weak arithmetic

The replacement (or collection or choice,) axiom scheme BB(Γ) asserts bounded quantifier exchange as follows: ∀I < |a| ∃x < ao(i, x) → ∃w ∀i < |a| o (i, [w]_i) where o is in the class Γ of formulas. The theory S₂¹ proves the scheme BB(Σ₁^b), and thus in S₂¹ every Σ₁^b formula is equivalent to a strict Σ₁^b formula (in which all non-sharply-bounded quantifiers are in front). Here we prove (sometimes subject to an assumption) that certain theories weaker than S₂¹ do not prove either BB(Σ₁^b) or BB(Σ₀^b). We show (unconditionally) that V⁰ does not prove BB(Σ₁^B), where V⁰ (essentially IΣ₀^1,b) is the two-sorted theory associated with the complexity class AC⁰. We show that PV does not prove BB(Σ₀^b), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollet introduced the theory C₂⁰ associated with the complexity class TC⁰, and later introduced an apparently weaker theory Δ₁^b - CR for the same class. We use our methods to show that Δ₁^b - CR is indeed weaker than C₂⁰, assuming that RSA is secure against probabilistic polynomial time attack. Our main tool is the KPT witnessing theorem.