Правила вывода многомодальных логик тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Кошелева, Анна Владимировна

• Кошелева, Анна Владимировна
• кандидат физико-математических наук
• 2007

Оглавление диссертации кандидат физико-математических наук Кошелева, Анна Владимировна

Введение.

1. Основные определения и теоремы.

1.1. Семантика Крипке.

1.2. Допустимые и выводимые правила.

2. Правила вывода SbtCt-логик.

2.1. Аксиоматика исследуемых логик.

2.2. Финитная аппроксимируемость логик 55tC/, I < t, S5tJ.

2.3. Разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик Л Э SbtCt.

2.4. Необходимые и достаточные условия разрешимости по допустимости правил с метапеременными в логиках S5tQ, I < t, S5tJ.

2.5. Структурная неполнота логик S5tCi, I < t, S5tJ.

3. Правила вывода некоторых линейных логик.

3.1. Предварительные сведения.

3.2. Разрешимость по допустимости правил вывода логик Lin Т и LinDA.

4. Логика SbtCt с ограниченным объемом сгустков.

4.1. Логики S^C? и 55(Cî|2.

4.2. Алгебра Bt.

Введение диссертации (часть автореферата) на тему «Правила вывода многомодальных логик»

Актуальность темы. В этой работе будут исследоваться на разрешимость по допустимости правил вывода некоторые многомодальные логики, расширяющие S5t, t € N, а также линейные логики LinT и LinDA, и для исследуемых логик будут построены алгоритмические критерии определения допустимости правил вывода. Правило вывода — это правило, регламентирующее допустимые способы перехода от некоторой совокупности формул ai, .,ап, называемых посылками, к некоторой определенной формуле ß, называемой заключением. Правило вывода обычно записывается в виде выражения . ,ап/ß. Правило вывода называется истинным в логике А, если из того, что а\,.,ап € А следует, что ß € А, называется выводимым (или доказуемым) в А, если ß выводится из посылок с помощью аксиом и постулированных правил логики А, и допустимым в А, если при любой подстановке е, из af £ А,., аеп € А следует, что ße 6 А. Допустимые правила вывода — это наибольший класс правил, которые мы можем использовать в выводах данной логики А, сохраняя множество ее доказуемых формул, т. е. с помощью таких правил мы не получим формул, которые не являются теоремами логики А. Так как в аксиоматике логик постулированных правил немного, то использование допустимых правил позволяет сокращать и упрощать процесс доказательства. Например, в исчислении высказываний (ИВ) и исчислении предикатов ничуть не реже, чем постулированное правило modus ponens: а, а ß /ß, используется правило а ß, ß —» 7/а —► 7. Но в ИВ все допустимые правила доказуемы, а в логиках первого порядка, модальных и супериптуиционистских логиках существуют допустимые, но не доказуемые правила вывода, и впервые это было замечено для интуиционистского исчисления Н (примерно в 50-х годах прошлого века в разных работах). Определение допустимого правила появилось в работе П. Лоренцеиа [51] в 1955 году. Правило называлось допустимым, если после добавления его к исходной системе все теоремы, выводимые при использовании этого правила, были бы теоремами исходной системы. П. Хар-роп в работе [46] за 1960 г. показал, что в Я допустимо, но не доказуемо правило -ix -* (у V z) / (~>х —► у) V (~>х —► z). До этого Г. Крайзель и X. Патнэм в [49] показали, что иитуициоиистской логике не принадлежит формула (->х —► (у v z)) —► ((-<х —► у) V (~>х -* z)). Г. Е. Минц в работе [9] доказал, что если правило г допустимо в Я и не содержит связок —» или V, то г выводимо в Я, и показал, что правило ((х —» у) —► (х V у)) / (((х у) -* х) V ((х —> у) 2))) допустимо, но не выводимо в Я. Выводимость допустимых в Я правил исследовалась также А. И. Циткиным в [34]. В модальных логиках 54, 54.1, йгг допустимо, но не выводимо правило Леммопа-Скотта □ (□ (□<>□;> -> Пр) -> {Пр V □ □ р) / ПОПр V □ -л Пр, [67].

Логики, в которых все допустимые правила доказуемы, называются структурно-полными. Такими логиками являются, к примеру, ИВ и модальная логика 54.3йгг. Модальные логики К, Т, #4, 54, 55 не являются структурно-полными. В этих логиках допустимо, но не доказуемо правило 0-<х А Ох /у. Структурной полнотой су-периптуиционистских логик занимались а. И. Циткин [35], Т. Прукнал [57], а структурную полноту модальных логик исследовали В. Джиобяк [39], В. В. Рыбаков [67]. Что касается немодальных и иесуперинтуиционистских логик, то известны такие результаты: Токарз установил структурную полноту некоторых логик Лукасевича [76], Прукнал доказал структурную полноту логики Медведева конечных задач [56], Войтыляк показал, что конечные классы многозначных логик являются структурно-полными [77].

По аналогии с проблемой разрешимости логик возникает вопрос о разрешимости по допустимости правил вывода. Впервые этот вопрос был поставлен в начале 70-х годов прошлого века X. Фридманом для интуициоиистского исчисления Я. В 1973 г. А. В. Кузнецов поставил вопрос о существовании конечного базиса допустимых правил для логики Я. Базис допустимых правил — это такие правила, из которых все остальные получаются как следствия. Положительное решение первого вопроса в 1984 г. в работе [17] и отрицательное решение второго вопроса в 1985 г. в [19] были даны В. В. Рыбаковым. Им же были найдены алгоритмические критерии и решены вопросы о базисах для широкого класса суперинтуициоиистских и транзитивных од-номодальных логик [14, 31, 67], [60]-[66]. К примеру, разрешимыми по допустимости оказываются логики #4, #4.1, #4.2, #4.3, 54, 54.1, 54.2, 54.3, вгг, вгг.2, вгг.3, Ы, Я, КС, 1С, логики #4, #4.1, #4.2, 54, 54.1, 54.2, Стг, вгг.2, Ы, Я, КС не имеют конечного базиса допустимых правил, а логика 54.3 и все ее нормальные расширения такой базис имеют и состоит он из одного правила Ох А -«Ох/у. То есть логика 54.3 и все ее нормальные расширения оказываются не только финитно-аппроксимируемы [37] и конечно аксиоматизируемы [40], но разрешимы по допустимости и обладают конечным базисом допустимых правил. Если же правило не допустимо в некоторой нормальной логике Л Э 54.3, то оно опровергается на конечном фрейме, адекватном данной логике. Таким свойством не обладают, к примеру, финитно-аппроксимируемые логики #4, 54, С?гг, [68]. В работах Р. Иемхофф [48] и В. В. Рыбакова [70] были построены бесконечные базисы для логик Я и 54 соответственно. А. Н. Руцким был построен бесконечный явный базис для логики #4 [12], а

Б. Р. Федоришиным для логики йЬ [33]. Разрешимость по допустимости логик ¿'4.2, КС и отсутствие у этих логик конечного базиса было доказано С. В. Бабенышевым в [1], [2]. Ю. В. Безгачева доказала, что транзитивные конечно-аксиоматизируемые и финитно-аппроксимируемые логики ширины 2 разрешимы по допустимости [3], а В. В. Римацким было доказано, что модальные финитно-аппроксимируемые логики ширины 2 имеют конечный базис допустимых правил [11]. Большое значение для решения задач, связанных с допустимостью правил, имела возможность представления свободных алгебр из многообразия модальных алгебр данной логики специальными моделями Крипке (являющимися реляционными) — п-характеристическими моделями. В [67] получен также критерий, при котором логика первого порядка разрешима относительно допустимости правил вывода. Такими логиками оказываются только логики, порожденные конечной моделью. Результаты о базисах и алгоритмические критерии для некоторых других модальных, временных и суперинтуиционистских логик смотрите, например, в работах [4, 10, 36, 45, 71, 72, 73].

Наряду с обычными правилами рассматриваются также правила вывода с мета-переменными, или, как еще говорят, с параметрами. Пусть, например, дано правило г := а (рь. ,рп, дь., 9/) //? (рь. ,рп, дь., и подстановки в это правило будем делать только вместо переменных р!,.,рп. Тогда переменные (¡1,- ■ ■, % называются метаперемениыми, а само правило г — правилом вывода с метапеременными. Оно считается допустимым в логике А при выполнении следующего условия. Если при некоторой подстановке вместо переменных р\,.,рп формулами 71,.,7П из того, что а(71,. ,7„, 91,. ,ф) € А следует, что ¡3(71,. ,7п, <7ь ■ ■ •,£

Причиной изучения таких правил стали проблемы подстановки и разрешимости логических уравнений, и проблема разрешимости уравнений в свободных алгебрах, соответствующих некоторой алгебраической логике. Сформулируем, например, вопрос о подстановке для заданной логики А: существует ли алгоритм, который для произвольной формулы а (р1,. ,рп, 91,., 9/), где 91,., 9; — это метапеременные, определяет, найдутся ли такие формулы /?!,.,/?„, что а (/?1, .,/?„, 91,. ,9;) € А? Проблема подстановки для интуиционистской логики Я в 50-х годах прошлого века обсуждалась в Московской и Ленинградской логических школах. Разрешимость проблемы подстановки для Н была доказана В. В. Рыбаковым в работе [29] за 1990 год. В этой работе он показал, что разрешимость проблемы подстановки, разрешимость логических уравнений, и разрешимость уравнений в свободной алгебре некоторой логики можно свести к разрешимости проблемы допустимости соответствующих правил вывода с метапеременными в соответствующей логике А. Он доказал разрешимость по допустимости правил вывода с метаперемеппыми большого класса суперинтуиционистских и транзитивных модальных логик [67, 24, 25, 28, 29, 31, 60, 62, 64]. К этому классу принадлежат КА, КАЛ, КА.2, КА.З, 54, 54.1, 54.2, 54.3, вгг, вгг.2, С?г,г.3, йЬ, Н, КС, ЬС. В. Р. Кияткиным доказано, что все предтабличные логики, расширяющие 54, и все конечно-аксиоматизируемые логики конечной глубины, разрешимы по допустимости правил вывода с метаперемеппыми [6].

Добавим еще, что также исследовались уравнения в свободных группах и свободных полугруппах. Уравнения свободных групп изучались Р. К. Линдоном [52], [53], а в свободных полугруппах Г. С. Макании построил алгоритм для нахождения решения таких уравнений [54], [55].

К настоящему времени существует глубоко развитая теория допустимых правил для транзитивных одномодальных логик, однако в нетраизитивных и многомодальных логиках кажется слишком сложным построить алгоритмы определения допустимости правил для достаточно широкого класса таких логик. Допустимости правил в иетрапзитивиых логиках посвящены, к примеру, работа М. И. Голованова и Е. М. Юрасовой [5], в которой доказана разрешимость по допустимости для нетраизитив-иой одномодальной логики с оператором «завтра», и Рыбакова [71], а допустимости в многомодальных логиках — работы [72, 73, 79, 80].

Одним из условий существования алгоритмов в [67] является обычная разрешимость логики и ее финитная аппроксимируемость. И в нашем случае алгоритмические критерии будут доказаны только для логик, обладающих этими двумя свойствами. Несмотря на то, что все расширения логики 55 финитно-аппроксимируемы, уже среди расширений логики 55з встречаются не финитно-аппроксимируемые логики, [41]. Эти логики относятся к особому классу многомодальных логик — многомерным логикам, основные результаты о которых суммированны в [41]. Но хотя обычно алгоритмы определения допустимости правил вывода строились для финитно-аппроксимируемых логик, в [72] Рыбаковым В. В. был построен алгоритм определения допустимости правил для двух не финитно-аппроксимируемых логик, это логики, порожденные фреймами {2, >, <), (/V, >, <).

Широкий круг вопросов о свойствах многомерных и многомодальных логик рассмотрен в работах [42, 43, 47, 50, 58, 74, 75].

Цель работы.

1) Исследовать разрешимость проблемы допустимости правил вывода в логиках 55¿С;, I < Ь, и 55^, где 55^, I < Ь — это логика с дополнительными к аксиоматике

