An approach to the constructivization of Cantor's set theory

A new approach is proposed for the construction of constructive analogs of set theory in hyperarithmetic languages $\mathbf L_\Lambda$, where $\Lambda$ is a scale of constructive ordinals. For every ordinal $\alpha\leqslant\Lambda$ in the language $\mathbf L_\Lambda$, a special relation of equality $=_\alpha$ is defined for codes of one-parameter formulas (conditions) of the level $\alpha$ in a constructive hyperarithmetic hierarchy corresponding to the scale $\Lambda$. The membership relation, $\in_\alpha$ (also expressible in the language $\mathbf L_\Lambda$), is defined by the condition $x\in_\alpha y\leftrightharpoons\exists z$ ($z=_\alpha x\&z\varepsilon_\alpha y$), where the relation $\varepsilon_\alpha$ is obtained by suitable refinement of the traditional representations of the constructive relation of membership. This results in a hierarchy of constructive analogs $M_\alpha$ of the theory of sets (in which the sets are represented by codes of conditions of level $\alpha$, identified modulo the relation $=_\alpha$, and $\in_\alpha$ is taken as the relation of membership). Some properties of this hierarchy are introduced which show that for the limits $\alpha$, $M_\alpha$ is sufficiently rich from the traditional set theoretic standpoint.