Интуиционистская теория алгебраических систем и гейтинговозначный анализ

Доказана
Теорема. Пусть $i$ — одно из следующих трех свойств кольца: 1) бирегулярное, 2) строго регулярное, 3) строго риккартово, а $i'$ — соответственно одно из следующих трех свойств кольца: 1') простое, 2') тело, 3') без делителей нуля. Пусть $\psi$ — АЕ-формула, а $\varphi$ — любая формула в языке колец; пусть $\varphi, \psi$ — в предваренной дизъюнктивной форме (хотя допустимы и более общего вида формулы). Если в теории множеств Цермело $Z$ выводимо $Z\vdash\forall K(((i')_K\Rightarrow\forall \overline{k}\in K (\varphi(\overline{k})\Rightarrow \psi(\overline{k}))_K))$, то в интуиционистской теории множеств Грейсона $ZFI$ выводимо ${ZFI\vdash\forall K((i)_K\wedge *(K)\Rightarrow\forall\overline{k}\in K(\varphi(\overline{k})\Rightarrow \psi(\overline{k}))_K)}$. Отсюда, по теореме Майхилла, можно строить терм в языке $ZF$, который для Е-формулы $\psi$ (а в ряде случаев и для АЕ-формулы $\psi$; например, в случае кольца $Z$) представляет то $y$, существование которого утверждается в $\psi$. Здесь $*(K)$ означает: $\forall c\in \mathcal{T}(k)\forall k,t,\ell\in K\forall e\in B(K)$ ($e\in[\![\check{t}=\check{e}]\!]_{B(K)}(c)\wedge e\cdot k=e\cdot t\Rightarrow e\cdot k=e\cdot \ell$); например, условие $*(K)$ следует из строгой разрешимости кольца $K$. Если вместо $(i')_K$ и $(i)_K$ соответственно написать одну и ту же формулу $\varkappa(K)^K$ в языке $ZF$ и при этом дополнительно потребовать, чтобы $ZFI\vdash[\varkappa(K)\Rightarrow[\![\varkappa(L(K))]\!]_{B(K)}=1]\wedge[K\text{- нормальное кольцо}]$, то верно будет такое же заключение. Здесь $L(K)$, например, равно $K$ или $K'$. Соответствие $i\leftrightarrow i'$ может быть описано в общем виде.