Переход от выводимости в классической теории множеств к выводимости в интуиционистской теории множеств для языка колец

В работе получены следующие результаты.
Теорема 1. а) Пусть $ZFI'\vdash\forall K[T(\overline{x}), \Phi_1, \Phi_3\Rightarrow\varphi(\overline{x})]_K$. Тогда $ZFI'\vdash \forall K$ ($K$ есть $\mathcal{J}$-кольцо $\Rightarrow[T'(\overline{x}),\Phi_1\Rightarrow\varphi'(x)]_K$). Формулу $\Phi_1$ можно одновременно опустить в посылке и в заключении.
б) Пусть $ZF\vdash \forall K[T(\overline{x})\Rightarrow\psi(\overline{x})]_K$. Toгдa: 1) $ZFI'\vdash\forall K(*(K)\Rightarrow[T'(\overline{x})\Rightarrow\psi'(\overline{x})]_K)$ (напомним: если $\psi$ хорнова, то $\psi'\Rightarrow\psi$); 2) $ZFI'\vdash\forall K(*(K)\Rightarrow[T(\overline{x}), \Phi_3\Rightarrow\psi(\overline{x})]_K)$.
в) Пусть $ZF\vdash \forall K\Rightarrow[T_\varphi(\overline{x}), \Phi_3\Rightarrow\psi(\overline{x})]_K$. Тогда: 1) $ZFI'\vdash\forall K(*(K)\Rightarrow[T'(\overline{x})\Rightarrow(\neg\neg\psi)'(\overline{x})]_K)$; 2) $ZFI\vdash\forall K(*(K)\Rightarrow[T(\overline{x}),\Phi_3\Rightarrow\neg\neg\psi(\overline{x})]_K)$.
г) В п. "а" к $\Phi_1$ можно одновременно добавить в посылке $i'$, а в заключении $i$, где $i=2,3,4,5$. В пп. "б", "в" к $T_\varphi$ можно одновременно добавить в посылке $i'$, а в заключении $i$, где $i=3,4,5$.
д) Во всех предыдущих пунктах длина вывода в заключении линейно зависит от длины вывода в посылке.
Теорема 2. Пусть $T$, $T_\varphi$, $\varphi$, $\psi$ — такие же, как в теореме 2. Пункты теоремы 2 остаются верными, если в их посылках и заключениях заменить $T$ и соответственно $T'$ на $T$, добавив в заключениях условие разрешимости $T(\overline{x})$ для кольца $K$ (или вместо этого математически предположив , что $T(\overline{x})$ — позитивная теория).
Теорема 3. Пункты теорем 1 и 2 верны, если в них вместо $\forall K\dots$ написать $\forall K(\varkappa(K)\Rightarrow\dots)$, где $\varkappa(\cdot)$ — любая абсолютная формула.