S5t аксиомами л nj2 ■ ■ ■ пи • • • пчР,

У il,.,il, Vji,.,ji, il,.,il € {1 ,.,t},l <t, jk ф js, ik ф is при к ф s, a S5tJ получена добавлением к Sbt аксиом □ tp —> Пф, г := 1,. ,t.

2) Исследовать на разрешимость по допустимости правил вывода линейные логики ЫпТ и LinDA.

3) Пусть S5tC? — это логика S5tCt плюс аксиомы ^ Д О* (ft А Д чрД . l<t<n+l l<jy«<n+l

Выяснить, является ли эта логика логика табличной.

Методика исследования. В исследовании применяются общие методы модальной логики.

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

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

1) Доказана разрешимость по допустимости правил вывода финитно-аппроксимируемых и разрешимых логик, расширяющих SbtCt.

2) Доказана разрешимость по допустимости правил вывода линейных финитно-аппроксимируемых и разрешимых логик, расширяющих Lin DA.

3) Доказано, что логика S5tC? является табличной, и ее наибольшие конечные корневые фреймы содержат не более пь элементов.

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

Апробация работы. Результаты диссертации докладывались на

• XL-международной научной студенческой конференции «Студент и научно-технический прогресс» (Новосибирск, 2002 г.).

• Международной конференции «Мальцевские чтения» (Новосибирск, 2003 г.).

