On Σ 1 ‐definable Functions Provably Total in I ∏ 1 −

We prove the following theorem: Let φ( x ) be a formula in the language of the theory PA − of discretely ordered commutative rings with unit of the form ∃yφ′( x,y ) with φ′ and let ∈ Δ 0 and let f φ: ℕ → ℕ such that f φ ( x ) = y iff φ′( x,y ) & (∀ z < y ) φ′( x,z ). If I ∏   1 −∈(∀ x ≥ 0), φ then there exists a natural number K such that I ∏   1 −⊢ ∃y∀x( x > y ⟹ ƒφ( x ) < x K ). Here I ∏   1 −1 − denotes the theory PA − plus the scheme of induction for formulas φ( x ) of the form ∀ y φ′( x , y ) (with φ′) with φ′ ∈ Δ 0 .