Приложение семантики Крипке к исследованию правил вывода тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

На правах рукописи

БЕЗГАЧЕВА ЮЛИЯ ВИКТОРОВНА

УДК 517.11

ПРИЛОЖЕНИЕ СЕМАНТИКИ КРИПКЕ К ИССЛЕДОВАНИЮ ПРАВИЛ ВЫВОДА

01.01.06 — математическая логика, алгебра и теория чисел

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Красноярск-1998

Работа выполнена в Красноярском государственном университете

Научный руководитель доктор физико-математических наук,

профессор РЫБАКОВ В.В.

Официальные оппоненты: доктор физико-математических наук,

профессор БЕЛЯЕВ В.В. доктор физико-математических наук, профессор ПАЛЬЧУНОВ Д.Е.

Ведущая организация Иркутский государственный

университет, г. Иркутск

Защита состоится " ¿3" QVtXiiSpjL 1998 г. в tb часов на заседании диссертационного совета Д-064.61.02 в Красноярском государственном университете по адресу 660041, г. Красноярск, пр. Свободный, 79.

С диссертацией можно ознакомиться в библиотеке Красноярского государственного университета.

Автореферат разослан " -2- ^ " QJlAAXjJfj9JL 1998 г.

Ученый секретарь диссертационного совета

кандидат физико-математических наук [уЛА/ Бабенышев C.B.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Применение математического аппарата в логических исследованиях основано на введении математического синтаксиса — постулировании аксиоматических систем — и фиксировании семантического аппарата, а именно описании адекватных моделей ллп логик. Этот подход практиковался с начала нашего века и был заложен в работах Гильберта, Лукасевича, Генцена, Эрбрана и Тарского. Аксиоматическая система задается фиксированием аксиом и правил вывода. Широко распространенная практика состоит в варьировании аксиом, что позволяет описывать различные логические системы. Исследуя выбранную логику, естественным представляется по возможности наиболее полно обогатить аксиоматическую систему с целью сокращения процесса доказательства. Обычно для этого применяются производные правила вывода. Но еще П.Лоренцем было замечено, что каждая логика обладает наибольшим классом правил вывода, совместимых с доказуемостью в данной логике.

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

Общая проблема допустимости правил вывода заключается в следующем: для любого данного правила вывода определить, допустимо ли оно в заданной формальной системе. Если в классическом исчислении высказываний проблема допустимости правил вывода решается тривиально, то уже случай интуиционистской пропозициональной логики потребовал разработки сложной техники. Интерес к интуиционизму был вызван связями с основаниями математики. В 40-е годы П.С. Новиков отмечал в своих

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

Вопрос о существовании алгоритма, распознающего допустимость правил вывода, был поставлен Кузнецовым А.В., схожая проблема была включена в обзор проблем Фридмана ([12], проблема 40). В 1977 году А.И. Цит-киным [9] были найдены критерии допустимости для правил специального вида. Им же были описаны модусно предполные суперинтуиционистские логики [10]. Но сама проблема Кузнецова-Фридмана разрешимости по допустимости в интуиционистском исчислении высказываний оставалась открытой. Аналогичная проблема также актуальна для модальных логик. Допустимость и производность специальных правил в логике Льюиса Б5 исследовалась Портом [16, 17] в 1981 году.

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

предтабличных, там же был поставлен вопрос о проблеме допустимости в "слабых" логиках [6]. Среди логик фиксированного слоя п наименьшей (самой слабой) является логика S4 + <Tfc [2, 3]. Алгоритмический критерий допустимости для логик S4 + (Jk был найден Рыбаковым В.В. в 1984 году

[7]. В том же году была доказана разрешимость проблемы допустимости для целого класса логик — логик, расширяющих S4.3 [8].

В [6] было замечено, что правило вывода а/ß допустимо в суперинтуиционистской логике А Э Int, тогда и только тогда, когда правило T(a)/T(ß) допустимо в <т(А) — наибольшем модальном напарнике А, где Т(а) перевод Гёделя-МакКинси-Тарского интуиционистской формулы а в модальную (см. например [1]). Появилась надежда, что проблему допустимости в Int можно решить, доказав разрешимость проблемы допустимости в одной из модальных логик яруса p_1(Int). В 1984 году Рыбаковым В.В.

[8] был найден алгоритмический критерий допустимости правил вывода в модальной системе S4 и интуиционистской логике Int. Одновременно были получены алгебраические аналоги этих результатов — разрешимость универсальных теорий свободной алгебры замыканий и свободной псевдобулевой алгебры. Суть метода, введенного в [8], заключается в том, что для всякого правила вывода в исследуемых логиках существует конечное, с точностью до изоморфизма, множество конечных моделей Крипке специального вида, на элементах которого можно проверять истинность правила, для выяснения его допустимости.

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

Другой подход к изучению формальных исчислений связан с исследованием утверждений, не выводимых в данной логике. Идея такого подхода присутствует уже в работах Аристотеля, который рассматривал правило вывода, называемое "modus tollens": если А влечет В, а В отвергается, то А тоже должно быть отвергнуто. Лукасевичем была поставлена общая проблема построения дедуктивной системы утверждений, неистинных в данной теории. Позднее эта тематика была развита в работах Слупецки и Брилла, Крайзеля и Патнема, Дуткевича [11], Ишимото и Кобаяши [15]. Шкурой был предложен метод построения таких систем для логик эквивалентности, построены системы опровержения для некоторых специальных логик [18, 19, 20, 21] а Горанко [13] описывал системы опровержения для логик К, Т, К А, KW, SAGrz, существенно опираясь на особенности семантической характеризации.

Цель работы

1) Описать алгоритмы распознавания допустимых правил вывода в линейных финитно аппроксимируемых временных логиках как в естественном обобщении модальных логик.

2) Изучить допустимые правила вывода в модальных системах ширины 2.

