Исследование правил вывода в модальных логиках, расширяющих S4

• Автор: Кияткин, Владимир Ростиславович
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 1999
• Место защиты: Красноярск
• Количество страниц: 104 с.

ОГЛАВЛЕНИЕ
ВВЕДЕНИЕ
Состояние вопроса и задачи исследования
Обзор содержания диссертации и полученных
результатов
1 СЕМАНТИКА КРИПКЕ И ДОПУСТИМЫЕ
ПРАВИЛА ВЫВОДА
1.1 Необходимые предварительные результаты
1.2 А-характеристические модели и допустимые правила
вывода
2 ПРАВИЛА ВЫВОДА С МЕТАПЕРЕМЕННЫМИ И ЛОГИЧЕСКИЕ УРАВНЕНИЯ В ТАБЛИЧНЫХ И ПРЕДТАБЛИЧНЫХ
МОДАЛЬНЫХ ЛОГИКАХ
2.1 Необходимые предварительные сведения
2.2 Случай табличных логик
2.3 Случай локально-конечных предтабличных модальных логик
2.4 Исследование для предтабличной модальной логики РТг
3 НЕЗАВИСИМЫЕ БАЗИСЫ ДЛЯ ПРАВИЛ, ДОПУСТИМЫХ
В ПРЕДТАБЛИЧНЫХ ЛОГИКАХ
3.1 Необходимые предварительные сведения
3.2 Существование независимого базиса у предтабличных
модальных логик

3.3 Независимый базис предтабличных суперинтуиционистских логик
4 ФИНИТНАЯ АППРОКСИМИРУЕМОСТЬ ПО
ДОПУСТИМОСТИ
4.1 Необходимые предварительные сведения
4.2 Отсутствие финитной аппроксимируемости по допустимости для правил вывода
4.3 Логики финитно аппроксимируемые по допустимости
ЗАКЛЮЧЕНИЕ
БИБЛИОГРАФИЧЕСКИЙ СПИСОК ИСПОЛЬЗОВАННОЙ
ЛИТЕРАТУРЫ
РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ
ВВЕДЕНИЕ

Состояние вопроса и задачи исследования
Актуальность темы. Аксиоматические логические системы могут быть заданы наборами аксиом и правил вывода. Варьируя эти два множества, можно получать новые аксиоматические системы. Обычная практика состоит в подборе подходящих систем аксиом при фиксированных правилах вывода и дальнейшем анализе полученных пропозициональных логик. Ситуация с правилами вывода выглядит сложнее. Они поддаются изучению с большим трудом, поскольку семантическая теория правил вывода сравнительно слабее развита. Однако, эта область исследований очень важна, поскольку правила вывода влияют на дедуктивную силу и эффективность формальных логических систем в большей степени, чем аксиомы, так как в логических выводах они играют более активную роль. По этой причине правила вывода являются базисным объектом теории доказательств. Все формулы, выводимые из аксиом с помощью постулированных правил вывода называются теоремами логики. Зафиксировав множество всех теорем, мы можем изменять множества аксиом и правил вывода так, чтобы сделать данную аксиоматическую систему дедуктивно более мощной и удобной. Очевидно, что новое множество аксиом выбирается из теорем данной логики. Много сложнее с совокупностью правил, которые можно добавить к постулированным правилам вывода так, чтобы это не расширило множества теорем данной логики. Такие правила называют допустимыми. Допустимые правила образуют наибольший класс правил вывода, с помощью которого мы можем расширить аксиоматическую систему данной логики, сохраняя её теоремы (Ьогеп-геп Р. [60]). Потребность в поиске новых допустимых правил объясняется возмож-

Если формулы а и /3 изначально не имеют указанного вида, то всегда можно положить, например, ад = а,/Зі = /3, а а2 = 02 = Т. Правилу (1) соответствует квазитождество
С[ : — Vxi, Vz/bVpi, , (ОД (ЯЧ, ... , Рі, *. , Pm) — 2 (*1, у "Tfc; Pi у у Pm)
-s> .,Xk,Pl, .-,Pm) — /2(®1, - . , Xk,Pl, у Pm)) , (2)
где aba2,ft,ft — термы сигнатуры модальных логик, соответствующие формулам «і, се2,/Зі,/?2, a pj, 1 j т — переменные, интерпретирующиеся в свободной алгебре Зш многообразия var(2l), как свободные образующие.
Докажем следующее утверждение: Зш = q -<=>- 3s = Я Для некоторого конечного s. Действительно, для универсальной формулы q утверждение слева направо верно. Обратно, пусть Зш q. В алгебре Зш найдутся /і(«і
«1 {fly ‘ ' у 1ку 1, * у Ууп) — &2 (Уі йт), (3)
у fkyUly у ат) + /32(/і
Возьмём s = таафт,/}. В алгебре элементы «і