Исследование допустимых правил вывода в нестандартных суперинтуиционистских и модальных транзитивных логиках

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

Содержание
ВВЕДЕНИЕ
1 СЕМАНТИЧЕСКИЕ МЕТОДЫ В ИССЛЕДОВАНИЯХ ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА
1.1 Синтаксис модальных и суперинтуициокиетских логик
1.2 Строение моделей Крипке
1.3 Алгебраическая семантика для модальных и еуперинтуиционистских логик .
1.4 Применение п-характеристических моделей Крипке в исследованиях допустимых правил вывода
1.5 Связь между суперинтуиционистскими и модальными логиками
2 РАЗРЕШИМОСТЬ ПО ДОПУСТИМОСТИ
МОДАЛЬНЫХ ЛОГИК Б4®аы и 54©&,+г
2.1 Предварительные сведения
2.2 Алгоритм распознавания допустимых правил вывода
модальных логик 54 © ап и 54 © £лг+і
2.3 Сохранение допустимости правил вывода при Т -переводе в модельно равномерных по допустимости логиках
3 НАСЛЕДОВАНИЕ ДОПУСТИМЫХ ПРАВИЛ ВЫВОДА В ТРАНЗИТИВНЫХ МОДАЛЬНЫХ
И СУПЕРИНТУИЦИОНИСТСКИХ ЛОГИКАХ
•3.1 Предварительные сведения
3.2 Критерий наследования допустимых правил вывода модальной логики А"4 ,

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

Актуальность темы. В основе большинства современных исследований в математической логике лежит понятие формальной дедуктивной или аксиоматической системы. Это понятие является ключевым в современном аксиоматическом методе, который без преувеличения можно назвать одним из главных достижений математической логики. Использование строгих формальных языков, учитывающих специфику поставленных задач, и создание четкого дедуктивного аппарата для построения той или иной теории сделали этот метод универсальным. Благодаря аксиоматическому методу были получены результаты, оказавшие влияние на развитие самой математики. Другое преимущество этого метода состоит в возможности использования сходных методик при решении проблем в различных областях математической логики.
При изучении свойств формальных систем наряду с теоретическими решаются и чисто прикладные задачи. Так, с использованием различных аксиоматических систем, главным образом временных и модальных логик, ведутся исследования по проблемам искусственного интеллекта и Computer Science. Среди направлений, где в последние годы плодотворно ведутся подобные исследования, можно отметить разработку баз данных, сетевые технологии, тестирование процессоров и компьютерных схем, создание самообучающихся систем и исследование различных аспектов программирования [48, 49, 52, 83, 105].
Любая формальная система определяется тремя составляющими: языком этой системы, ее аксиомами и правилами вывода. Задавая аксиоматическую систему, можно формулировать точные и корректные математические утверждения и проводить построение доказательств или опровержений теорем. Аксиоматическая система соответствует единственной пропозициональной логике, формируя с помощью правил вывода этой системы из ее аксиом множество теорем. Однако конкретная пропозициональная логика может соответствовать многим аксиоматическим системам, обладающим различной дедуктив-

Применение модели Ск(п) для исследования допустимых правил вывода определено в следующей лемме.
Лемма 1.1 [96]. Пусть А - финитно аппроксимируемая модальная логика, расширяющая логику КА, или суперинтуиционистская логика. Если существует означивание V переменных правила вывода т:= ат(£),..., ап(х)/[}{х) во фрейме некоторой р-характеристической модели Ск(р), которое опровергает правило г, тогда существует означивание 5 этих переменных во фрейме модели СЬ.(к) (где к - число переменных правила вывода г), которое также опровергает правило г.
1.5 Связь между еуперинтуициониетскими и модальными логиками
Приведем основные факты о взаимосвязи суперинтуиционистских и модальных логик. Изложение будем вести, следуя МакКинси, Тарскому, Думмету, Леммону, Максимовой и Рыбакову [14, 40, 54, 79, 96].
Первое практическое воплощение идеи Гёделя было основано на переводе пропозициональных формул языка интуиционистского исчисления в формулы модальных исчислений. Т-перевод, или перевод Гёделя-МакКинси-Тарского, имеет следующее индуктивное определение:
Т(р) := Пр, для пропозициональной переменной р,
Т(АЛВ) := Т(А)ЛТ(В),
Т(А V В) := Т(А) V Т(В), (1)
Т(А В) := □(Т(А) -э- Т(В)),
Т(-гА) := □-•Г(А).