3) Описать принцип построения аксиоматических систем опровержения (refutation systems) на основе техники исследования допустимых правил вывода.

Методика исследования. В исследовании применяются общие методы теоретико-модельной и алгебраической семантики для модальных и временных логик, преимущественно используется семантика Крипке.

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

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

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

• XI межреспубликанской конференции по математической логике (Казань, 1992),

• III международной конференции по алгебре памяти Каргаполова (Красноярск, 1993),

• международной конференции по математической логике посвященной 85-летию со дня рождения А.И. Мальцева (Новосибирск, 1994),

• русско-японском логическом коллоквиуме N81/95 (Иркутск, 1995),

• на международной конференции "Мальцевские чтения" (Новосибирск, 1997)

• на заседаниях семинара по неклассическим логикам при НГУ (Новосибирск)

• на заседаниях Красноярского алгебраического семинара.

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

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

СОДЕРЖАНИЕ РАБОТЫ

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

В первой главе приведены необходимые предварительные сведения из области модальных и временных логик, указаны основные результаты из области семантики Крипке.

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

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

В разделе 1.3 вводится понятие п-характеристической модели логики и описывается общая процедура построения таких моделей. В разделе 1.4 дано определение допустимых правил вывода и приведен критерий допустимости правил вывода через п-характеристические модели.

Во второй главе изложены основные результаты автора, относящиеся к построению алгоритмических критериев допустимости во временных логиках ЫпТСгг,ЫпТ*, ЫпТ и родственных им классах линейных и нелинейных временных логик.

В разделе 2.1 описана аксиоматическая система и характеристический

класс фреймов для логики ЫпТСгг. Логика ЫпТСгг определена как расширение наименьшей нормальной бимодальной логики К2 посредством следующих аксиом:

Со : ОьПнА -> Л, С1 : ОдОьА -» А;

Уо : ПьА □¿□¿Л, Уг : □ дЛ ПдОдЛ; Т0 : ПьА А, Г, : аяА -> А;

Ь0 : ПА -> □¿□дЛ, : ПЛОдП^Л;

