Глобально допустимые правила вывода

Задание базовых правил вывода имеет фундаментальное значение для логики. Наиболее общим вариантом возможных правил вывода являются допустимые правила вывода: в логике $L$ правило вывода допустимо, если множество теорем $L$ замкнуто относительно данного правила. Изучение допустимых правил вывода было стимулировано проблемой Фридмана: существует ли алгоритм распознавания допустимости правила вывода в интуиционистской логике? Для широкого класса неклассических логик проблема разрешимости по допустимости правил вывода была решена в сер. 1980-х. К проблеме А. Кузнецова (1975) восходит другой способ описания всех допустимых в логике правил: задание некоторого (конечного) набора допустимых правил, из которого все остальные допустимые в логике правила будут выводиться как следствия, т. е. задание (конечного) базиса. Большинство базовых неклассических логик не имеют конечного базиса для допустимых правил вывода. В начале 2000-х гг. для большинства базовых неклассических логик и некоторых табличных логик проблема Фридмана – Кузнецова была решена с помощью описания явного базиса для допустимых правил.
Следующим этапом изучения допустимых правил вывода неклассических логик можно считать понятие глобально допустимого правила вывода. Глобально допустимыми правилами в логике $L$ называем те правила вывода, которые допустимы сразу во всех (финитно аппроксимируемых) расширениях данной логики. Представленная работа посвящена изучению глобально допустимых правил логики $S4$. Были получены условия глобальной допустимости в логике $S4$, построена характеристическая (универсальная) модель (проверка глобальной допустимости сводится к проверке истинности правила на ее подмоделях), описаны базис (из него выводятся все глобально допустимые правила) и антибазис (из него выводятся все правила, недопустимые глобально в $S4$).