Logical metatheorems for abstract spaces axiomatized in positive bounded logic

In this paper we show that normed structures which can be axiomatized in positive bounded logic (in the sense of Henson and Iovino) admit proof-theoretic metatheorems (as developed by the second author since 2005) on the extractability of explicit uniform bounds from proofs in the respective theories. We apply this to design such metatheorems for abstract Banach lattices, Lp- and C(K)-spaces as well as bands in Lp(Lq)-Bochner spaces. We also show that a proof-theoretic uniform boundedness principle can serve in many ways as a substitute for the model-theoretic use of ultrapowers of Banach spaces.