<?Г20 : □¿(□¿(Л -> □¿Л) -» Л) -> Л, вгг 1 : Пд(Пд(Л ОдЛ) Л) -)■ Л.

В разделе 2.2 эффективно строится п-характеристическая модель М„с для логики ЫпТСгг и доказываются следующие результаты:

ТЕОРЕМА 2.3 Модель А/„с является п-характеристической моделью для логики ЫпТСгг.

ТЕОРЕМА 2.5 Все элементы модели М„с являются формульными.

В разделе 2.3 на основании приведенных выше теорем решается проблема допустимости и строится алгоритмический критерий.

ТЕОРЕМА 2.6 Логика ЫпТСгг разрешима по допустимости.

ТЕОРЕМА 2.7 Правило вывода г не допустимо в логике ЫпТСгг тогда и только тогда, когда некоторая конечная линейно упорядоченная прайоровская модель М с добавленным изолированным элементом и общим числом элементов ^ 2 * © 1 опровергает г.

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

ТЕОРЕМА 2.14 Логика ЫпТ разрешима по допустимости.

ТЕОРЕМА 2.15 Правило вывода г, зависящее от п переменных, не допустимо в логике LinT тогда и только тогда, когда некоторая рефлексивная транзитивная упорядоченная прайоровская модель М, состоящая из конечного числа конечных сгустков, с добавленным изолированным элементом и общим числом элементов ^ 2 * 2SubM * 2" ф 1 опровергает г.

Обозначим Lin* логику, характеристический класс которой является подклассом характеристического класса для Lin, удовлетворяющим следующему условию: его элементами являются конечные транзитивные упорядоченные прайоровские фреймы, не содержащие соседних иррефлек-сивных элементов.

ТЕОРЕМА 2.17 Логика Lin* разрешима по допустимости.

ТЕОРЕМА 2.18 Пусть Л — линейная финитно аппроксимируемая временная логика и Lin* С Л или LinT С Л. Тогда логика Л разрешима по допустимости.

ТЕОРЕМА 2.19 Пусть Л — транзитивная финитно аппроксимируемая временная логика, заданная некоторым эффективно описываемым бесконечным семейством фреймов SF, удовлетворяющих следующему условию: для любого фрейма F € SF любая редукция фрейма F также принадлежит семейству SF. Тогда логика Л разрешима по допустимости.

В главе 3 решается проблема допустимости для конечно аксиоматизируемых финитно аппроксимируемых модальных логик ширины 2. В разделе 3.1 дано определение логик ширины 2, приведены примеры фреймов, задающих такие логики. В разделе 3.2 описан и обоснован процесс построения n-характеристических моделей с формульными элементами. В разделе 3.3 доказан алгоритмический критерий распознавания допустимости.

ТЕОРЕМА 3.5 Для любой транзитивной финитно аппроксимируемой

конечно аксиоматизируемой логики А ширины 2 существует алгоритм, определяющий допустимость правил вывода.

В главе 4 даны основные определения, относящиеся к системам опровержения, описан общий принцип построения таких систем с использованием п-характеристических моделей, приведены системы опровержения для логик 84.1 и Б4.2.

Основным результатом этой главы является следующая

ТЕОРЕМА 4.3 Пусть Л — некоторая транзитивная финитно аппроксимируемая конечно аксиоматизируемая модальная логика. Тогда можно эффективно построить бесконечную дедуктивную систему опровержения для логики Л.

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ

Основные результаты диссертации состоят в следующем:

1) Построены критерии допустимости правил вывода и доказана разрешимость проблемы допустимости во временных линейных логиках ЫпТ, ЫпТвгг, и ЫпТ*

2) Построен критерий допустимости правил вывода для временных логик, заданных специальной системой конечных фреймов.

3) Доказана разрешимость проблемы допустимости правил вывода в транзитивных конечно аксиоматизируемых финитно аппроксимируемых модальных логиках ширины 2.

4) Описан способ построения систем опровержения для транзитивных

