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

Введение

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

2. Логика эпистемической разрешимости

2.1. Транзитивная евклидова логика разрешимости.

2.2. Сериальная логика разрешимости.

3. Секвенциальная логика арифметической разрешимости

3.1. Аксиоматические системы.

3.2. Полнота аксиоматик.

4. Секвенциальные рефлексивные логики разрешимости

4.1. Аксиоматические системы.

4.2. Метод замыкания.

4.3. Полнота аксиоматик.

4.4. Полнота посредством обратного перевода.

4.5. Неустранимость сечения и интерполяция.

4.6. Логика доказательств с оператором сильной разрешимости

5. Определимые классы шкал

5.1. Определимость классов шкал в >-языке.

5.2. Элементарные эквиваленты для >-формул.

5.3. Инфинитарный оператор И.

5.4. Определимость классов шкал в К1-языке.

5.5. Эквиваленты I и II порядка для И-формул.

Актуальность темы. При построении логических исчислений в модальной логике традиционным стал выбор языка с операторами необходимости □ и возможности О- Однако определенный технический и философский интерес (см. [22]) представляют системы, где в качестве базисного выбирается оператор разрешимости (или неслучайности1), подразумеваемая семантика которого определяется равенством >Л = ПАУ П~*А. Это равенство задает перевод [>-формул (т.е. формул модального языка с единственным модальным оператором [>, или >-языка) в Ш-формулы (определяемые аналогично). Теперь, если задана П-логика L (т.е. логика в ПН-языке), то логикой разрешимости над L (обозначаемой посредством L>) называется множество >-формул, переводы которых являются теоремами логики L.

В работах [22, 23] были предложены различные аксиоматики логик разрешимости над известными нормальными логиками Т, S4 и S5 (определения которых см. ниже). Некоторые семейства логик разрешимости в интервале между Т> и 85^ изучались в работах [24, 25]. Отметим, что в случае когда логика L содержит Т, а точнее, аксиому рефлексивности ПА —У А, исследование логики разрешимости над L упрощается благодаря тому, что оператор □ выразим через t> посредством равенства ПА = А &; о А Аналогичная картина наблюдается в логике Ver, имеющей

Термин „неслучайность" (non-contingency) принят в англоязычной литературе; мы будем употреблять термин „разрешимость", происходящий из рассмотрения доказуемостной интерпретации оператора □ (предложение разрешимо в теории, если в ней доказуемо либо оно, либо его отрицание). в числе своих теорем все формулы вида ПА: в этой логике □ выражается через > посредством тривиального равенства ПА = Т. В статье [13] построен нетривиальный пример логики, не содержащей Т и отличной от Ver, в которой тем не менее □ выразим через [>.

Систематичное изучение логики разрешимости было начато в работе [17], содержащей первую, достаточно громоздкую аксиоматику минимальной логики разрешимости (т.е. логики К^). В последующей работе [19] эта аксиоматика была упрощена, а также была аксиоматизирована логика разрешимости над К4.

Определенный интерес к изучению модальной логики связан с возможностью использовать ее в качестве инструмента исследования понятия формальной доказуемости. Эти исследования восходят к работам И.Орлова [6] и К.Гёделя [15]. Формулировка „правильной" логики доказуемости в арифметике Пеано, известной сейчас как логика Гёделя-Лёба GL, появилась позднее в работе М.Лёба [20], а первое доказательство арифметической полноты логики GL принадлежит Р.Соловэю [30].

Логика Гёделя-Лёба GL является наименьшей по включению логикой доказуемости. Она описывает модальные законы, которым подчиняется предикат доказуемости в „объектной" теории РА с точки зрения „метатеории" РА. Если же варьировать „метатеорию" в классе расширений РА, а „объектную" теорию — в классе перечислимых расширений РА, то получится семейство логик доказуемости (имеющее мощность континуума), полностью описанное Л.Д.Беклемишевым (см. [1], формальное определение логики доказуемости см. там же).

Наряду с доказуемостью, понятие разрешимости в формальной теории является одним из центральных в теории доказательств. Так, первая теорема Гёделя о неполноте утверждает, что существуют неразрешимые в РА предложения. Нам удалось аксиоматизировать лишь минимальную логику арифметической разрешимости — логику GL^. Естественным образом возникает интересная проблема описания многообразия всех пропозициональных логик арифметической разрешимости, аналогичная упомянутой выше.

Другим аспектом, объясняющим интерес к модальной логике, являются выразительные возможности ее языка, с точки зрения, например, семантики Крипке. Известно (см. [11, 10]), что, с одной стороны, модальный язык не сравним по выразительным возможностям с языком первого порядка, а с другой, он вкладывается в язык второго порядка.

Поскольку имеется естественное вложение языка с оператором разрешимости в язык с оператором необходимости, выразительные возможности первого не больше, чем последнего. В статье [17] было обнаружено, что они даже существенно меньше: известные классы шкал, определимые в □языке, такие как классы рефлексивных, сериальных, транзитивных, симметричных, евклидовых шкал, оказываются не определимыми в >-языке. В настоящее время вопрос о точных границах выразительных возможностей >-языка мало изучен; ему посвящена последняя глава настоящей работы.

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

Методы исследования. В диссертации использована техника канонических моделей для доказательства полноты систем гильбертовского типа, адаптированная для применения к логикам разрешимости в работах [17, 19], метод пополнения секвенций и его модификация — метод насыщения секвенций для доказательства полноты секвенциальных исчислений. Научная новизна. Результаты диссертации являются новыми и состоят в следующем:

1) Построены гильбертовские системы для логик разрешимости над логиками В, К5, К45, „эпистемической" логикой KD45, логикой Гже-горчика Grz, логикой арифметической доказуемости GL.

2) Построены секвенциальные исчисления (с сечением) для логик разрешимости над логиками К, К4, GL, а также секвенциальные исчисления с аналитическим правилом сечения для логик разрешимости над рефлексивными логиками Т, S4, В, S5, Grz. Доказано, что последние логики обладают интерполяционным свойством Крейга.

3) Установлено, что в секвенциальных исчислениях для рефлексивных логик разрешимости сечение неустранимо; в то же время, доказано, что данные исчисления для логик разрешимости над Т, S4, S5 и Grz обладают (слабым в случае Grz) свойством подформульности.

