Continuity and comprehension in intuitionistic formal systems
Michael J. Beeson · Pacific Journal of Mathematics · 1977
KLS(JR, R) in various arithmetic theories was proved in [2].The proof carries over easily to the case of KLS(X, R), as soon as one discusses how to formalize complete separable metric spaces, as is done in [3].Thus the independence results of this paper apply equally to KLS(X, R) as to KLS.