Realizing Brouwerʹs sequences Original Research Article

When Kleene extended his recursive realizability interpretation from intuitionistic arithmetic to analysis, he was forced to use more than recursive functions to interpret sequences and conditional constructions. In fact, he used what classically appears to be the full continuum. We describe here a generalization to higher type of Kleeneʹs realizability, one case of which, (U, R)-realizability, uses general recursive functions throughout, both to realize theorems and to interpret choice sequences. (U, R)-realizability validates a version of the bar theorem and the usual continuity principles, while also providing naturally, as Kleeneʹs 1965 realizability does not, for versions of lawless sequence axioms, as well as of Churchʹs Thesis.