Допустимые правила вывода в нестандартных логиках и их базисы Римацкий, Виталий Валентинович

Введение к работе

Актуальность темы.

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

Понятие допустимого правила вывода, введенное Лоренценом в 50-х годах, непосредственно вытекает из понятия формального логического исчисления. Это в точности те правила вывода, добавление которых к списку постулированных правил не расширит исчисления, не изменит множество теорем логики. Ценность допустимых правил формального исчисления заключается в том, что с их помощью можно упростить и сократить процесс вывода и верификации формул в этом исчислении, кроме того понятие допустимого правила не зависит от конкретной аксиоматизации исчисления, то есть является инвариантом. Проблема допустимости правил вывода заключается в следующем: допустимо ли данное правило вывода в заданном формальном исчислении (логике).

Проблематика допустимости естественно переносится на случай ло-

гических исчислений. Если в классическом исчислении высказываний проблема допустимости правил вывода решается тривиально, то уже случай интуиционистской пропозициональной логики потребовал разработки сложной техники. Первые конкретные результаты по проблеме допустимости в интуиционистской логике были получены в 60-ых годах. Так Харропом в 1960 году [22], а после Минцем в 1972 [18] были получены примеры допустимых, но не производных правил вывода. Г.Е. Минцем в [17, 18] был найден ряд достаточных условий допустимости и производ-ности в интуиционистской логике.

Вопрос о существовании алгоритма, распознающего допустимость правил вывода, был поставлен Кузнецовым А.В. Схожая проблема была включена в обзор проблем Фридмана ([21], проблема 40). В 1977 году А.И. Цит-киным были найдены критерии допустимости для правил специального вида в [19]. Им же в [20] были описаны модусно предполные суперинтуиционистские логики. Но сама проблема Кузнецова-Фридмана разрешимости по допустимости в интуиционистском исчислении высказываний оставалась открытой. Аналогичная проблема также актуальна для модальных логик. Допустимость и производность специальных правил в логике Льюиса S5 исследовалась Портом в 1981 году в [23, 24].

Проблема допустимости имеет прямой алгебраический аналог, а именно: правило допустимо в логике, если и только если соответствующее ему квазитождество истинно на свободных алгебрах многообразия, соответствующего этой логике. Разрешимость проблемы допустимости в логике эквивалентна разрешимости квазиэквациональной теории свободных алгебр многообразия, порожденного этой логикой. Это позволило привлечь к решению проблемы допустимости хорошо разработанные алгебраические методы. На основе этого подхода Рыбаковым В.В. была доказана в

1981 году разрешимость проблемы допустимости для "сильных" модальных логик — табличных и предтабличных, там же был поставлен вопрос о проблеме допустимости в "слабых" логиках [2]. Алгоритмический критерий допустимости для логик S4+crfc был найден Рыбаковым В.В. в 1984 в [3]: В том же году была доказана разрешимость проблемы допустимости для целого класса логик — логик, расширяющих S4.3 [5].

В [2] было замечено, что правило вывода а//? допустимо в суперин
туиционистской логике А Э hit, тогда и только тогда, когда правило
T(a)/T(j3) допустимо в <т(А) — наибольшем модальном напарнике А, где
Т(а) перевод Гёделя-МакКинси-Т арского интуиционистской формулы а
в модальную. Появилась надежда, что проблему допустимости в Int мож
но решить, доказав разрешимость проблемы допустимости в одной из
модальных логик яруса p~¹(lnt). В 1984 году Рыбаковым В.В. [4] был
найден алгоритмический критерий допустимости правил вывода в мо
дальной системе S4 и интуиционистской логике Int. Одновременно бы
ли получены алгебраические аналоги этих результатов — разрешимость
универсальных теорий свободной алгебры замыканий и свободной псев
добулевой алгебры. *

Помимо проблемы распознавания допустимых правил вывода не меньшую важность имеет проблема нахождения конечного числа допустимых правил вывода, называемых базисом допустимых правил вывода, из которых все остальные получаются как следствия (проблема Кузнецова, 1973г.). Проблема конечной базируемое по допустимости также имеет алгебраический аналог: нахождение базиса квазитождеств квазимногообразия, порождаемого свободной алгеброй счетного ранга JF^A) из многообразия, соответствующего логике А. Благодаря этому при изучении вопроса о конечной базируемое допустимых правил заданной логики или