• Международной конференции «Алгебра, логика и кибернетика», посвященная 75-летию со дня рождения А. И. Кокорина (Иркутск, 2004 г.).

Публикации. По теме диссертации опубликовано пять работ [78]-[82].

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

Заключение диссертации по теме «Математическая логика, алгебра и теория чисел», Кошелева, Анна Владимировна

Заключение

К настоящему времени существует глубоко развитая теория допустимых правил для транзитивных одномодальных логик, но получено очень мало результатов о допустимости правил вывода в многомодальных логиках. Допустимости правил вывода в многомодальных логиках посвящены, например, работы [72, 73, 79, 80]. Поэтому полученные в диссертации результаты могут быть полезны для дальнейшего изучения правил вывода в многомодальных логиках. Имеет смысл исследовать на разрешимость по допустимости не только расширения логики £>5г, но и саму эту логику.

В работе Рыбакова [72] было доказано, что бимодальные логики, порожденные фреймами (2, >, <), (./V, >, <) не являются финитпо-аппроксимируемыми, но разрешимы относительно допустимости правил вывода. В параграфе 3.2 мы доказали, что логики, порожденные фреймами (ф, >, <), >, <) финитно-аппроксимируемы и разрешимы по допустимости. В связи с этими результатами возникает также вопрос о разрешимости по допустимости логик, порожденных, например, фреймами г, >, <), (лг, >, <), (я, >, <) и (я, >, <).

