Kleene's realizability interpretation for first-order arithmetic was shown by Hyland to fit into the internal logic of an elementary topos, the “Effective topos” . In this paper it is shown, that there is an internal realizability definition in , i.e. a syntactical translation of the internal language of into itself of form “n realizes ” , which extends Kleene's definition, and such that for sentences , the equivalence [harr]n is true in . The internal realizability definition depends on finding separated (...) covers for non-separated objects of . However, for the objects arising in higher-order arithmetic, canonical covers are available, which are definable in higher-order arithmetic. These canonical covers yield “covering axioms”. It is shown that these covering axioms, together with uniformity principles and Extended Church's Thesis, axiomatize a formalized extension of Kleene realizability to a constructive system of higher-order arithmetic. The details are worked out for second and third-order arithmetic, but the method can be extended to any order. As an application, it is shown in the final section that a certain completeness property of the category of “modest sets” can be derived in third-order arithmetic from the realizability axioms. (shrink)

We introduce a predicative version of topos based on the notion of small maps in algebraic set theory, developed by Joyal and one of the authors. Examples of stratified pseudotoposes can be constructed in Martin-Löf type theory, which is a predicative theory. A stratified pseudotopos admits construction of the internal category of sheaves, which is again a stratified pseudotopos. We also show how to build models of Aczel-Myhill constructive set theory using this categorical structure.