I am not sure I fully understand the question, but there is a theorem allowing the introduction of new functional symbols. Namely, let T be the original theory. We proved . Let T' be T with a new constant 0 and a new axiom . We can define a natural translation from formulas of T' to formulas of T: e.g.,

is translated into

If is a formula in T', let denote the translation of A, which is a formula in T. Then iff , and for all formulas in the language of T, iff .