Choice in applicative theories
Gerard R. Renardel de Lavalette · 1989
TAPP is a total applicative theory, conservative over intuitionistic arithmetic. In this paper, we first show that the same holds for TAPP + the choice principle EAC; then we generalize this to TAPP + inductive definitions. Finally, we use TAPP to show that P.Martin-Lofs basic extensional theory MLp is conservative over intuitionistic arithmetic. 1980 Mathematical Subject Classification: 03F50, 03F55. Key words and phrases: applicative theory, intuitionism, constructivism, metamathematics, Heyting's arithmetic, realizability, Skolem functions, forcing, inductive definitions, theory of types, extensional types, extensional realizability 1.1. Applicative theories. APP and TAPP are one-sorted intuitionistic theories about a universe of objects, among which the natural numbers and the constants of combinatory logic. These objects can be applied to one another; in APP this application. is partial, in TAPF t total. We refer to [TD88b, 9;.3]