The recursion hierarchy for PCF is strict

Let PCF_k 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 PCF_k form a strict hierarchy, in the sense that for each k, there are closed programs of PCF_{k +1} that are not observationally equivalent to any programs of PCF_k. 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öhm trees) as expounded in the forthcoming book of Longley and Normann.