Realizability models refuting Ishiharaʼs boundedness principle

Ishiharaʼs boundedness principle BD-N was introduced in Ishihara (1992) [5], and has turned out to be most useful for constructive analysis, see e.g. Ishihara (2001) [6]. It is equivalent to the statement that every sequentially continuous function from NN to N is continuous w.r.t. the usual metric topology on NN. We construct models for higher order arithmetic and intuitionistic set theory in which both every function from NN to N is sequentially continuous and in which the axiom of choice from NN to N holds. Since the latter is known to be inconsistent with the statement that all functions from NN to N are continuous these models refute BD-N.