4) Доказана определимость в элементарном языке классов шкал, задаваемых некоторыми из аксиом рассмотренных логик разрешимости.

5) Построена полная аксиоматика логик доказательств с оператором сильной разрешимости, отвечающих некоторым естественным классам предикатов доказательства в арифметике.

6) Найден инфинитарный оператор необходимости, определимый через оператор разрешимости, и изучены выразительные возможности языка с этим оператором в смысле семантики Крипке.

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

Апробация. Результаты диссертации докладывались и обсуждались на семинаре "Модальная и алгебраическая логика" (под руководством В. Б. Шехтмана и М. Р. Пентуса), на семинаре "Алгоритмические вопросы алгебры и логики" (под руководством проф. С.И.Адяна), и на Научно-исследовательском семинаре по математической логике механико-математического факультета МГУ (под руководством проф. С.И.Адяна и проф. В.А.Успенского), семинаре по математической логике математического факультета Тверского государственного университета (под руководством проф. А. В. Чагрова). Основные результаты диссертации содержатся в следующих публикациях автора: [2], [3], [4], [32], [33]. Структура и объем работы. Диссертация состоит из введения и пяти глав. Текст диссертации изложен на 104 страницах. Список литературы содержит 33 наименования.

1. Л.Д.Беклемишев, О классификации пропозициональных логик доказуемости, Изв. АН СССР, Серил матем., т. 53, 5 (1989), с. 915-943.

2. E. Золин, Секвенциальные рефлексивные логики разрешимости, Мат. заметки, 2002, т. 71, вып. 6, с. 798-814.

3. Е. Золин, Секвенциальная логика арифметической разрешимости, Вестн. Моск. ун-та. Серия 1. Математика. Механика. 2001. № б, с. 43-48.

4. Г.Е.Минц, Системы Льюиса и система Т (1965-1973). — В кн.: Р. Фейс, Модальная логика. М.: Наука, 1974, с. 423-509.

