Find $\forall$-axiomatisation of definitional extension of EA with functional symbols for all Kalmar elementary functions. Then use Herbrand's theorem to find the class of provable-recursive functions in EA.
I know that class of provable-recursive functions is stable over $\Pi_1$-extensions. But how will Herbrand's theorem help? (sorry, i've just started exploring proof-theory)