An Independence Result on Weak Second Order Bounded Arithmetic

We show that length initial submodels of S¹₂ can be extended to a model of weak second order arithmetic. As a corollary we show that the theory of length induction for polynomially bounded second order existential formulae cannot define the function division.