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

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

Примечательно, что эти чисто логические исследования также сформировали область универсальной алгебры. Исторически первым семантическим аппаратом для изучения этих логик были различные алгебраические системы и модели. Фундамент данного направления был заложен в исследованиях А. Тарского и А. И. Мальцева (теория моделей), Лукасевича и Поста (многозначные алгебры), Стоуна и Маккинси (псевдои топобулевы алгебры). И только в 60-е годы в работах С. Крипке появилась теоретико-модельная семантика нестандартных логик, развитая впоследствии Леммоном, Дамметтом и другими.

Вполне естественно, что первоначально изучались различные аксиоматизации логик и их теоремы. Однако затем было замечено, что изменя набор постулированных правил вывода, можем также получать различные логики. Или добавляя некоторые правила вывода мы сохраняем множество теорем логики, значительно усиливая при этом ее дедуктивную силу. Стало ясно, что правила вывода играют более важную роль в процессе вывода 2 по сравнению с аксиомами системы. Все это привело к вопросу: когда правило вывода совместимо с заданной логикой и как следствие к понятию допустимого правила вывода.

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

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

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

Проблема допустимости имеет прямой алгебраический аналог, а именно, правило допустимо в логике, если соответствующее ему квазитождество истинно на свободных алгебрах многообразия, соответствующего этой логике. Разрешимость проблемы допустимости в логике эквивалентна разрешимости квазиэквацио-нальной теории свободных алгебр многообразия, порожденного этой логикой. Это позволило привлечь к решению проблемы допустимости хорошо разработанные алгебраические методы. На основе этого подхода Рыбаковым В. В. была доказана в 1981 году разрешимость проблемы допустимости для «сильных» модальных логик — табличных и предтабличных, там же был поставлен вопрос о проблеме допустимости в «слабых» логиках [13]. Алгоритмический критерий допустимости для логик S4 + Ofc был найден Рыбаковым В. В. в 1984 в [15]. В том же году была доказана разрешимость проблемы допустимости для целого класса логик — логик, расширяющих S4.3 [17].

В [13] было замечено, что правило вывода а/ßдопустимо в суперинтуиционистской логике Л Э Int, тогда и только тогда, когда правило Т (а) /T (?) допустимо в сг (А) — наибольшем модальном напарнике Л, где Т (а) перевод Гёделя-МакКинси-Тарского интуиционистской формулы, а в модальную (см. например [5]). Появилась надежда, что проблему допустимости в Int можно решить, доказав разрешимость проблемы допустимости в одной из модальных логик яруса /Г1 (Int). В 1984 году Рыбаковым В. В. [16] был найден алгоритмический критерий допустимости правил вывода в модальной системе S4 и интуиционистской логике Int. Одновременно были получены алгебраические аналоги этих результатов — разрешимость универсальных теорий свободной алгебры замыканий и свободной псевдобулевой алгебры. Заметим, что. как показано в [14], элементарные теории этих алгебр неразрешимы.

Использованный Рыбаковым В. В. в [16] метод оказался достаточно мощным и гибким в использовании. Помимо решения основной проблемы допустимости, с помощью этого критерия удалось получить ряд не менее интересных результатов: таких, как уже упоминавшееся доказательство разрешимости универсальных теорий свободной алгебры замыканий и свободной псевдобулевой алгебры, доказательство отсутствия базиса допустимых правил от конечного числа переменных. Данная техника, с несущественными изменениями, использовалась для доказательства разрешимости проблемы допустимости в логиках Grz, S (логика Соловая), GL (логика Гёделя-Лёба), К4 (см. [67, 65]). Причем логики S и Gl представляют особый интерес, как логики, аксиоматизирующие различные варианты понятия доказуемости в арифметике [74, 1, 33, 34]. В настоящее время интенсивно исследуются различные аспекты проблемы допустимости [19]—[27], [70, 64, 40, 75, 76].

