Допустимые правила вывода в нестандартных логиках и их базисы

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

ОГЛАВЛЕНИЕ.
ВВЕДЕНИЕ
1 Предварительные сведения
1.1 Синтаксис и алгебраическая семантика
1.2 Теоретико-модельная семантика
1.3 Правила вывода нестандартных логик
2 Критерий принадлежности конечных алгебр квазимногообразию 3$(А)
3 Базисы допустимых правил
3.1 Базисы допустимых правил логик глубины
3.2 Базисы допустимых правил логик ширины
3.3 Базис допустимых правил интуиционистской логики Int в полу-редуцированной форме
4 Логики, сохраняющие допустимость правил вывода
4.1 Сохранение допустимости правил вывода в логиках, родственных логике
4.2 S4.3-логики, сохраняющие допустимость правил
вывода
СПИСОК ЛИТЕРАТУРЫ
РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

Введение.
Любое логическое исследование связано с некоторой логической дедуктивной системой (логикой) или классом таких систем. Как правило рассматривается конкретная аксиоматизация логики. состоящая из фиксированного набора аксиом и правил вывода, определяющих данную систему. Выбирая язык, набор аксиом и правил вывода можем задать самые различные логики. Особую роль играют широко известные классическая пропозициональная логика PC и исчисление предикатов РРС, развитые в работах Д. Гильберта, К. Гёделя и Г. Генцена в 20 - 40-е годы. Примерно в то же время в трудах А. Рейтинга (интуиционистская 1930), Лукасевича (многозначная 1920), К. Льюиса (модальная 1920 -1930) появились первые логики, отличающиеся от классических - так называемые неклассические или нестандартные логики.
Примечательно, что эти чисто логические исследования также сформировали область универсальной алгебры. Исторически первым семантическим аппаратом для изучения этих логик были различные алгебраические системы и модели. Фундамент данного направления был заложен в исследованиях А. Тарского и А. И. Мальцева (теория моделей), Лукасевича и Поста (многозначные алгебры), Стоуна и Маккинси (псевдо- и топобулевы алгебры). И только в 60-е годы в работах С. Крипке появилась теоретико-модельная семантика нестандартных логик, развитая впоследствии Леммоном, Дамметтом и другими.
Вполне естественно, что первоначально изучались различные аксиоматизации логик и их теоремы. Однако затем было замечено, что изменя набор постулированных правил вывода, можем также получать различные логики. Или добавляя некоторые правила вывода мы сохраняем множество теорем логики, значительно усиливая при этом ее дедуктивную силу. Стало ясно, что правила вывода играют более важную роль в процессе вывода

по сравнению с аксиомами системы. Все это привело к вопросу: когда правило вывода совместимо с заданной логикой и как следствие к понятию допустимого правила вывода.
Понятие допустимого правила вывода, введенное Лоренценом в 50-х годах, непосредственно вытекает из понятия формального логического исчисления. Это в точности те правила вывода, добавление которых к списку постулированных правил не расширит исчисления, не изменит множество теорем логики. Ценность допустимых правил формального исчисления заключается в том, что с их помощью можно упростить и сократить процесс вывода и верификации формул в этом исчислении, кроме того понятие допустимого правила не зависит от конкретной аксиоматизации исчисления, то есть является инвариантом. Проблема допустимости правил вывода заключается в следующем: допустимо ли данное правило вывода в заданном формальном исчислении (логике).
Проблематика допустимости естественно переносится на случай логических исчислений. Если в классическом исчислении высказываний проблема допустимости правил вывода решается тривиально, то уже случай интуиционистской пропозициональной логики потребовал разработки сложной техники. Интерес к интуиционизму был вызван связями с основаниями математики. В 50-ые годы П.С. Новиков отмечал в своих лекциях важность различия допустимых и производных правил вывода в интуиционистской логике. Первые конкретные результаты по проблеме допустимости в интуиционистской логике были получены в 60-ых годах. Так Харропом в 1960 году [54], а после Минцем в 1972 [10] были получены примеры допустимых, но не производных правил вывода. Г.Е. Минцем в [10, 11] был найден ряд достаточных условий допустимости и производности в интуиционистской логике.

ния фреймов Co{üj) некоторых подпрямо неразложимых алгебр на Со(С]1). В силу произвольности выбора сгустка Ci доопределяем р-морфизм / из конечного прямого объединения фреймов Co(£j) некоторых подпрямо неразложимых алгебр на Со(ся). Лемма доказана.
Таким образом, непосредственно из предыдущей Теоремы вытекает
Теорема 2.12 Пусть X - табличная логика над 54 или Int, G - произвольный конечный Х-фрейм такой, что существует хотя бы один вырожденный сгусток первого слоя фрейма G.
G+ € дт(А) тогда и только тогда, когда для любого элемента у Е G существует р-морфизм из конечного прямого объединения фреймов Co{zj),j Е J, Х-последовагпелей максимальных подпрямо неразложимых алгебр на каждую локальную компоненту К(у), где т - мощность алгебры, порождающей логику X.
Действительно, если такой р-морфизм существует, то по Лемме 2.9 получаем следующую цепочку р-морфизмов: U,;G/3+(A) -4 JiejCo(£i) -> К(у), где 1 < w. В силу того, что фрейм G есть р-морфный образ прямого объединения всех К (у), у Е G, число которых конечно в силу конечности фрейма G, заключаем G+ Е Зт(Х).
Обратно, если G+ Е ЗуА), то для произвольного у Е G фрейм К (у) есть р-морфный образ UiejCo{cf), где I < w и с Е Зщ(А). Следовательно, учитывая замеченное выше получаем цепочку р-морфизмов ”на”: ITg/ LI jeJ Co(zj) -> Jie]Co(cf) -4 К (у), где
IA-J < w.