Введение 3
1 Основные понятия и предварительные сведения из теории модальных
систем 4
1.1 Синтаксис модальных систем 4
1.2 Семантика Крипке для модальных систем и семантические понятия 4
1.3 Правила вывода в модальных системах 6
2 Базовые конструкции для построения критерия допустимости .... 8
2.1 ^-характеристическая модель для логики K4 + bw2 8
3 Алгоритмический критерий допустимости 12
Заключение 22
Список использованных источников 23
При изучении логических систем кроме постулированных правил вывода обычно применяются и допустимые правила, то есть те, относительно которых логики замкнуты.
Если существует алгоритм, позволяющий по любому правилу вывода распознать его допустимости в изучаемой логике, то последняя называется разрешимой по допустимости.
Проблема допустимости была решена для предтибличных модальных логик [1], конечнослойных модальных логик [2], расширений системы S4.3 [3], модальной логики S4 и интуиционистской логики Int [4]. В [4], в частности, был найден критерий допустимости правил вывода в S4. Одним из достоинств этого критерия является возможность его широкого обобщения на другие решетки модальных логик. Схема из [4] была использована для разрешения проблемы допустимости S5, K4, S4.2, S4.2Grz, в суперинтуиционистской логике KC.
Другой подход к решению проблемы допустимости состоит в отыскании конечного базиса для допустимых правил. В случае наличия такого базиса решение указанной проблемы для K4 + bw2 явилось следствие её финитной аппроксимируемости, доказанной, например в [5](стр.256). Но у этой логики отсутствует конечный базис допустимых правил. Поэтому алгоритмический путь решения по схеме [4] является наиболее простым. В результате исследования найден семантический критерий допустимости правил вывода в изучаемой логике и на его основе построен алгоритм, распознающий допустимость правил в этой логике. Таким образом проблема разрешимости по допустимости для логики решена положительно.
В работе были получены следующие результаты:
1. Найден семантический критерий допустимости правил вывода в логике K 4 + bw2.
2. Построен алгоритмический критерий, распознающий допустимость правил в логике K4 + bw2.
Проблема разрешимости по допустимости для логики K4 + bw2 решена положительно.
Полученные результаты имеют теоретическое значение и могут быть использованы в теории нестандартных логик.
