Базис глобально допустимых правил логики $S4$

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