Realizability interpretation of PA by iterated limiting PCA

For any partial combinatory algebra (PCA for short) A, the class of A-representable partial functions from N to A quotiented by the filter of cofinite sets of N is a PCA such that the representable partial functions are exactly the limiting partial functions of A-representable partial functions (Akama 2004). The n-times iteration of this construction results in a PCA that represents any n-iterated limiting partial recursive function, and the inductive limit of the PCAs over all n is a PCA that represents any arithmetical partial function. Kleene's realizability interpretation over the former PCA interprets the logical principles of double negation elimination for Σ⁰ n-formulae, and over the latter PCA, it interprets Peano's arithmetic (PA for short). A hierarchy of logical systems between Heyting's arithmetic (HA for short) and PA is used to discuss the prenex normal form theorem, relativised independence-of-premise schemes, and the statement 'PA is an unbounded extension of HA'.