Список литературы диссертационного исследования кандидат физико-математических наук Кошелева, Анна Владимировна, 2007 год

1. Бабенышев С. В. Разрешимость проблемы допустимости правил вывода в модальных логиках 54.2 и S4.2Grz и суперинтуиционистской логике КС. // Алгебра и логика. 1992. - Т.31. - №4. - С.341-359.

2. Бабенышев С. В. Базисы допустимых правил вывода модальных логик 54.2 и SA.2Grz. // Алгебра и логика. 1993. - Т.32. - №2. - С.117-130.

3. Кияткин В. Р. Правила вывода с метапеременными и логические уравнения в табличных и предтабличных локально конечных модальных логиках. // Красноярск, Краен, университет. 1995. - Деп. в ВИНИТИ - 15.12.95. - ДО3350-В95.

4. Кияткин В. Р. Правила вывода с метапеременными и логические уравнения в предтабличной модальной логике РМ1. // Сибирский математический журнал.- 2000. Т.41. - №1. - С.88-97.

5. Мендельсон Э. Введение в математическую логику. // Москва, Наука. -1971.- 320 с.

6. Минц Г. Е. Производность допустимых правил. // Записки научного семинара ЛОМИ АН СССР. 1972. - №32. - С.85-99.

7. Руцкий А. Н. Явный базис для правил вывода, допустимых в модальной системе КА. // Красноярск, Краен, университет. 2002. - Деп. в ВИНИТИ -11.11.2002. - М939-В2002.

