Remarks on applicative theories

We deal with applicative theories which are based on combinatory logic with total application, extensionality and natural numbers. We prove a conservative extension theorem and two consistency results, involving principles of uniformity, reflection, enumeration and choice. A typical feature of these systems is that they have a strong definitional power, though they are proof-theoretically comparatively weak. As to the motivation, they have been investigated since the mid seventies in the frame of constructive (non-intuitionistic) foundations of logic and mathematics in the sense of S. Feferman. The basic proof methods mainly involve constructive semantical tools (i.e. variants of forcing and realizability).