The recursion hierarchy for PCF is strict

Let PCFk denote the sublanguage of Plotkin’s PCF in which fixed point operators Yσ are admitted only for types σ of level ≤ k. We show that the languages PCFk form a strict hierarchy, in the sense that none of the Yσ for σ of level k + 1 are definable in PCFk up to observational equivalence. This answers a question posed by Berger in 1999. Our proof makes substantial use of the theory of nested sequential procedures (also called PCF B¨ohm trees) as expounded in the recent book of Longley and Normann.