Kleene computable functionals and the higher order existence property (Q1104319)

In this paper the connection between constructive mathematics and recursion theory is further explored; the author gives a topos-theoretic proof of the higher order existence property. To be brief, define the sets \(\Phi\) (n), \(n=1,2,..\). inductively by: \(\Phi (0)=N=\{0,1,...\}\); \(\Phi (n+1)=N^{\Phi (n)}.\Phi\) (n) consists of the (total) functionals of type n. Existence Theorem. Fix an integer \(n\geq 0\), and suppose the existential sentence \(\exists x\in \Phi (n+1)\cdot A(x)\) is provable in constructive higher order arithmetic (HAH). Then there is a numerical term t without parameters such that the Kleene computable partial functional \(\lambda \alpha^ n\cdot t(\alpha^ n)\) \((=\) the function whose arguments are type n functionals and whose values are numbers computed using t) is provably total in HAH, and \(A(\lambda \alpha^ n\cdot t(\alpha^ n))\) is provable in HAH.