8. Руцкий А. Н., Федоришин Б. Р. Критерий наследования допустимых правил вывода модальной логики К А. / / Сибирский математический журнал. 2002. -Т.43 - №6.

9. Рыбаков В. В. Допустимые правила предтабличных модальных логик. // Алгебра и логика. 1981. - Т.20. - №4. - С.440-464.

10. РЫБАКОВ В. В. Базисы квазитождеств конечных модальных алгебр. // Алгебра и логика. 1982. - Т.21. - №2. - С.219-228.

11. РЫБАКОВ В. В. Разрешимость проблемы допустимости в конечнослойных модальных логиках. // Алгебра и логика. 1984. - Т.23. - №1. - С.100-116.

12. РЫБАКОВ В. В. Критерий допустимости правил в модальной системе 54 и интуиционистской логике. // Алгебра и логика. 1984. - Т.23. - №5. - С.546-572.

13. Рыбаков В. В. Допустимые правила логик, включающих 54.3. // Сибирский математический журнал. 1984. - Т.25. - №5. - С.141-145.

14. РЫБАКОВ В. В. Базисы допустимых правил логик 54 и Int. // Алгебра и логика. 1985. - Т.24. - №1. - С.87-107.

15. РЫБАКОВ В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики. // Математический сборник. 1985. - Т. 128. - №3. -С.321-339.

16. Рыбаков В. В. Универсальные теории свободных А-алгебр при А 3 54.3. // Сложностные проблемы математической логики. Калинин. 1985. - С.72-75.

17. РЫБАКОВ В. В. Алгебраические методы в пропозициональной логике. // Семиотика и информатика. 1986. - Вып.28. - С.102-121.

18. РЫБАКОВ В. В. Разрешимость по допустимости модальной системы Grz и интуиционистской логики. // Известия АН СССР: Сер. математическая. 1986. - Т.50. - №3. - С.598-616.

19. РЫБАКОВ В. В. Уравнения в свободной топобулевой алгебре. // Алгебра и логика. 1986. - Т.25. - №2. - С.172-204.

20. Рыбаков В. В. Уравнения в свободной топобулевой алгебре и проблема подстановки. // Доклады АН СССР. 1986. - Т.287. - №3. - С.554-557.

21. Рыбаков В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики. // Математический сборник. 1987. - Т.56. - №2. - С.311-331.

22. РЫБАКОВ В. В. Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике. // Известия АН СССР: Сер. математическая. 1990. - Т.54. - №6. - С.1331-1341.

23. РЫБАКОВ В. В. Семантические критерии допустимости правил вывода в логиках SA и Grz. // Математические заметки. 1991. - Т.50. - Вып.1б. - С.84-91.

24. ЦИТКИН А. И. О допустимых правилах иитуициоиистской логики высказываний. // Математический сборник. 1977. - Т. 102. - №2. - С.314-323.

25. ЦИТКИН А. И. О структурной полноте суперинтуициопистских логик. // Доклады АН СССР. 1978. - Т.241. - №1. - С.40-43.

26. Bezgacheva J. v. Admissible rules of temporal logic LinTGrz. // Bulletin of the Section of Logic. 1997. - V.26. - №2. - P.60-69.

27. Bull R. That all normal extension of 54.3 have the finite model property. // Z. fur Math. Log. und Grundl. der Math. 1967. - V.12. - P.325-329.

28. Chagrov A., Zakharyaschev M. Modal logics. // London, Cambridge Press. -1997. 589 p.

29. Dziobiak W. Structural completeness of modal logics containing KA. // Bulletin of the Section of Logic. 1983. - V.12. - M. - P.32-36.

30. Fine K. Logic containing 54.3. // Z. fur Math. Log. und Grundl. der Math. 1971. - V.17. - P.371-376.

31. Gabbay D. M., Kurucz A., Wolter F., Zakharyaschev M. Many-dimensional modal logics: theory and applications. // Studies in Logic and Foundations of Mathematics, Elseiver Sci. Publ., North-Holland. 2003. - V.148. - 768 p.

32. Gabbay D., shehtman V. Products of modal logics. Part I. // Logic Journal of the IGPL. 1998. - V.6. - P.73-146.