Несмотря на успехи метода в решении проблем допустимости в различных логиках, приблизительно в то же время, стали отчетливей видны его ограничения. Первое (очевидное и принципиальное) ограничение заключается в том, что проблему разрешимости по допустимости можно поставить только в разрешимых логиках, из всего многообразия нормальных модальных логик мощности континуум, поскольку допустимость правила вида р V -1 р/а в логике равносильна тому, что, а теорема этой логики. Второе принципиальное ограничение основывается на том, что метод применим только к транзитивным финитно аппроксимируемым логикам, поскольку только в этом случае удается эффективно описать «-характеристические модели логики. В то же время, оказалось, что аналогичный подход может быть реализован напрямую и в суперинтуиционистских логиках [69], полимодальных логиках, логиках схем, то есть там, где используется семантика Кринке с транзитивными фреймами.

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

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

Табличные логики, расположенные в верхней части решетки модальных (суперинтуиционистских) логик, являются наиболее сильными в классе всех данных логик. В частности, многообразие алгебр, соответствующее табличной логике, является локально конечным, т. е. любая конечно порожденная алгебра из данного многообразия — конечна. Этот факт позволил высказать предположение, что любая транзитивная табличная логика конечно базируема по допустимости.

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

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

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

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

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

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

1. Артемов С. Н. Модальные логики доказуемости // Известия Академии наук СССР. Сер. математическая. 1985. № 49. С. 1123−1154.

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

3. Ершов Ю. Л. Проблемы разрешимости и конструктивные модели. — М.: Наука, 1980.

4. Ершов Ю. Л., Лавров И. А., Тайманов А. Д., Тайцлин М. А. Элементарные теории // Успехи математических наук. 1965. Т. 20. №. 4. С. 37−108.

5. Захарьящев М. В. Синтаксис и семантика суперинтуиционистских логик // Алгебра и логика. 1989. Т. 28. № 4. С. 402−429.

6. Chagrov A., Zakharyaschev М., On the independent axiomatizability of modal and superintuitionistic logics. J. of Logic and Computation, Vol. 5, 1995, 287 — 302.

7. Максимова Л. Л. Модальные логики конечных слоев // Алгебра и логика. 1975. Т. 14. № 3. С. 304−319.

8. Максимова Л. Л., Рыбаков В. В. О решетке нормальных модальных логик // Алгебра и логика. 1974. Т. 13. № 2. С. 105 122.

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

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

11. Минц Г. Е. Допустимые и производные правила // Записки научного семинара ЛОМИ АН СССР. 1968. № 8. С. 189−191.

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

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

14. Рыбаков В. В. Элементарные теории свободных алгебр замыканий // XXVI Всесоюзная алгебраическая конференция: Тез. докл.— Ленинград, 1981. С. 116.

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

16. Рыбаков В. В. Критерий допустимости правил в модальной системе S4 и интуиционистской логике // Алгебра и логика. 1984. Т. 23. № 5. С. 546−572.

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

18. Рыбаков В. В. Базисы допустимых правил логик S4 и Int // Алгебра и логика. 1985. Т. 24. № 1. С. 87−107.

19. Рыбаков В. В. Базисы допустимых правил модальной системы Grz и интуиционистской логики // Математический сборник. 1985. Т. 128. № 3. С. 321−338.

20. Рыбаков В. В. Универсальные теории свободных Л-алгебр при, А Э 84.3 // Сложностные проблемы математической логики. Калинин. 1985. С. 72−75.

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

22. Рыбаков В. В. Уравнения в свободных топобулевых алгебрах // Алгебра и логика. 1986. Т. 25. № 2. С. 172−204.

23. Рыбаков В. В. Алгебраические методы в пропозициональной логике // Семиотика и информатика. — М., 1986. № 28. С. 102−121.

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

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

26. Рыбаков В. В. Допустимость правил вывода и логические уравнения в модальных логиках, аксиоматизирующих доказуемость // Известия АН СССР. Сер. математическая. 1990. Т. 54. № 2. С. 357−377.

27. Рыбаков В. В. Критерии допустимости правил вывода с параметрами в интуиционистской пропозициональной логике // Известия АН СССР. Сер. математическая. 1990. Т. 54. № 6. С. 693−703.

28. Rybakov V.V. Admissibility of logical inference rules. -Book. Studies in Logic and Foundations of Mathematics., Vol. 136, Elsevier Publ., Amsterdam, New-York, 1997, 617 pp.

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

30. Циткин А. И. О структурально полных суперинтуиционистских логиках // Доклады АН СССР. 1978. Т. 241. № 1. С. 4043.

