Δ0-complexity of the relation y = Πi ⩽ nF(i) Original Research Article

We prove that if G is a Δ0-definable function on the natural numbers and F(n) = Πi = 0nG(i), then F is also Δ0-definable. Moreover, the inductive properties of F can be proved inside the theory IΔ0.