33. Gabbay D., Shehtman V. Products of modal logics. Part III. Products of modal and temporal logics. // Studia Logica. 2002. - V.72. - №2. - P. 157-183.

34. Goldblatt R. Logic of time and computation. // Center for the Study of Language and Information, Leland Stanford Junior University. 1987. - №7. - 126 p.

35. Golovanov M. I, Rybakov V. V., Yurasova E. M. A necessary condition for the rules to be admissible in temporal tomorrow logic. // Bulletin of the Section of Logic. 2003. - V.32. - №4. - P.213-220.

36. Harrop R. Concerning formulas of the types A —> B v C, A 3 xB(x) in intuitionistic formal system. // Journal of Symbolic Logic. 1960. - V.25. - №1. -P.27-32.

37. Hirch R., Hodkinson I., and Kurucz A. On modal logics between K x K x K and S5 x S5 x S5. // Journal of Symbolic Logic. 2002. - V.67. - P.221-234.

38. IemhOFF R. On the admissible rules of intuitionistic propositional logic. // Journal of Symbolic Logic. 2001. - V.66. - №2. - P.402-428.

39. Kreisel G., Putnam H. Eine Unableitbarkeitsbeweismethode fur den intuitionistischen Aussagankalkiil. // Arch. Math. Logik Grundlagenforsch. 1957.- V.3. Nos.3-4, 74-78.

40. Kurucz A. On axiomatising products of Kripke frames. // Journal of Symbolic Logic. 2000. - V.65. - P.923-945.

41. LORENZEN P. Einfiing in Operative Logik und Mathmatik. // Berlin. Gottingen.- Heidelberg. 1955. - 412 p.

42. Lyndon R. C. Equations in free groups. // Trans. Amer. Math. Soc. -1960. V.96.- P.445-457.

43. Lyndon R. C. Equations in free metabelian groups. // Pros. Amer. Math. Soc. -1966. V.17. - P.728-730.54. makanin G. S. Problem of solvability for equations in free semigroups. // Mathemetical Sbornik. 1977. - №.2. - P. 147-236.

44. PRUCNAL T. Structural completeness of some fragments of intermediate logics. // Bulletin of the Section of Logic. 1983. - V.12. - №1 - P.18-21.

45. Reynolds M. and Zakharyaschev M. On the products of linear modal logics. // Journal of Logic and Computation. 2001. - V.ll. - P.909-931.

46. RlMATSKlY V. V. Finite bases of admissible inference rules for modal logics of width 2. // Bulletin of the Section of Logic. 1997. - V.26. - №3. - P. 126-134.

47. RYBAKOV V. V. Metatheories of first-order theories. // Proc. of the 4-th Asian Logic Conference. CSK Educational Center. Tokyo, Japan. - 1990. - P. 16-17.

48. Rybakov V. V. Rules of inference with parameters for intuitionistic logic. // Journal of Symbolic Logic. 1992. - V.57. - №3. - P.912-923.

49. Rybakov V. V. Admissibility of logical inference rules. // Studies in Logic and Foundations of Mathematics, Elseiver Sci.Publ., North-Holland. New-York.- Amsterdam. 1997. - V.136 - 617 p.

50. Rybakov V. V. Construction of an explicit basis for rules admissible in modal system 54. // Mathematical Logic Quarterly. 2001. - V.47. - №4. - P.441-451.

51. Rybakov V. V. Logical consecutions in intransitive temporal linear logic of finite intervals. // Journal of Logic Computation. 2005. - V.15. - №5. - P.C63-678.

52. Rybakov V. V. Logical consecutions discrete linear temporal logic. // Journal of Symbolic Logic. 2005. - V.70. - №4. - P.1137-1149.

53. Rybakov V. V. Logics with universal modality and admissible consecutions. // Journal of Applied Non-Classical Logics. 2007. - V.17. - №3. - P.381-394.

54. Segerberg K. Modal logic with linear alternative relations. // Theoria. 1970. -V.36. - P.301-322.75. shehtman V. Two-dimensional modal logics. // Mathematical Notices of the USSR Academy of Sciences. 1978. - V.23. - P.417-424.