5. Орлов И. Е., Исчисление совместности предложений. Мат. сборник, 1928, т. 35, № 3, pp. 263-286.

6. S. А^ётоу, Logic of Proofs, Annals of Pure and Applied Logic, vol. 67 (1994), pp. 29-59.

7. A.Avron, On Modal Systems Having Arithmetical Interpretation, The Journal of Symbolic Logic, vol. 49 (1984), num. 3, pp. 935-942.

8. L. D. Beklemishev, Classification of Propositional Provability Logics. Amer. Math. Soc. Transl. (2), 192:1-56.

9. P.Blackburn, M. de Rijke and Y.Venema. Modal Logic. A Textbook. Unpublished manuscript. CWI, Amsterdam, 1994.

10. G.Boolos, The Logic of Provability. Cambridge University Press, 1993.

11. A. Chagrov, M. Zakharyaschev, Modal Logic, Oxford Science Publications, 1997.

12. M. J. Cresswell, Necessity and contingency, Studia Logica, vol. 47 (1988), pp. 145-149.

13. J.N.Crossley (ed). Algebra and Logic. Springer Lecture Notes in Mathematics, 450. Berlin, 1975.15lK.G6del, Eine Interpretation des intuitionistischen Aussagenkalkuls, Ergebnisse Math. Colloc., Bd. 4 (1933), S. 39-40.

14. R. I. Goldblatt, S. K. Thomason, Axiomatic classes in propositional modal logic. In 14], pp.163-173.

15. I. L. Humberstone, The logic of non-contingency, Notre Dame Journal of Formal Logic, 1995, 36(2):214-229.

16. S.T.Kuhn, abstract in "Mathematical Reviews", 1996g:03030.

17. S.T.Kuhn, Minimal non-contingency logic, Notre Dame Journal of Formal Logic, 1995, 36(2):230-234.

18. M.H.Lob, Solution of a problem of Leon Henkin, Journal of Symbolic Logic, 20 (1955), 115-118.

19. D.Makinson, Some embedding theorems for modal logic, Notre Dame Journal of Formal Logic, 1971, 12(2):252-254.

20. Н. Montgomery, R. Routley, Contingency and non-contingency bases for normal modal logics, Logique et analyse, vol. 9 (1966), pp. 318-328.

21. H. Montgomery, R. Routley, Noncontingency axioms for 54 and 55, Logique et analyse, vol. 11 (1968), pp. 422-424.

22. H. Montgomery, R. Routley, Modalities is a sequence of normal non-contingency modal systems, Logique et analyse, vol. 12 (1969), pp. 225— 227.

23. C. Mortensen, A sequence of normal modal systems with non-contingency bases, Logique et Analyse, vol. 19 (1976), pp. 341-344.

24. E. Nogina, Logic of Proofs with Strong Provability Operator. International Conference on Proof Theory, Provability Logic and Computation (PPC'94), Berne, Switzeland, 1994, pp. 1-22.

25. M. Ohnishi, K.Matsumoto, Gentzen method in modal calculi, Osaka Math. /., vol. 9 (1957), num. 2, pp. 113-130. (Correction: Osaka Math. J., vol. 10 (1958), num. 1, p. 147.)

26. M. Ohnishi, K.Matsumoto, Gentzen method in modal calculi II, Osaka Math. J., vol. 11 (1959), num. 2, pp. 115-120.

27. R. M. Smullyan, Analytic Cut, The Journal of Symbolic Logic, 33 (1968), pp. 560-564.

28. R. Solovay, Provability interpretations of modal logics, Israel Journal of Mathematics, vol. 25 (1976), pp. 287-304.

29. M. Takano, Subformula property as a substitute for cut elimination in modal propositional logics, Mathematica Japonica, vol. 37 (1992), num. 6, pp. 1129-1145.

30. E. Zolin, Completeness and Definability in the Logic of Noncontingency, Notre Dame Journal of Formal Logic, 1999, vol. 40, № 4, pp. 533-547.Библиография 104

31. Е. Zolin, Infinitarу Definability of Necessity in Terms of Contingency, Proceedings of ESSLLI Student Session. — Finland, Helsinki, 13-24 August 2001, pp. 310-319.