Totality in applicative theories (Q1896484)

This article deals with applicative theories of operations and numbers of the type considered by \textit{S. Feferman} and \textit{G. Jäger} [ibid. 65, No. 3, 243-263 (1993; Zbl 0794.03074)], but now term application is assumed to be total. It is established that the proof-theoretic strength of the theories considered does not change. One can even add the axiom of extensionality. The proof is by formalization of suitable term models. For the theories of the strength of PRA the elements are provably defined partial recursive terms. For stronger theories a suitable reduction notion is introduced by an inductive definition which can be modeled in a theory of known strength.