On realizations of predicate formulas

M. M. Kipnis

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IV, Tome 20 (1971), pp. 40-48

Résumé

In view of Nelson's theorem for every intuitionistically derivable predicate formula there is a number realizing all its closed arithmetical substitution iastances (but not only a partial recursive function transforming every arithmetical substitution into some realization of the corresponding substitution instance). It is proved in this note that such uniform realization exists for every realizable predicate formula if substituted predicates are of bounded complexity. More precisely: for every closed predicate formula $A$, every partial recursive function realizing $A$ and every natural $k$ it is possible to construct a natural number realizing every substitution in $A$ of predicates of class $\Pi_m$ ($m\leq k$) or $\Sigma_m$ ($m\leq k$). Here $\Pi_m$ is the class of all formulas of the form $\exists e\forall x_m\rceil\forall x_{m-1}\rceil\forall x_{m-2}\dots\rceil\forall x_1R$ and $\Sigma_m$ is the class of a l l formulas of the form $\exists e\rceil\forall x_m\rceil\forall x_{m-1}\dots\rceil\forall x_1R$.