Анализ Допустимых Правил Вывода Нестандартных Логик

Рыбаков B.B.


Исследуются правила вывода нестандартных логик: модальных и
суперинтуиционистских систем. Алгебраический аналог изучаемых объектов -
квазимногообразия соответствующих алгебр и квазимногообразия, порожденные
свободными алгебрами. Центральное место отведено допустимым правилам вывода -
квазитождествам истинным на свободных алгебрах. Приведем ниже несколько
типичных результатов.
Подробно исследована финитная аппроксимируемость (FMP) модальных логик
по допустимости правил вывода. Найдено общее достаточное условие для
отсутствия финитной аппроксимируемости:
модальная логика над $K4$ не имеет его как только
имеет свойство ко-накрытий и ширину превышающую 2.
Поразительно много, лучше сказать все,
важные логики с шириной более 2, попадают в область действия теоремы:
$K4$ сама, $S4$, $GL$,
$K4.1$, $K4.2$, $S4.1$,
$S4.2$, $GL.2$, и. т. д. Т.е. ситуация прямо противоположна
обычной финитной аппроксимируемости:
это свойство имеет абсолютное большинство важных логик, но в отношении
FMP по допустимости, как мы доказываем, все они ведут себя иначе.
Для модальных
логик с шириной не более 2 - зоны где FMP по допустимости еще
возможно,
найдено достаточное условие:
доказывается, что все такие логики плотности 2 имеют FMP по
допустимости правил вывода.
Решается проблема эффективного описания
базиса для допустимых правил
интуиционистской логики IPC - старая открытая проблема.
Найден базис , состоящий из правил в
полу-редуцированной форме, удовлетворяющих специфическим
дополнительным условиям.
Используя представленную технику мы также находим
базис для допустимых
правил вывода логики КС закон слабого исключенного третьего.
Исследуется проблема независимости базисов для правил вывода.
Из теорем Максимовой-Эсакия-Месхи
известно, что существует ровно пять предтабличных $S4$-логик и ровно три
предтабличных суперинтуиционистских логик. Даже
табличные модальные логики иногда не имеют независимого базиса допустимых
правил вывода. Однако здесь мы доказываем, что все предтабличные
модальные логики и все предтабличные суперинтуиционистские логики обладают
независимыми базисами допустимых правил вывода.