Transfer from deducibility in the classical set theory to deducibility in intuitionistic set theory for the language of rings (Q2366364)

This article is a direct continuation of our previous publication [Algebra Logika 30, No. 3, 320-332 (1991; Zbl 0793.03068)] and is essentially a detailed study of one aspect of Theorem 1 of that paper. We show that for a large class of properties of the language of ring theory their deducibility in classical Zermelo-Fraenkel set theory ZF implies their deducibility in the intuitionistic set theories ZFI and \(\text{ZFI}'\) defined by \textit{R. J. Grayson} [Lect. Notes Math. 753, 402- 414 (1979; Zbl 0419.03033)]. Furthermore, the derivation of the latter deducibility from the former one is done finitely (by means of a primitive recursive function), i.e., completely explicitly, and in such a way that the increase in the length of the second conclusion depends linearly on the length of the first conclusion.