Об интуиционистском исчислении высказываний с кванторами

Пусть $L$ — язык интуиционистского исчисления высказываний $J$, пополненный кванторами $\forall$, $\exists$, и пусть исчисление $2J$ в языке $L$ содержит, кроме аксиом $J$, аксиомы $\forall\,x$ $B(x)\supset B(y)$ и $B(y)\supset\exists\,x$ $B(x)$. Строится семантика Кринке для $2J$ и доказывается теорема о полноте. Обобщается результат Д. Габбая о неразрешимости $C2J^+$ расширения $2J$ схемами $\exists\,x$ $(x\equiv B)$ и $\forall\,x$ $(A\vee B(x))\supset A\vee\forall\,x$ $B(x)$, а именно: доказывается неразрешимость всякой теории $T$ в языке $L$ такой, что $[2J]\subseteq T\subseteq[C2J^+]$ ($[2J]$ обозначает множество всех теорем исчисления $2J$). Библ. 1 назв.