On a~hierarchy of Brouwer constructive functionals

N. A. Shanin

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VI, Tome 40 (1974), pp. 142-147

Résumé

An account is given on a variant (obeying principles of the constructive mathematics) of hierarchy approach to make precise L. E. J. Brouwer's idea of the notion of arithmetical functional defined on unary number-theoretic functions and computable from a finite number of values of its argument. Given a constructive ordinal $\beta$ a formula is constructed expressing the relation $\ll t_0$ is a godelnumber of a general recursive function (representing a functional) which bars the node of universal spread with number $t_1$ on the height not exceeding $\beta\gg$. This formula is equivalent to one of the form $\exists t_2\forall t_3\exists t_4(\varphi(t_0,t_1,t_3,t_4)=0)$, $\varphi$ being Kalmar-elementary. Functionals satisfying this condition with $t_1=0$ are called constructive Brouwer functionals of rank $\beta$. Brouwer uniform continuity theorem for constructive Brouwer functionals of rank $\beta$ can be proved by induction on $\beta$.