The replacement (or collection or choice) axiom scheme BB(T) asserts bounded quantifier exchange as follows: ∀i<|a|Ǝx<aϕ(i,x) → Ǝw∀i<|a|ϕ(i,[w]{i}) where ϕ is in the class T of formulas. The theory S_2^1 proves the scheme BB(\sum\nolimits_1^b), and thus in S_2^1 every \sum\nolimits_1^b formula is equivalent to a strict \sum\nolimits_1^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_2^1 do not prove either BB(\sum\nolimits_1^b) or BB(\sum\nolimits_0^b). We show (unconditionally) that V{0} does not prove BB(\sum\nolimits_0^B), where V{0} (essentially I\sum\nolimits_0^{1,b}) is the two-sorted theory associated with the complexity class AC{0}. We show that PV does not prove BB(\sum\nolimits_0^b), assuming that integer factoring is not possible in probabilistic polynomial time. Johannsen and Pollet introduced the theory C_2^0 associated with the complexity class TC^0 , and later introduced an apparently weaker theory \Delta _1^b - CR for the same class. We use our methods to show that \Delta _1^b - CR is indeed weaker than C_2^0, assuming that RSA is secure against probabilistic polynomial time attack. Our main tool is the KPT witnessing theorem.