An Independence Result on Weak Second Order Bounded Arithmetic
Satoru Kuroda · Mathematical logic quarterly · 2001
We show that length initial submodels of S12 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.