31. Фейс Р. Модальная логика. — М.: Наука, 1974.

32. Balcer К. Finite equational basis for finite algebras a congruence-distributive equational class // Advanced Mathematics. 1977. V. 24. № 3. P. 207−243.

33. Beklemishev L.D. Provability logics for natural Turing progressins of arithmetical theories // Studia Logica. 1991. V. 50. P. 107 128.

34. Beklemishev L.D. On bimodal logics of provability // Annals of Pure and Applied Logic. 1994. V. 68. P. 115−159.

35. Bellissima F. Finitely Generated Free Heyting Algebras // The Journal of Symbol с Logic. 1986. V. 51. № 1. P. 152−165.

36. Blok W.J. The Free Closure Algebra on Finitely Many Generators // Indogations Mathematicae. 1977. V. 39. № 5. P. 362−379.

37. Blok W.J., Pigozzi D. A finite basis theorem for quasivarieties // Algebra Universalies. 1986. V. 22. P. 1−13.

38. Chagrov A., Zakharyaschev M., Modal logics. // Book, Cambridge Press, 1997, 589 pp.

39. Dummctt M.A.E., Lemmon E.J. Modal logics between S4 and S5. // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1959. V. 4. P. 250−264.

40. Fagin R., Halpern J.Y., Vardi M.Y. What is an inference rule // The Journal of Symbolic Logic. 1992. V. 57. № 3. P. 1018−1045.

41. Fine K. Logics Containing S4.3 // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1971. V. 17. P. 371−376.

42. Fine K. An Ascending Chain of S4 Logics. // Theoria. 1974. V. 40. P. 110−116.

43. Fine K. Logics containing K4, Part I // The Journal of Symbolic Logic. 1974. V. 39. № 3. P. 229−237.

44. Fine K. Logics containing K4. Part II // Journal of Symbolic Logic. 1985. V. 50. № 3. P. 619−651.

45. Friedman H. One hundred and two problems in mathematical logic // The Journal of Symbolic Logic. 1975. V. 40. № 3. P. 113−129.

46. Gabbay D.M. Selective Filtration in Modal Logics // Theoria. 1970. V. 30. P. 323−330.

47. Gabbay D.M. A General Filtration Method for Modal Logics // Journal of Philosophical Logics. 1972. № 1. P. 29−34.

48. Gabbay D.M., De Jongh D.H.J. A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property // The Journal of Symbolic Logic. 1974. V. 39. № 1. P. 67−78.93.

49. Gleit Z., Goldfarb W. Characters and fixed points in provability logic // Notre Dame Journal of Formal Logic. 1990. V. 31. № 1. P. 26 36.

50. Goldblatt R.I. Metamathematics of modal logics. Part I // Reports on Mathematical Logic. 1976. V. 6. P. 41−78.

51. Goldblatt R.I. Metamathematics of modal logics. Part II // Reports on Mathematical Logic. 1976. V. 7. P. 21−52.

52. Goldblatt R.I. The McKinsev axiom is not canonical // The Journal of Symbolic Logic. 1991. V. 56. № 2. P. 554 -562.

53. Gurevich Y., Shelah S. Fixed-point extensions of first-order logic J // Annals of Pure and Applied Logic. 1986. V. 32. P. 265−280.

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

55. Jonsson B., Tarski A. Boolean Algebras with operators // American Journal of Mathematics. 1951. V. 73. P. 891−939.

56. Kripke S. Semantic Analysis of Modal Logic // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1963. V. 9. P. 67−96.

57. Lemmon E.J. Algebraic semantics for modal logics, II // The Journal of Symbolic Logic. 1966. V. 31. P. 191−218.

58. Makinson D. On some completeness theorems in modal logic // Zeitschrift fur mathematische Logik und Grundlagen der Mathematik. 1966. V. 12. P. 379 -394.

59. McKinsey J.C.C. On the syntactical construction of systems of modal logic // The Journal of Symbolic Logic. 1945. V. 10. P. 83−94.

60. McKinsey J., Tarski A. Some theorems about the sentential calculi of Lewis and Heyting // The Journal of Symbolic Logic. 1948. V. 13. P. 1−15.

61. Pigozzi D. Finite basis theorem for relatively congruence-distributive quasivarieties // Transactions of the American Mathematical Society. 1988. V. 310. № 2, P. 499−533.

