Схемы доказательств в аксиоматических теориях гильбертовского типа

Схемой вывода в аксиоматической теории называется конечная последовательность анализов применений правил и аксиом. Выводом по схеме $U$ называется любой вывод, у которого список анализов применений аксиом и правил совпадает с $U$. Схема вывода допустима, если можно построить вывод по этой схеме. Пусть $\mathfrak{A}$ — некоторая аксиоматическая теория гильбертовского типа. Рассматриваются следующие задачи: а) распознавания допустимости схем вывода в $\mathfrak{A}$, б) распознавания выводимости формулы по данной схеме вывода в $\mathfrak{A}$. Для обычных формулировок исчисления предикатов без равенства доказана разрешимость первой задачи и неразрешимость второй. Библ. – 11 назв.