The strength of replacement in weak arithmetic
arXiv:cs/0409015
Abstract
The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption.