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

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

Первые модальные системы были построены К. Льюисом в начале XX века [12]. Многие известные на данный момент модальные системы ведут начало от таких областей знания, как философия, основания математики, информатика, когнитология и математическая лингвистика.

Наблюдающийся в последнее время интерес к математической логике обусловлен связью между этой логикой и логическими основаниями программирования. Благодаря данной связи стало возможным применение методов и результатов модальной логики в развитии теории программирования.

Алгебраическая семантика, а также реляционная семантика модальной логики, построенная С. Крипке [10], открыли возможность для изучения всей совокупности систем модальной логики. К этому направлению относятся исследования В. Блока, JI. Л. Максимовой, К. Сегербер-га, Е. Расевой, В. Раутенберга, В. В. Рыбакова, С. Томасона, К. Файна, В. Б. Шехтмана, Л. Л. Эсакиа и многих других.

В нашей работе будут рассматриваться как расширения известных модальных систем К4, S4 и S5, так и менее известных wK4 и DL. Логики 54 и S5 были получены при характеризации различных вариантов интерпретации оператора? («необходимость»), в то же время системы К и wK4 появились из чисто технических соображений.

Логика wK4 изучалась рядом авторов, среди которых отметим Л. Л. Эсакиа [37]. В работе [37] изучение логики wK4 связано с рассмотрением шкал Крипке со слабо транзитивным отношением достижимости, удовлетворяющим условию (х ф zSzxRySzyRz => xRz). Данная логика является промежуточной между минимальной модальной логикой К и логикой К4. Эсакиа нашел топологическую семантику для wK4 и дал определение алгебр с деривацией, образующих алгебраическую семантику этой модальной системы. В диссертации мы будем называть данные алгебры слабо транзитивными.

Заключительный параграф работы [37] посвящен рассмотрению логики KS (Krister Segerberg). Данная логика построена К. Сегербергом в работе [20] при аксиоматизации модальной системы, характеризуемой шкалами (X, R), в которых отношение достижимости R совпадает с отношением неравенства. Логика KS позднее изучалась рядом авторов, среди которых можно отметить В. Горанко [8] и М. Де Рийке [5], и получила название логики неравенства DL (Difference logic). Кроме того, было отмечено (см., например, [11]), что добавление к другим модальным операторам модальности неравенства существенно увеличивает выразительность языка.

Как правило, при изучении модальных логик выделяются классы логик, обладающих теми или иными свойствами. К таким свойствам можно отнести полноту относительно семантики некоторого типа, разрешимость, финитную аппроксимируемость, табличность, дизъюнктивное и интерполяционные свойства. Под разрешимостью свойства Р мы будем понимать существование алгоритма, позволяющего по выбранной формуле, А определить, обладает ли логика с аксиомой, А этим свойством. Остановимся подробнее на последнем из перечисленных свойств, которому посвящена данная диссертационная работа.

Интерполяционная теорема была доказана В. Крейгом в 1957 г. для классической логики предикатов [4]. Это доказательство послужило поводом для изучения интерполяции в различных формальных теориях. В классической логике предикатов интерполяционная теорема Крейга имеет ряд эквивалентных формулировок, однако для модальных логик данные формулировки становятся неэквивалентными. В этой связи было сформулировано несколько основных вариантов интерполяционного свойства: интерполяционное свойство Крейга CIP, дедуктивное ин-терполяцинное свойство IPD, ограниченное интерполяционное свойства.

I PR [13] и, наконец, слабое интерполяционное свойство WIP [16].

Д. Габбаем (см., например, [7]) доказана интерполяционная теорема для логик 54 и if, а Г. Шуммом [23] для логики 55. Данные результаты были существенно расширены JI. JI. Максимовой, получившей доказательство того, что среди расширений логики 55 ровно четыре логики, включая 55 и противоречивую логику For, обладают интерполяционным свойством Крейга [29]. В работе [7] приведен список из 37 логик, содержащий все непротиворечивые расширения 54, в которых верна теорема Крейга, а также список из 49 логик, содержащий все непротиворечивые расширения 54 со свойством IPD. Доказано, что CIP и IPD разрешимы над логикой 54. Однако А. В. Чагровым [3, 35] доказано, что над К, А данные свойства неразрешимы. Семейство расширений логики К А, обладающих свойством С IP, имеет мощность континуума [7].

Основной целыо данного диссертационного исследования является рассмотрение слабой интерполяции над логиками К4 и wKA, а также над логикой неравенства DL: расширяющей wKA.

Изучение данных свойств стало возможным благодаря существованию дуального изоморфизма между классом расширений логики и классом подмногообразий соответствующего многообразия алгебр (см., например, [7]). При этом исследование интерполяции сводится к изучению амальгамируемости многообразий модальных алгебр.

В работах JI. Л. Максимовой изучаются различные варианты амальга-мируемости многообразий модальных алгебр. В частности, в [28] показано, что не более 50 многообразий топобулевых алгебр являются амальгамируемыми, среди них не более 38 имеют свойство сверхамальгами-руемости. В работе [30] найдены необходимые и достаточные условия амальгамируемости, что позволило свести вопрос о наличии указанных свойств у данного многообразия модальных алгебр к рассмотрению подкласса конечно порожденных финитно неразложимых алгебр. Слабое интерполяционное свойство сводится к амальгамируемости класса конечно порожденных простых алгебр [31].

Цель данной работы определила перечень следующих задач: описание всех конечно порожденных простых транзитивных и слабо транзитивных модальных алгебр, а также DL-алгебр, на основании которого необходимо провести анализ амальгамируемости соответствующих многообразий модальных алгебр.

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

1. Получен критерий простоты слабо транзитивных модальных алгебр. На основании критерия получено полное описание конечно порожденных простых слабо транзитивных модальных алгебр. Описана структура вложений конечно порожденных простых DL-алгебр. Описана решетка многообразий DL-алгебр, а вместе с ней и решетка расширений логики неравенства. Представлена классификация многообразий .DL-алгебр.

2. Найдены необходимые условия амальгамируемости многообразий DL-алгебр. Доказано, что для многообразий DL-алгебр слабая амальгамируемость эквивалентна амальгамируемости. Замечено, что существует в точности 16 амальгамируемых многообразий DL-алгебр Кроме того, получен критерий слабой амальгамируемости многообразий слабо транзитивных модальных алгебр.

3. Доказана разрешимость слабого интерполяционного свойства над логиками S4, К4 и wK4 и дедуктивного интерполяционного свойства над логикой неравенства. В частности, доказано, что сами логики wK4 и DL не обладают слабым интерполяционным свойством.

Все основные результаты диссертации являются новыми.

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

Результаты дисссертации докладывались на семинарах «Неклассические логики» и «Алгебра и логика», проходящих на механико-математическом факультете Новосибирского государственного университета, а также на следующих международных конференциях: «Математика в современном мире» (Новосибирск, 2007), «Международная научная студенческая конференция» (Новосибирск, 2007 и 2009), «Logic Colloquium».

Швейцария, Бери, 2008), «Мальцевские чтения» (Новосибирск, 2009 и 2010).

Основные результаты изложены в работах [39]—[48]. Статьи [46]—[48] опубликованы в журналах, входящих в перечень ВАК ведущих рецензируемых научных журналов и изданий.

Представим содержание диссертации более подробно.

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

1. Blok W. J. The lattice of modal logics, an algebraic investigation.// The Journal of Symbol Logic. 1980. Vol. 45, No. 6, pp. 221−236.

2. Birkhoff G. On the combination of subalgebras.// Proceedings of Cambbridge Philosophical Society. 1933. Vol. 29, pp. 441−464.

3. Chagrov A. and Zakharyaschev M. Modal Logic. Oxford University Press, Oxford, 1997.

4. Craig W. Three uses of Herberand-Gentzen theorem in relating model theory and proof theory.// Journal of Symbol Logic. 1957. Vol. 22, pp. 269−285.

5. De Rijke M. The Modal logic of inequality.// The Journal of Symbol Logic. 1992. Vol. 57, No. 2, pp. 566−584.

6. Fine K. An incomplete logic containing S4.// Theoria. 1974. Vol. 40, pp. 23−29.

7. Gabbay D. M., Maksimova L. L. Interpolation and definability: modal and intuitionistic logics (Oxford Logic Guides, 46- Oxford Sci. Publ). Oxford, Clarendon Press, 2005.

8. Goranko V. Modal definability in enriched languages.// Notre Dame J. of Formal Logic. 1990. Vol. 31, No. 1, pp. 81−105.

9. Jonsson В. and Tarski A. Boolean algebras with operators.// American Journal of Mathematics. 1951. Vol. 73, pp. 891−939.

10. Kripke S. Semantic analysis of modal logic I. Mormal modal prepositional calculi.// Zeitschrift fur mathematische Logic und Grundlagen der Mathematik. 1963. Vol. 9, pp. 67−96.

11. Kudinov A. Topological modal logics with difference modality.// In: Advances in Modal Logic. 2006. College Publications, London. Vol. 6, pp. 319−332.

12. Lewis С. I. and Langford С. H. Appleton-Centyre-Croft.// Symbol Logic. 1932. New York.

13. Maksimova L. Restricted interpolation in modal logics.// In: P. Balbiani, N. Y. Suzuki, F. Wolter, M. Zakharyashev, eds. Advances in Modal Logics. Kings’s College London Publications, London. 2003. Vol. 4, pp. 297 — 312.

14. Maksimova L. On a form of interpolation in modal logic.// Logic Colloq. 2005, Bull. Symb. Log. 2006. Vol. 12, No. 2, p. 340.

15. Maksimova L. Interpolation and joint consistency.// In: We Will Show Them! Essays in Honour of Dov Gabbay. Volume 2, S. Artemov, H. Barringer, A. d’Avila Garcez, L. Lamb and J. Woods, eds. King’s College Publications, London. 2005. pp. 293−305.

16. Maksimova L. Definability and Interpolation in Non-Classical Logics.// Stud. Log. 2006. Vol. 82, No. 2, pp. 271−291.

17. Rautenberg W. Klassische und nicht-classische Aussagenlogik.// Wiesbaden, Vieweg, Braunschweig, 1979.

18. Rautenberg W. Splitting lattice of logics.// Arch. math. Logik. 1980. Vol. 20, pp. 155−159.

19. Segerberg K. Essay in classical modal logic.// Uppsala. 1971.

20. Segerberg K. «Somewhere else» and «some other time» .// In: Wright and Wrong: mini-essay in honor of G.H. von Wright, Publ. the group in logic and methodology of Real Finland. 1976. pp. 61−64.

21. Segerberg K. A note on the logic of elsewhere.// Theoria. 1980. Vol. 46, No. 2/3, pp. 183−187.

22. Shehtman V. «Everywhere» and «Here». // J. of Applied Non-classical Logic. 1999. Vol. 9, No. 2/3, pp. 369−380.

23. Shumm G. F. Interpolation in S5 and relation systems.// Reports math. Logic. 1976. Vol. 6, pp. 107−110.

24. Thomason S. K. An incompleteness theorem in modal logic.// Theoria. 1974. Vol. 40, pp. 30−34.

25. Гончаров С. С. Счетные булевы алгебры и разрешимость. Научная книга, Новосибирск, 1996.

26. Максимова Л. Л. Предтабличные расширения логики S4 Льюиса. // Алгебра и логика. 1975. Т. 14, № 1, С. 28−55.

27. Максимова Л. Л. Об одной классификации модальных логик.// Алгебра и логика. 1979. Т. 18, № 3, С. 328−340.

28. Максимова Л. Л. Интерполяционные теоремы в модальных логиках и амальгамируемые многообразия топобулевых алгебр.// Алгебра и логика. 1979. Т. 18, № 5, С. 556−586.

29. Максимова JI. Л. Интерполяционные теоремы в модальных логиках. Достаточные условия.// Алгебра и логика. 1980. Т. 19, № 2, С. 194— 213.

30. Максимова Л. Л. Модальные логики и мноообразия модальных алгебр: свойство Бета, интерполяция и амальгамируемость.// Алгебра и логика. 1992. Т. 31, № 2, С. 145−166.

31. Максимова Л. Л. Слабая форма интерполяции в эквациональной логике.// Алгебра и логика. 2008. Т. 47, № 1, С. 94−107.

32. Максимова Л. Л. Разрешимость проблемы интерполяции и родственных свойств в табличных логиках.// Алгебра и логика. 2009. Т. 48, № 6, С. 754−792.

33. Мальцев А. И. Алгебраические системы. М., Наука, 1970.

34. Расева Е., Сикорский Р. Математика метаматематики. М. Наука, 1972.

35. Чагров А. В. Неразрешимые свойства расширений логики доказуемости.// Алгебра и логика. 1990. Т. 29, № 5, С. 350—367.

36. Шрайнер П. А. Автоматическое распознавание интерполяции в модальных исчислениях. // Алгебра и логика. 2007. Т. 46, № 1, С. 103— 119.

37. Эсакиа Л. Л. Слабая транзитивность реституция.// Логические исследования. 2001. М., Наука. Т. 8, С. 244—255.

38. Янков В. А. О связи между выводимостью в интуиционистком исчислении высказываний и конечными импликативными структурами.// Доклады АН СССР. 1963. Т. 151, № 6, С. 1293 — 1294. Работы автора по теме диссертации.

39. Karpenko A. Weak interpolation property in NE (K4).// Abstracts of Plenary Talks, Tutorial, Special Sessions, Contributed Talks. Logic Colloquium 2008, Bern, Switzerland, pp.35−36.

40. Karpenko A. Weak interpolation property in NE (K4).// The Bulletin of Symbol Logic. March 2009. Vol. 15, No. 1, pp.119−120.

41. Карпенко А. В. Слабое интерполяционное свойство в расширениях логики S4. // Студент и научно-технический прогресс. Материалы XLV Международной научно студенческой конференции. Новосибирск, 2007. С. 136.

42. Карпенко А. В., Слабая интерполяция в расширениях модальной логики SA // Математика в современном мире. Материалы российской конференции. Новосибирск, 2007. С. 33—34.

43. Карпенко А. В., Финитно-неразложимые DL-алгебры // Студент и научно-технический прогресс. Материалы XLVII Международной научно студенческой конференции. Новосибирск, 2009.

44. Карпенко А. В., Описание простых слабо транзитивных модальных алгебр// Мальцевские чтения 2009 г. Материалы конференции, Новосибирск, 2009, С. 225.

45. Карпенко А. В., Амальгамируемые многообразия DL-алгебр// Мальцевские чтения 2010 г., Материалы конференции, Новосибирск, 2010, С. 23.

46. Карпенко А. В., Слабое интерполяционное свойство в расширениях логик S4 и К А.// Алгебра и логика. 2008. Т. 47, № 6, С. 705−722.

47. Карпенко А. В., Максимова Л. Л. Простые слабо транзитивные модальные алгебры.// Алгебра и логика. 2010. Т. 48, № 3, С. 349 368.

48. Карпенко А. В. Интерполяционные теоремы в расширениях логики неравенства.// Сибирский математический йсурнал. 2010 .Т. 51, № 3, С. 553−568.У4.