Injecting uniformities into Peano arithmetic

We present a functional interpretation of Peano arithmetic that uses Gödel’s computable functionals and which systematically injects uniformities into the statements of finite-type arithmetic. As a consequence, some uniform boundedness principles (not necessarily set-theoretically true) are interpreted while maintaining unmoved the Π 2 0 -sentences of arithmetic. We explain why this interpretation is tailored to yield conservation results.