62. Port J. The deducibilities of S5 // Journal of Philosophical Logic. 1981. V. 10. P. 409−422.

63. Port J. Axiomatization and independence in S4 and S5 // Reports on Mathematical Logic. 1983. V. 16. P. 23−33.

64. Rautenberg W. Applications of Weak Kripke Semantics to Intermediate Consequences // Studia Logica. 1986. V. 45. P. 119−134.

65. Rybakov V.V. Logical equations and admissible rules of inference with parameters in modal provability logics // Studia Logica, 1990. V. XLIX. № 2. P. 215−239.

66. Rybakov V.V. Metatheories of first-order theories // Proc. of the IV Asian Logic Conference. CSK Educational Center. — Tokyo. Japan. 1990. P. 16−17.

67. Rybakov V.V. Problems of substitution and admissibility in the modal system Grz and intuitionistic calculus. // Annals of pure and applied logic. 1990. V. 50. P. 71−106.

68. Rybakov V.V. Poly-modal logic as metatheory of pure predicate calculus // Abstracts of the 9-th Intern. Congress of Log. Meth. and Phil, of Sci., Section 1−5. Uppsala. Sweden. 1991. P. 158.

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

70. Rybakov V.V. Criteria for admissibility of inference rules modal and intermediate logics with the branching property // Studia Logica. 1994. V. 53. № 2. P. 203−22.

71. Segerberg K. Decidability of Four Modal Logics // Theoria. 1968. V. 28. P. 21−25.

72. Segerberg K. An essay in classical modal logic // Filosofiska Studier. University of Uppsala.— Uppsala, 1971. V. 1−3. № 13.

73. Selman A. Completness of calculi for axiomaticalv defined classes of algebras // Algebra Universalies. 1972. V. 2. .№ 1. P. 20−32.

74. Solovay R. Provability interpretations of modal logic // Israel J. Math. 1976. V. 25. P. 287−304.

75. Venema Y. Derivation rules as anti-axioms in modal logic // The Journal of Symbolic Logic. 1993. V. 59. № 3. P. 1003−1034.

76. Williamson T. Some Admissible Rules in Nonnormal Modal Systems // Notre Dame Journal of Formal Logic. 1993. V. 34. № 3. P. 378−400.

77. Wojtvlak P. Independent axiomatizability of Sets of Sentences. Annals of Purer and Applied Logic, V. 44, 1989, 259 — 299. РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ.

78. В. В. Римацкий. Базисы допустимых правил вывода Табличных Модальных Логик глубины 2. Алгебра и логика, т. 35 (1996), N5 с. 612 -623.

79. V.V. Rimatskiy. Finite Bases of Admissibile inference rules for Modal Logics of Width 2. Bulletin of the Section of Logic: v.26, N.3, Oct. 1997, pp. 126 134.

80. B.B. Римацкий. О конечной базируемое&tradeдопустимых правил вывода модальных логик ширины 2. Алгебра и логика, г. 38 (1999), N5, с. 436 455.

81. V.V. Rybakov, М. Terziler, V. Remazki. Bases in semi-reduced form for admissible rules of intuitionistic logic IPC. Mathematical Logic Quaterly, No. 2, Vol. 46 (2000), 17 pp.

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

83. В. В. Рыбаков, В. В. Римацкий. 54.2-логики, сохраняющие допустимые правила вывода логики 54.2 и родственных ей логик, Сиб. Мат. Журнал, в печати.

84. В. В. Римацкий. Базисы допустимых правил вывода Табличных Модальных Логик глубины 2. Тезисы Международной конференции по математической логикег. Новосибирск, 1994; с. 86.

85. В. В. Римацкий. О базисах квазитождеств модальных алгебр. Тезисы XXXV Международной студенческой научнойконференции, секция алгебры и математической логики, г. Новосибирск, 1997; с. 86.

86. В. В. Римацкий. 1Ч-характеристические модели некоторых неклассических логик. Тезисы XV Научно-практической конференции, г. Красноярск, апрель 1997; с. 17.

87. В. В. Римацкий. Конечная базируемость допустимых правил вывода модальных логик ширины 2. Тезисы XV Научно-практической конференции, г. Красноярск, апрель 1997; с. 17.