конечно аксиоматизируемых финитно аппроксимируемых модальных логик, построены системы опровержения для логик 54.1 и 54.2.

Литература

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

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

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

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

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

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

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

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

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

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

[11] Dutkiewicz R. The method of axiomatic rejection for the intuitionistic propositional logic. // Studia Logica, XLVIII. 1989. V. 4. P. 449-460.

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

[13] Goranko V. Refutation system in modal logic // Studia Logica. 1994. V. 53. №2. P. 299-325.

[14] Harrop R. Concerning formulas of the types A В V С, A —> БхВ(х) in intuitionistic formal systems // The Journal of Symbolic Logic. 1960. V. 25. №1. P. 27-32.

[15] Inoue Т., Ishimoto A., Kobayashi M. Axiomatic rejection for the propositionalfragment of Lesnewski ontology // Soviet-Japan Symposium "Lesnewski's ontology and it's application", Moscow 1990.

[16] Port J. The deducibilities of S5 // Journal of Phylosophical Logic. 1981. V. 10. P. 409-422.

[17] Port J. Axiomatization and independence in S4 and S5 // Reports on Mathematical Logic. 1983. V. 16. P. 23-33.

[18] Skura T. A completesyntactial characterization of the intuitionistic logic // Reports on mathematical logic. 1983. №23. P. 75-80.

[19] Skura T. On pure refutation formulation of sentential logics // Bull, of Sect, of Logic. 1990. V.19 №3. P. 102-107.

[20] Skura T. Refutation rules for three modal logics // Bull, of Sect, of Logic. 1992. V.21 №1. P. 31-32.

[21] Skura Т. On decision procedure for sentential logics // Studia Logica.

1991. L №2. P. 173-179.

РАБОТЫ АВТОРА ПО ТЕМЕ ДИССЕРТАЦИИ

1. Безгачева Ю.В. О временной логике LinTDum // XI межреспубликанская конференция по математической логике: Тез. сообщений. Казанский ун-т. — Казань, 1992. С. 17.

2. Безгачева Ю.В. Временные логики линейного действия // Материалы XXXI международной научной студенческой конференции. Математика. Новосиб. ун-т. Новосибирск, 1993. С. 6-9.

3. Безгачева Ю.В. Допустимость правил вывода в логиках ширины 2 // Международная конференция по математической логике: Тез. сообщений. Новосиб. ун-т. — Новосибирск, 1994. С. 19-21.

4. Безгачева Ю.В. Исследование многообразия, соответствующего логике LinTDum // III международная конференция по алгебре: Тез. докл. Красноярский ун-т. — Красноярск, 1993. С. 38.

5. Julia V. Bezgacheva Refutation Systems for Logics S4.1 and S4.2 // NSL'95: Abstracts. University of Irkutsk. — Irkutsk, 1995. PP. 16-18. Ha англ. яз.

6. Julia V. Bezgacheva Admissibility of Inference Rules in Modal Logics of Width 2 and Some Properties of Logics LinTGrz and LinTDum // Logic Colloqium'95: Abstracts. Technion Israel Institute of Technology, University of Haifa. — Haifa, 1995. PROOF-61. На англ. яз.

7. Julia V. Bezgacheva Admissible rules for temporal logic LinTGrz //Bulletin of the Section of Logic, University of Lodz, Volume 26, Number 2. 1997. PP. 60-67. На англ. яз.

8. Безгачева Ю.В. Допустимость правил вывода в логиках, заданных некоторыми классами конечных фреймов // Деп. ВИНИТИ 27.07.98 N 2376-В98, 26 с.

9. Безгачева Ю.В. Допустимые правил вывода логики ЫпТвгг // Сборник грантового центра НИИ МИОО — Новосибирск, 1998.

10. Безгачева Ю.В. Построение систем опровержения // Деп. ВИНИТИ 27.07.98 N 2375-В98, 10 с.

11. Безгачева Ю.В. Допустимость правил вывода в логиках ширины 2// Деп. ВИНИТИ 27.07.98 N 2377-В98, 11 с.