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 extend TAPP with choice sequences and study the principle EBIa0. The resulting theories are used to characterise the arithmetical fragment of EL +EBIa0. As a digression, we use TAPP to show that P. Martin-Löf's basic extensional theory ML0 is conservative over intuitionistic arithmetic.

Every recursively enumerable extension of arithmetic which obeys the disjunction property obeys the numerical existence property [Fr, 1]. The requirement of recursive enumerability is essential. For extensions of intuitionistic second order arithmetic by means of sentences (in its language) with no existential set quantifiers, the numerical existence property implies the set existence property. The restriction on existential set quantifiers is essential. The numerical existence property cannot be eliminated, but in the case of finite extensions of HAS, can be replaced by (...) a weaker form of it. As a consequence, the set existence property for intuitionistic second order arithmetic can be proved within itself. (shrink)

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 extend TAPP with choice sequences and study the principle EBIa0 . The resulting theories are used to characterise the arithmetical fragment of EL +EBIa0. As a digression, we use TAPP to show that P. Martin-Löf's basic extensional theory ML0 is conservative over intuitionistic arithmetic.

V. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a "q-variant" we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe (...) an analogous development for elementary analysis, with partial continuous application replacing partial recursive application. (shrink)