Totality in applicative theories Original Research Article

In this paper we study applicative theories of operations and numbers with (and without) the non-constructive minimum operator in the context of a total application operation. We determine the proof-theoretic strength of such theories by relating them to well-known systems like Peano Arithmetic PA and the system (Π∞0-CA)<ε0 of second order arithmetic. Essential use will be made of so-called fixed-point theories with ordinals, certain infinitary term models and Church-Rosser properties.