Неразрешимые классы формул для конструктивного исчисления предикатов. I

Секвенция называется абсолютной, если в ее сукцеденте не более одной формулы и она не содержит вхождений знаков $\supset$, $\neg$ и положительных вхождений квантора $\forall$. Показано, что абсолютная секвенция тогда и только тогда выводима в классическом исчислении предикатов, когда она выводима в конструктивном и минимальном исчислениях предикатов. Используя генценовские методы, доказывается, что класс абсолютных секвенций вида
$$ A\to\exists x_1\dots x_n(P_1(x_2,\dots,x_n)\& P_2(x_1,\dots,x_n)), $$
где формула $A$ не содержит предикатных переменных, отличных от $P_1$ и $P_2$, является классом сведения как для классического, так и для конструктивного исчисления предикатов.
Библ. 12 назв.