We define a property of substructures of models of arithmetic, that of being length-initial, and show that sharply bounded formulae are absolute between a model and its length-initial submodels. We use this to prove independence results for some weak fragments of bounded arithmetic by constructing appropriate models as length-initial submodels of some given model.

We prove that the sharply bounded arithmetic T02 in a language containing the function symbol ⌊x /2y⌋ is equivalent to PV1.