класса логик оказалось возможным использовать аппарат универсальной алгебры. На сегодняшний день теория допустимых правил вывода представляет собой результат слияния методов универсальной алгебры (теории квазимногообразий) и теоретико-модельной семантики Крипке. .

Оказалось, что для многих базовых, индивидуальных нестандартных логик не существует базиса от конечного числа переменных для допустимых правил вывода. Например, Рыбаковым В.В. было доказано отсутствие такого базиса для логик S4 и Int в [6], Grz в [7], для логик 54.1, 54.2, 54/„, А'4, Л'4.1, Л'4.2, КС, /„, п Є N в Главе 4.2 [1]. Однако, некоторые фрагменты множества допустимых правил логики Int имеют конечный базис [19], так же как и любая модальная логика, расширяющая логику 54.3 (Corollary 4.3.20 [1]). В тоже время целые классы достаточно "сильных" табличных логик ширины или глубины 2 имеют конечный базис для допустимых правил, что было доказано в [26], [28].

Цель работы

1. получить достаточно эффективный и удобный семантический критерий принадлежности конечной алгебры квазимногообразию свободной алгебры конечного ранга;

2. разработать технику исследования базисов допустимых правил табличных модальных пропозициональных логик, расширяющих логику Льюиса S4, и суперинтуиционистских логик;

3. доказать конечную базируемость по допустимости произвольной табличной логики глубины 2, а также финитно аппроксимируемых логик ширины 2;

4. Описать базис допустимых правил вывода интуиционистской логи-

ки Int;

5. Описать 54.2-логики и родственные им логики, сохраняющие допустимость правил вывода, допустимых в логиках 54.2, Grz.1, КС;

В диссертации получены следующие основные результаты

5. Доказана конечная базируемость по допустимости произвольной табличной логики глубины 2, а также финитно аппроксимируемых логик ширины 2;

6. Как следствие доказана конечная базируемость квазиэквациональ-ной теории квазимногообразий, порожденных свободными алгебрами 5т(А) и &«(А), где А — логика из описанного выше класса;

7. Описан рекурсивный базис допустимых правил вывода интуиционистской логики Int в полу-редуцированной форме;

8. Описаны 54.2-логики и родственные им логики, сохраняющие допустимость правил вывода, допустимых в логиках 54.2, Grz.1, КС;

Научная новизна. Все результаты, полученные в диссертации, являются новыми и снабжены строгими доказательствами.

Теоретическая и практическая ценность. Полученные результаты имеют теоретическую ценность и могут быть использованы в дальнейших исследованиях по проблемам допустимости правил вывода и их базисов.

Апробация работы.

Результаты диссертации докладывались на Международной конференции по математической логике, посвященной 85-летию со дня рож-

дения А.И. Мальцева (г. Новосибирск, 1994 г.), XXXIV - XXXV Международных научных студенческих конференциях (г. Новосибирск, 1996 и 1997 гг.), I и II Международной конференции "Мальцевские чтения" (г. Новосибирск, 1997 и 1998 гг.), XV Межрегиональной научно- технической конференции (г. Красноярск, 1997г.), а также на заседаниях семинаров "Алгебра и логика" при Новосибирском государственном университете, семинара по неклассическим логикам при Институте математики СО РАН (г. Новосибирск) и на заседаниях Красноярского алгебраического семинара.

Публикации. По теме диссертации опубликовано 10 работ [26] - [35].

Структура и объем работы. Диссертация состоит из введения, четырех глав и списка литературы из 83 наименований и занимает 98 страниц машинописного текста.

Много раз результаты и ход работы обсуждались с Владимиром Владимировичем Рыбаковым, которому я благодарен за поддержку и терпение. ' Я также благодарен Голованову М.И. за полезные обсуждения на семинарах кафедры алгебры и математической логики Красноярского госуниверситета. .