Boldface Recursion on Platek Spaces

Abstract

The present work develops a boldface version of the theory of Platek spaces initiated by [2]. This is done by studying recursion on spaces with special elements which embody the so called transfer operation of [1], Chapter 14 affording full lambda-abstraction. Transfer is characteristic of the monotonic hierarchies of operative spaces, which hierarchies form models of a typed lambda-mu-calculus. The principal result here is a boldface version of the abstract Platek First Recursion Theorem of [2]; we prove appropriate boldface Enumeration and Second Recursion Theorems as well.