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.

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.

In 1969, De Jongh proved the “maximality” of a fragment of intuitionistic predicate calculus forHA. Leivant strengthened the theorem in 1975, using proof-theoretical tools (normalisation of infinitary sequent calculi). By a refinement of De Jongh's original method (using Beth models instead of Kripke models and sheafs of partial combinatory algebras), a semantical proof is given of a result that is almost as good as Leivant's. Furthermore, it is shown thatHA can be extended to Higher Order Heyting Arithmetic+all trueΠ 2 0 (...) -sentences + transfinite induction over primitive recursive well-orderings. As a corollary of the proof, maximality of intuitionistic predicate calculus is established wrt. an abstract realisability notion defined over a suitable expansion ofHA. (shrink)