Non-definability of the Ackermann function with type 1 partial primitive recursion (Q1816488)

The paper builds on a simply typed term system \({\mathcal {PR}}^\omega\) [cf. the author, Ann. Pure Appl. Logic 75, 153-178 (1995; Zbl 0832.68057)] providing a notion of partial primitive recursive functional on arbitrary Scott domains \(D_\sigma\) that includes a suitable concept of parallelism. Computability on the partial continuous functionals seems to entail that Kleene's schema of higher type simultaneous course-of-values recursion (SCVR) is not reducible to partial primitive recursion. The aim of the paper is to present an extension \({\mathcal {PR}^{\omega e}}\) that is closed under SCVR and yet stays within the realm of subrecursiveness in an appropriate extended sense. The twist are certain type 1 Gödel recursors \({\mathcal R}_k\) for simultaneous partial primitive recursion. Formally, given objects \(\vec g\), \(\vec H\), \(x\), \(i\) of appropriate types, \({\mathcal R}_k \vec g \vec H xi\) denotes a function \(f_i\) of type \(\iota\to \iota\), however, \({\mathcal R}_k\) is modelled such that \(f_i\) is a finite element of \(D_{\iota\to \iota}\) or in other words, a partial sequence. It is shown that the growth of any function \(f\) definable in \({\mathcal {PR}}^{\omega e}\) can be dominated by a primitive recursive function in suitable codes of \(f\)'s arguments. Thus, the Ackermann function is not definable in \({\mathcal {PR}}^{\omega e}\).