Логика Гейтинга - Оккама и негативные модальности тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

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

Дробышевич Сергей Андреевич

ЛОГИКА РЕЙТИНГА — ОККАМА И НЕГАТИВНЫЕ МОДАЛЬНОСТИ

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

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

31 ОКТ 2013

Новосибирск-2013

005536473

005536473

Работа выполнена в Федеральном государственном бюджетном учреждении науки Институте математики им. С. Л. Соболева Сибирского отделения Российской академии наук.

Научный руководитель:

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

Максимова Лариса Львовна, доктор физико-математических наук, профессор, Федеральное государственное бюджетное учреждение науки Институт математики им. С. Л. Соболева Сибирского отделения Российской академии наук, главный научный сотрудник;

Карпенко Анастасия Валерьевна, кандидат физико-математических наук, Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Новосибирский национальный исследовательский государственный университет», старший преподаватель.

Ведущая организация: Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования «Алтайский государственный университет».

Защита состоится 16 ноября 2013 г. в 16 часов 00 минут на заседании диссертационного совета Д 003.015.02 при Федеральном государственном бюджетном учреждении науки Институте математики им. С. Л. Соболева Сибирского отделения Российской академии наук по адресу: 630090, Новосибирск, пр. Акад. Коптюга, 4.

С диссертацией можно ознакомиться в библиотеке Федерального государственного бюджетного учреждения науки Института математики им. С. Л. Соболева Сибирского отделения Российской академии наук.

Автореферат разослан « » октября 2013 г.

Учёный секретарь диссертационного совета кандидат физико-математических наук

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

Тематика диссертации. Результаты, изложенные в диссертации, связаны с так называемой логикой Гейтинга — Оккама N*. Логика N* была введена в качестве дедуктивной базы для фундированной семантики логических программ с отрицаниями в [5], где она была определена как расширение логики К. Дошена N. Логика N [9, 10], в свою очередь, представляет собой попытку сформулировать логику, отрицание в которой было бы слабее, чем отрицание минимальной логики Иохансонна J — для этого роль связки отрицания в логике играет модальный оператор невозможности весьма общего вида, тогда как позитивные связки конъюнкции А, дизъюнкции V и импликации —> интерпретируются как в позитивной логике Pos.

Аксиомы логики Гейтинга — Оккама позволили определить в ней интуиционистскую константу абсурда ±, в связи с чем в диссертации логика N* задана как интуиционистская модальная логика, немодальный фрагмент которой совпадает с интуиционистской логикой Int, сформулированной в языке £х := {A, V, —>, J_}, а единственное отрицание обозначается и представляет собой негативный модальный оператор. Как обычно, интуиционистской отрицание может быть определено через константу абсурда как —А := А —> _L.

Наиболее распространёнными операторами модальных логик являются позитивные модальные операторы необходимости и возможности, на ряду с которыми можно рассматривать также дуальные негативные модальные операторы невозможности и не-необходимости. Как известно, над классической логикой все четыре типа операторов могут быть определены друг через друга при помощи классического отрицания, что позволяет свести изучение нормальных операторов перечисленных типов к изучению всевозможных расширений наименьшей классической нормальной модальной логики К, названной в честь С. Крипке.

Для интуиционистских модальных логик не существует общепризнанного аналога логики К, задающего базу для изучения нормальных модальных операторов, тем не менее, были предприняты различные попытки ввести общую теорию интуиционистских модальных логик. Так, например, В. Сотировым была определена интуиционистская модальная логика IM PL [19], единственный модальный оператор которой задавался исключительно правилом экстенсиональности. Другой подход был предложен К. Дошеном и М. Божичем [3, 8], которые ввели че-

тыре различные системы интуиционистских модальных логик, каждая из которых соответствовала своему типу модального оператора: НКО — необходимости, НК0 — возможности, НКО' — не-необходимости и НКО' — невозможности. При этом предполагалось, что каждая из четырёх систем будет играть ту же роль для интуиционистских модальных логик соответствующих оператору заданного вида, как и логика К для классических модальных логик. В диссертации используется подход Божича и Дошена для работы с интуиционистскими модальными логиками, при этом четыре перечисленные логики мы будем называть логиками Гейтинга — Крипке. В качестве общего обзора по интуиционистским модальным логикам можно порекомендовать [24].

Помимо модального оператора невозможности, модальный оператор не-необходимости также может служить естественным обобщением понятия отрицания. Такой подход можно найти, например, в работе Р. Сильвана [20], где была введена логика ССШ, из семантической интерпретации которой видно, что отрицание в ней является некоторым модальным оператором не-необходимости.

Оба подхода (т.е. отрицание как невозможность и отрицание как не-необходимость) присутствуют в работах Д. Вакарелова [21, 22] (см. также [23]), которым была предпринята попытка ввести общую (хотя и не исчерпывающую) классификацию отрицаний. Базовыми типами отрицаний в классификации Вакарелова являлись так называемые регулярные и корегулярные отрицания, при этом отрицание первого типа можно трактовать как оператор невозможности, а второго — как оператор не-необходимости. Стоит отметить, что Вакарелов строил свою теорию отрицаний над дистрибутивными логиками (т.е. логиками, чья алгебраическая семантика задаётся дистрибутивными решётками) для того, чтобы избавиться от влияния характера импликации на отрицание. Однако эта теория легко может быть обобщена до интуиционистских или классических модальных логик.

Интересной особенностью отрицания логики N* является то, что новые (относительно логики ЛГ) аксиомы логики позволяют интерпретировать отрицание в ней не только как модальный оператор невозможности, но и как модальный оператор не-необходимости. Более того, отрицание в логике N* в точности является оператором, объединяющим свойства оператора невозможности логики НКО' и оператора ненеобходимости логики НКО'. В классификации Вакарелова отрицание логики ТУ* соответствует отрицанию, которое является одновременно

нормальным и конормальным. В данной диссертации мы будем называть отрицание логики отрицанием Раутли в связи с тем, что для его интерпретации в семантике Крипке используется антимонотонная функция * — подход, широко распространённый в работах по релевантным логикам (см., например, [17]).

Одним из фундаментальных свойств логик является разрешимость. Логика называется разрешимой, если существует процедура, позволяющая по произвольной формуле определить, принадлежит ли она логике. Часто доказательство разрешимости логики сводится к доказательству того, что она обладает свойством конечных моделей, то есть что она полна относительно некоторого класса конечных шкал Крипке. В диссертации установлено, что логика ЛГ* обладает свойством конечных моделей и разрешима, причём представлено два независимых доказательства этих утверждений. В первом строится гибридное исчисление для логики, то есть исчисление, в синтаксисе которого явным образом присутствуют элементы семантики логики. Анализ класса конечных шкал, относительно которого получена полнота этим методом, позволяет провести более простое доказательство, основанное на методе фильтрации для интуиционистской логики и классических модальных логик [6].

Доказав полноту логики относительно какого-то класса шкал, естественным представляется вопрос о том, можно ли получить сильную полноту логики относительно данного класса. В диссертации рассмотрена более широкая ситуация и показано, что не существует класса конечных шкал, относительно которого сильно полна логика ЛГ*. Приведённое доказательство основано на теореме Джёбяка [12], который показал, что всякая нетривиальная суперинтуиционистская логика или классическая нормальная модальная логика сильно полна относительно некоторого класса конечных шкал тогда и только тогда, когда она таблична. Напомним, что логика таблична, если она задаётся одной конечной шкалой. В диссертации доказано аналогичное утверждение для расширений логики N*, названое теоремой Джёбяка для N*.

С.П. Одинцовым было доказано [14], что оператор --> логики ЛР, полученный композицией интуиционистского отрицания и отрицания Раутли, является частным случаем оператора необходимости. Этот оператор, кроме того, был использован в [14] для формулировки критерия подпрямой неразложимости алгебр Гейтинга — Оккама, которые задают адекватную алгебраическую семантику логики N*. Композиция операторов является одним из простейших способов введения новых опера-

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

Как известно, интуиционистское отрицание само по себе может быть интерпретировано как модальный оператор невозможности [9]. Кроме того, было показано, что оператор двойного интуиционистского отрицания является частным случаем оператора необходимости. Этот результат был получен независимо Сотировым [18] и Дошеном [7, 2]. Одним из приложений оператора двойного интуиционистского отрицания является теорема Гливенко (см., например, [6, теорема 2.47]), которая гласит, что формула А принадлежит классической логике тогда и только тогда, когда формула — — А принадлежит интуиционистской. Аналог теоремы Гливенко для расширений логики N* был доказан в [15]. В связи с вышесказанным, интерес представляет вопрос об аксиоматизации оператора двойного отрицания Раутли. В диссертации сформулирована аксиоматизация данного оператора в качестве нормального расширения № логики НКО.

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

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

Методы исследования. В диссертации используются методы работы с семантикой Крипке [6], методы универсальной алгебры [4] для работы с алгебраической семантикой логики N*, а также некоторые результаты из области классической логики первого порядка [1]. Кроме того, построенные в диссертации гибридные исчисления основаны на технике табличных исчислений, развитой в [16].

Основные результаты диссертации.

1. Доказано, что логика N* обладает свойством конечных моделей и разрешима. Построено гибридное исчисление для логики N*, доказаны утверждения о его корректности и полноте относительно семантики логики (опубликовано в [30]).

2. Доказан аналог теоремы Джёбяка для расширений логики N*. А именно, показано, что всякое нормальное расширение L логики N* является сильно полным относительно некоторого класса конечных шкал тогда и только тогда, когда L — табличная логика (опубликовано в [31]).

3. Получена аксиоматизация композиции интуиционистского отрицания и отрицания Раутли —> в логике N' в качестве оператора необходимости (опубликовано в [33]).

4. Получена аксиоматизация оператора двойного отрицания Раутли -■-I в качестве оператора необходимости (опубликовано в [32]).

Второй из основных результатов получен совместно с С. П. Одинцовым при равном участии обеих сторон, остальные результаты получены автором самостоятельно.

Апробация работы. Результаты диссертации докладывались на международных конференциях: «Мальцевские чтения» (Новосибирск, 2009, 2010, 2012), «Logic Colloquium 2011» (Барселона, Испания), «Advances in Modal Logic 2012» (Копенгаген, Дания). Также результаты диссертации докладывались на совместных семинарах ИМ СО РАН и НГУ «Нестандартные логики» и «Алгебра и логика».

Публикации. Основные результаты опубликованы в работах [25-33], из них [30-33] входят в перечень ВАК российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук. Работа [31] написана совместно с С. П. Одинцовым при равном участии обеих сторон.

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

ратуры состоит из 39 наименований, в том числе 9 работ автора по теме диссертации. Объём работы — 121 страница. Все утверждения (предложения, леммы, теоремы и следствия) пронумерованы тремя числами: первое является номером главы, второе — номером раздела, третье — порядковым номером утверждения в рамках указанного раздела.

Глава 1 посвящена необходимым предварительным сведениям.

В разделе 1.1 сформулированы интуиционистская логика Int [6] в языке С1- = {Л, V, —», J-}, четыре интуиционистские модальные логики Гейтинга — Крипке НКП, НКО, НКП' и НКО' [3, 8], а также логика Гейтинга — Оккама N* [14]. Множества формул соответствующих языков определяются стандартным образом при помощи множества пропозициональных переменных Prop. Заданная в диссертации аксиоматика логики N* в языке СГ = £хи{-|} получается добавлением к аксиоматике Int правила контрапозиции для отрицания Раутли, а также аксиом

Под логикой в диссертации мы понимаем множество её теорем, отношение выводимости (названное а работе отношением синтаксического следования) при таком подходе является производным.

Раздел 1.2 посвящён семантике Крипке для перечисленных логик, /«¿-шкалы представляют собой частично упорядоченные множества. НК(5-шкалы для 6 6 {□, О, 0'} формулируются как /«¿-шкалы с дополнительным бинарным отношением достижимости Я для интерпретации соответствующего модального оператора, удовлетворяющим условию согласования с частичным порядком:

а ЛГ*-шкалы — как /«¿-шкалы с дополнительной анти-монотонной функцией * на множестве миров, используемой для интерпретации отрицания Раутли. Модели соответствующего типа задаются как шкалы вместе с означиванием V, удовлетворяющим условию монотонности

ОБЗОР СОДЕРЖАНИЯ ДИССЕРТАЦИИ

N1. —ip Л—iq—t -i(p V q)\ N3. -.(р A <?)->• V -Iq;

N2. - - (p -»■ p); N4. - -I(p -> p).

Vx, y,z(x <y и yRz => xRz) — в случае 5 e {□, 0'}; Vx, y,z(x < у и xRz => yRz) — в случае S e {0, □'};

Vx, у (x 6 v(p) и x < у => у € v(p)), где p 6 Prop.

Сформулировны утверждения о полноте логик относительно заданных семантик. Далее в разделе приведены основные определения и утверждения, составляющие метод канонических моделей для доказательства полноты логик на примере логик Гейтинга — Крипке. В конце раздела приведено вложение логики N* в логику первого порядка, явным образом использующее семантику Крипке для логики, при помощи так называемой стандартной трансляции.

В разделе 1.3 изложены основные сведения, касающееся алгебраической семантики логики N* [14]. Как уже было упомянуто, соответствующие алгебры носят название алгебр Гейтинга — Оккама (или HO-алгебр) и представляют собой алгебры Гейтинга с дополнительным оператором отрицания, удовлетворяющим тождествам

->(ж V у) = -<х А —'2/, -'0 = 1,

->(ж А у) = -<х V -1 у, -il = 0.

В разделе сформулирована теорема о полноте логики N* относительно ЯО-алгебр, а также дуальный изоморфизм между классом всех нормальных расширений логики и классом всех подмногообразий многообразия всех ЯО-алгебр. Далее изложен критерий подпрямой неразложимости ЯО-алгебр, в котором явным образом участвует оператор, полученный композицией интуиционистского отрицания и отрицания Раутли. В конце раздела задана связь между алгебраической семантикой и семантикой Крипке для логики Гейтинга — Оккама.

Раздел 1.4 посвящён гибридному исчислению для Int, которое позднее будет расширено до исчисления для логики N* и ещё одной интуиционистской модальной логики. Исчисление представляет собой формализованную процедуру построения контр-модели для произвольной формулы и основано на гибридном исчислении для логик описаний [16], причём в его формулировке использованы идеи Р. Дыкхова [11] относительно того, как задать исчисление для интуиционистской логики, не требующее отдельного механизма для поиска циклов в выводе. Доказанные утверждения о полноте и корректности исчисления могут быть использованы для получения нового доказательства того, что интуиционистская логика обладает свойством конечных моделей и разрешима.

Предметом изучения главы 2 является класс конечных шкал для логики Гейтинга — Оккама.

В разделе 2.1 исчисление, заданное в разделе 1.4 для интуиционистской логики, расширено до исчисления для ЛГ*, доказаны утверждения о его полноте и корректности относительно заданной семантики, откуда выведено, что логика полна относительно некоторого класса конечных шкал специального вида и разрешима.

Класс шкал, относительно которого получена полнота логики N* в разделе 2.1, использован в разделе 2.2 для того, чтобы доказать её разрешимость более простым способом, основанным на методе фильтрации для интуиционистской логики и классических нормальных модальных логик [6]. Основной особенностью данного метода фильтрации является то, что в нём использовано не одно, а сразу несколько отношений эквивалентности, по которым факторизуется данная модель. Заметим, что класс шкал, относительно которого получена полнота логики N* в данном разделе, в точности совпадает с классом шкал, относительно которого получена полнота в разделе 2.1.

В разделе 2.3 для расширений логики ТУ* доказан аналог теоремы Джёбяка [12]. А именно, доказано, что всякое нормальное расширение логики ТУ* полно относительно некоторого класса конечных шкал тогда и только тогда, когда оно является табличной логикой. Отсюда выводится, что не существует класса конечных шкал, относительно которого была бы сильно полна логика N*. В частности, таковым не является и класс шкал, относительно которого получена слабая полнота логики в разделах 2.1 и 2.2.

В главе 3 получена аксиоматизация композиции интуиционистского отрицания и отрицания Раутли —-> в качестве оператора необходимости.

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

В разделе 3.2 получена аксиоматизация композиции —□' интуиционистского отрицания и оператора не-необходимости логики НК□' в качестве оператора необходимости. Для этого сначала сформулировано нормальное расширение НК^ логики НКО и выделен класс НКП-шкал, относительно которого полна логика НК^. Затем доказано, что логика НК^ задаёт аксиоматизацию упомянутого оператора —□'. Точ-

нее, показано, что для всякой формулы А имеет место

А е НК° ти(А) е НКП',

где г„ — трансляция, такая что i) ти(р) = р для р € Prop; ii) r„(±) = _L; iii) ти(А ° В) = ти(А) о ти{В) для о e {A,V,->} и iv) ти{ПА) = 'ти{А). Ключевым моментом в доказательстве является сведениие семантики Крипке логики НК^ к семантике логики НКП'.

В разделе 3.3 сначала показано, что композиция —0' интуиционистского отрицания и невозможности в логике НК0' не является оператором необходимости, а затем сформулировано наименьшее расширение HKf логики НК0', в котором данная композиция оператором необходимости является, и выделен класс НК()'-шкал, относительно которого i полна логика. Аксиоматизация оператора -0' получена как нормальное

расширение НКР логики НКП.

В разделе 3.4 дано решение для основной задачи главы. Для начала сформулировано нормальное расширение HK^j? логики НКП и выделен класс НКП-шкал, относительно которого полна логика НКJ?. Для доказательства того, что логика НКj? задаёт аксиоматизацию композиции —-1 интуиционистского отрицания и отрицания Раутли, потребовалось получить полноту НКj? относительно класса конечных шкал специального вида, что стало возможным благодаря технике гибридных исчислений, развитой в разделе 2.1. Итак, в разделе задано гибридное исчисление для логики НКдоказаны утверждения о его корректности и полноте, откуда выведено, что логика НКj? полна относительно некоторого класса конечных Н/СП-шкал специального вида и разрешима. Затем этот класс конечных шкал использован для доказательства того, что логика НК{? действительно задаёт аксиоматизацию композиции —-1 интуиционистского отрицания и отрицания Раутли. Заметим, что выполнены включения

НКП С НК° С НК° С НК°,

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

Глава 4 посвящена аксиоматизации оператора ->-i двойного отрицания Раутли в качестве оператора необходимости.

В разделе 4.1 введено нормальное расширение АГ" логики НК□ и при помощи метода канонических моделей доказана её полнота относительно шкал, в которых для интерпретации оператора необходимости используется монотонная функция на множестве всех миров. Основной особенностью заданной логики является то, что оператор необходимости в ней объединяет свойства оператора необходимости логики НК□ и оператора возможности логики НК О-

В разделе 4.2 доказано свойство конечных моделей для АГ" относительно указанного типа шкал при помощи адаптации метода фильтрации, описанного в разделе 2.2. Из этого результата стандартным образом выведена разрешимость логики.

В разделе 4.3 доказано, что логика № задаёт аксиоматизацию оператора двойного отрицания Раутли в качестве оператора необходимости.

В разделе 4.4 проведено краткое сопоставление конструктивных свойств логик И* и А^, а именно доказано, что логика АГ' обладает дизъюнктивным свойством, тогда как логика Ы* не обладает ни дизъюнктивным свойством, ни конструктивным свойством отрицания.

Список литературы

[1] Ершов Ю.Л., Палютин Е. А. Математическая логика. Изд. 2-е, испр. и доп. М.: Наука, 1987. 336 с.

[2] Bozic М., DoSen К. Axiomatizations of intuitionistic double negation // Bull. Sect. Logic Univ. Lodz. 1983. V. 12, № 2. P. 99-104.

[3] Bozic M., DoSen K. Models for normal intuitionistic modal logics // Studia Logica. 1984. V. 43. P. 217-245.

[4] Burris S., Sankappanavar H.P. A course in universal algebra. Grad. Texts in Math., Vol. 78. New York: Springer, 1981. 276 p.

[5] Cabalar P., Odintsov S.P., Pearce D. Logical foundations of well-founded semantics // Principles of Knowledge Representation and Reasoning: Proceedings of the 10th International Conference (KR2006) / Eds. P. Doherty et al. Menlo Park: AAAI Press, 2006. P. 25-36.

[6] Chagrov A., Zakharyaschev M. Modal logic. Oxford: Clarendon Press, 1997. 624 p.

[7] DoSen K. Intuitionistic double negation as a necessity operator // Publ. Inst. Math. (Beograd)(N.S.). 1984. V. 35. № 49. P. 15-20.

[8] DoSen K. Negative modal operators in intuitionistic logic // Publ. Inst. Math. (Beograd)(N.S.). 1984. V. 35. P. 3-14.

[9] DoSen K. Negation as a modal operator // Rep. Math. Logic. 1986. V. 20. P. 15-28.

[10] DoSen K. Negation in the light of modal logic // What is negation? Appl. Log. Ser., V. 13. / Eds. D. Gabbay et al. Dordrecht: Kluwer Acad. Publ., P. 77-86.

[11] Dyckhoff R. Contraction-free sequent calculi for intuitionistic logic // J. Symbolic Logic. 1992. V. 57. P. 795-807.

[12] Dziobiak W. Strong completeness with respect to finite Kripke models // Studia Logica. 1981. V. 40. № 3. P. 249-252.

[13] Gabbay D. Semantical Investigations in Heyting's Intuitionistic Logic. Synthese Lib, vol. 148. Dordrecht: Kluwer Acad. Publ., 1981. 287 p.

[14] Odintsov S.P. Combining intuitionistic connectives and Eoutley negation // Sib. Électron. Math. Izv. 2010. V. 7. P. 21-41.

[15] Odintsov S.P. Glivenko theorem for iV*-extension // Sib. Électron. Math. Izv. 2011. V. 8. P. 365-368.

[16] Odintsov S. P., Wansing H. Inconsistency-tolerant description logic. Part II: A tableau algorithm for CACCc //J. Appl. Log. 2008. V. 6. P. 343-360.

[17] Routley R., Routley V. The semantics of first degree entailment // Nous. 1972. V. 6. P. 335-359.

[18] Sotirov V. The intuitionistic double negation is a modality // Abstracts of 7-th International Witgenstein Symp. 22-29 August 1982, Kircherg an Wechsel, Austria, 1982. P. 58.

[19] Sotirov V. Modal Theories with Intuitionistic Logic // Mathematical Logic, Proc. of the Conference Dedicated to the memory of A. A. Markov (1903-1979). Sofia, September 22-23. Bulgarian Acad, of sc., 1984. P. 139-171.

[20] Sylvan R. Variations on Da Costa C Systems and Dual-Intuitionistic Logics I. Analyses of Cu and CCU // Studia Logica. 1990. V. 49. P. 4765.

[21] Vakarelov D. Theory of Negation in Certain Logical Systems. Algebraic and Semantical Approach. Ph.D. dissertation, University of Warsaw, 1976.

[22] Vakarelov D. Consistency, Completeness and Negation // Paraconsistent Logics: Essays on the Inconsistent / Eds. G. Priest, R. Routley, J. Norman. Munchen: Philosophia Verlag, 1989. P. 328-363.

[23] Vakarelov D. The non-classical negation in the works of Helena Rasiowa and their impact on the theory of negation // Studia Logica. 2006. V. 85. P. 105-127.

[24] Wolter F., Zakharyaschev M. Intuitionistic Modal Logics // Logic and Foundations of Mathematics. Synthese Lib., Vol. 280. / Eds. A. Cantini, E. Casari, P. Minari. Dordrecht: Kluwer Acad. Publ., 1999. P. 227-238.

Работы автора по теме диссертации

Тезисы конференций

[25] Drobyshevich S.A. Decidability of logic N* // Abstracts, Maltsev Meeting 2009, Novosibirsk, Russia, August 24-28. P. 235.

[26] Drobyshevich S.A. Filtration for logic N* // Abstracts, Maltsev Meeting 2010, Novosibirsk, Russia, May 2-6. P. 41.

[27] Drobyshevich S.A. A necessity operator in logic N* // Abstracts, Maltsev Meeting 2012, Novosibirsk, Russia, November 12-16. P. 167.

[28] Drobyshevich S.A. A double negation operator in logic N* // Bull. Symbolic Logic. 2012. V. 18, № 3. P. 444-445.

[29] Drobyshevich S., Odintsov S. Some remarks on negative modalities // Short presentations, Advances in Modal Logic 2012, Copenhagen, Denmark, August 22-25. P. 28-32.

Оригинальные статьи

[30] Дробышевич С. А. Гибридное исчисление для логики N*, её конечная аппроксимируемость и разрешимость // Алгебра и логика. 2011. Т. 50, Вып. 3. С. 351-367.

[31] Дробышевич С. А., Одинцов С. П. Свойство конечных моделей для негативных модальностей // Сиб. электрон, матем. изв. 2013. Т. 10. С. 1-21.

[32] Дробышевич С. А. Оператор двойного отрицания в логике N* // Вестник НГУ. Серия: Матем., Механика, Информ. 2013. Т. 13, Вып. 4. С. 24-40.

[33] Дробышевич С. А. Композиция интуиционистского отрицания и негативных модальностей как оператор необходимости // Алгебра и логика. 2013. Т. 52, Вып. 3. С. 305-331.

Дробышевич Сергей Андреевич

ЛОГИКА ГЕЙТИНГА - ОККАМА И НЕГАТИВНЫЕ МОДАЛЬНОСТИ

Автореферат диссертации на соискание ученой степени кандидата физико-математических наук

Подписано в печать 01.10.13. Формат 60x84 1/16. Усл. печ. л. 1,0. Уч.-изд. л. 1,0. Тираж 100 экз. Заказ № 101.

Отпечатано в ООО «Омега Принт» 630090, Новосибирск, пр.Лаврентьева, 6

РОССИЙСКАЯ АКАДЕМИЯ НАУК СИБИРСКОЕ ОТДЕЛЕНИЕ ИНСТИТУТ МАТЕМАТИКИ им. С. Л. СОБОЛЕВА

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

04201364161

Дробышевич Сергей Андреевич

ЛОГИКА ГЕЙТИНГА-ОККАМА И НЕГАТИВНЫЕ МОДАЛЬНОСТИ

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

диссертация на соискание ученой степени кандидата физико-математических наук

)

Научный руководитель доктор физико-математических наук Одинцов Сергей Павлович

Новосибирск-2013

Оглавление

Введение 4

1 Предварительные сведения 15

1.1 Аксиоматизация логик..........................................15

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

1.3 Алгебраическая семантика iV* ................................28

1.4 Гибридное исчисление для Int................................33

2 Класс конечных Л^*-шкал 45

2.1 Гибридное исчисление для логики N*........................45

2.2 Фильтрация для N*............................................53

2.3 Теорема Джёбяка для N*......................................58

3 Композиция интуиционистского отрицания и негативных модальностей 64

3.1 Постановка задачи и

предварительные замечания....................................64

3.2 Интуиционистское отрицание и

не-необходимость................................................72

3.3 Интуиционистское отрицание и

невозможность..................................................77

3.3.1 Логика HKf............................................77

3.3.2 Логика HKf как аксиоматизация композиции интуиционистского отрицания и

невозможности..........................................83

3.4 Интуиционистское отрицание и

отрицание Раутли ..............................................88

3.4.1 Логика HKf............................................88

3.4.2 Свойство конечных моделей для HKf................91

3.4.3 Логика HKf как аксиоматизация композиции интуиционистского отрицания и

отрицания Раутли ...................100

4 Оператор двойного отрицания Раутли 103

4.1 Логика N»............................103

4.2 Свойство конечных моделей для N*.............108

4.3 iV" как аксиоматизация оператора

двойного отрицания Раутли..................111

4.4 Конструктивные свойства дгй и N*..............113

Литература 117

Введение

Результаты, изложенные в диссертации, так или иначе связаны с так называемой логикой Гейтинга-Оккама N*, в связи с чем начнём изложение с нескольких слов относительно этой логики. Логика N* была введена в качестве логической базы для фундированной семантики логических программ с отрицанием в [7], где она была сформулирована в качестве расширения логики К. Дошена N. Логика N, в свою очередь, представляет собой попытку сформулировать логику, отрицание -i в которой было бы слабее, чем отрицание минимальной логики Иохансонна J — для этого роль связки отрицания в логике играет модальный оператор невозможности весьма общего вида, тогда как позитивные связки конъюнкции А, дизъюнкции V и импликации —> интерпретируются как в позитивной логике Pos [11].

Аксиомы логики Гейтинга-Оккама позволили определить в ней интуиционистскую константу абсурда _L и, посредством сведения к абсурду, интуиционистское отрицание —, в связи с чем в диссертации мы будем рассматривать логику N* как интуиционистскую модальную логику с одной негативной модальностью. Точнее, мы зададим N* как логику, немодальный фрагмент которой совпадает с интуиционистской логикой Int, сформулированной в языке L1- = {A, V, —-L}, а единственное отрицание обозначается и представляет собой негативный модальный оператор.

Наиболее распространёнными объектами изучения модальных логик являются модальные операторы необходимости и возможности, на ряду с которыми можно рассматривать также дуальные негативные модальности невозможности и не-необходимости. Как известно, над классической логикой все четыре типа операторов могут быть определены друг через друга при помощи классического отрицания, что позволяет свести изучение нормальных операторов перечисленных типов к изучению всевозможных расширений наименьшей классической нормальной модальной логики К, названной в честь С. Крипке.

Для интуиционистских модальных логик не существует общепризнанного аналога логики К, задающего базу для изучения нормальных модальных операторов, отчасти потому, что над Int в силу характера интуиционистского отрицания не выполняются упомянутые связи между четырьмя типами операторов. Тем не менее, были предприняты различные попытки ввести общую теорию интуиционистских модальных логик. Так, например, В. Сотировым была определена интуиционистская модальная логика IMPL, единственный модальный оператор которой задавался исключительно правилом экстенсиональности [22]. Такой подход позволял задавать всевозможные интуиционистские модальные логики, в частности, логики с операторами необходимости и возможности, как расширения данной системы. Другой подход был предложен К. До-шеном и М. Божичем [5, 10], которые ввели четыре различные системы интуиционистских модальных логик, каждая из которых соответствовала своему типу модального оператора: НКО — необходимости, НКО — возможности, НКП' — не-необходимости и НКО' — невозможности. При этом предполагалось, что каждая из четырёх систем будет играть ту же роль для интуиционистских модальных логик соответствующих оператору заданного вида, как и логика К для классических модальных

логик. В диссертации мы будет следовать подходу Божича и Дошена для работы с интуиционистскими модальными логиками при этом четыре перечисленные логики мы будем называть логиками Гейтинга-Крипке. В качестве общего обзора по интуиционистским модальным логикам можно порекомендовать [30].

Помимо модального оператора невозможности, модальный оператор не-необходимости также может служить естественным обобщением понятия отрицания. Такой подход можно найти, например, в работе Р. Силь-вана [23], где в качестве расширения при помощи правила контрапозиции паранепротиворечивой логики Да Косты Сш была введена логика ССШ, из семантической интерпретации которой видно, что отрицание в ней является некоторым модальным оператором не-необходимости.

Оба подхода (т.е. отрицание как невозможность и отрицание как ненеобходимость) были изложены в работах Д. Вакарелова [26, 27] (см. также [28]), которым была предпринята попытка развить некоторую общую (хотя и не исчерпывающую) классификацию отрицаний. Базовыми типами отрицаний в классификации Вакарелова являлись так называемые регулярные и корегулярные отрицания, при этом отрицание первого типа можно трактовать как оператор невозможности, а второго — как оператор не-необходимости. Стоит отметить, что Вакарелов строил свою теорию отрицаний над дистрибутивными логиками (т.е. логиками, чья алгебраическая семантика задаётся дистрибутивными решётками) для того, чтобы избавиться от влияния характера импликации на отрицание. Однако эта теория легко может быть обобщена до интуиционистских или классических модальных логик.

Интересной особенностью отрицания логики ./V* является то, что новые (относительно логики А/") аксиомы логики позволяют интерпретировать отрицание в ней не только как модальный оператор невозможности,

но и как модальный оператор не-необходимости. Более того, отрицание в логике ./V* в точности является оператором, объединяющим свойства оператора невозможности логики НКО' и оператора не-необходимости логики НКО'. В классификации Вакарелова отрицание логики ./V* соответствует отрицанию, которое является одновременно нормальным и конормальным. В данной диссертации мы будем называть отрицание логики ./V* отрицанием Раутли в связи с тем, что для его интерпретации в семантике Крипке используется антимонотонная функция * — подход, широко распространённый в работах по релевантным логикам (см., например, [20]).

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

Одним из фундаментальных свойств логик является разрешимость. Логика называется разрешимой, если существует процедура, позволяющая по произвольной формуле определить, принадлежит ли она логике. Часто доказательство разрешимости логики сводится к доказательству того, что она обладает свойством конечных моделей, то есть что она полна относительно некоторого класса конечных шкал Крипке. В диссертации установлено, что логика Ы* обладает свойством конечных моделей и разрешима, причём представлено два независимых доказательства этих обстоятельств. В первом используется гибридное исчисление для логики, то есть такое исчисление, в синтаксисе которого явным образом присутствуют элементы семантики логики. Исчисление основано на гибридном исчислении для логик описаний [19] и в его формулировке использованы идеи Р. Дыкхова относительно того, как задать исчисление для интуиционистской логики, не требующее отдельного механизма для поиска циклов в выводе [13]. Анализ класса конечных шкал, относительно которого получена полнота этим методом, позволил провести более простое

доказательство, основанное на методе фильтрации для интуиционистской логики и классических модальных логик [8].

Доказав полноту логики относительно какого-то класса шкал, естественным представляется вопрос о том, можно ли получить сильную полноту логики относительно данного класса. В диссертации рассмотрена более широкая ситуация и показано, что не существует класса конечных шкал, относительно которого была бы сильно полна логика N*. Доказательство будет основано на теореме Джёбяка [14], который показал, что всякая промежуточная (т.е. нетривиальная суперинтуиционистская) логика или классическая нормальная модальная логика сильно полна относительно некоторого класса конечных шкал в том и только в том случае, когда она таблична. Напомним, что логика таблична, если она порождается одной конечной шкалой. Мы докажем аналогичное утверждение для расширений логики N*, назвав его теоремой Джёбяка для N*.

С.П. Одинцовым было доказано [17], что оператор — логики N*, полученный композицией интуиционистского отрицания и отрицания Ра-утли, является частным случаем оператора необходимости. Этот оператор, кроме того, был использован в [17] для формулировки критерия подпрямой неразложимости алгебр Гейтинга-Оккама, которые задают адекватную алгебраическую семантику логики N*. Композиция операторов является одним из простейших способов введения новых операторов. Естественным примером являются уже упомянутые дуальности над классической логикой: так, например, оператор необходимости □ в логике К может быть определён через оператор не-необходимости по правилу ПА := —D'A, где минусом обозначено классическое отрицание. В соответствии с вышесказанным возникает естественный вопрос о том, какие свойства модального оператора необходимости соответствуют упо-

минутой композиции интуиционистского отрицания и отрицания Раутли. Точнее, была поставлена задача аксиоматизации данного оператора в качестве оператора необходимости, решение которой приведено к диссертации. Поставленная задача оказалась в значительной степени трудоёмкой и её решение потребовало потребовала разрешения некоторых дополнительных вопросов. Как мы уже отмечали, отрицание Раутли может быть представлено и как частный случай модального оператора невозможности, и как частный случай оператора не-необходимости. В связи тем, что композиция классического отрицания и оператора не-необходимости является оператором необходимости над классической логикой, интерес вызывают свойства оператора необходимости, соответствующие композиции — интуиционистского отрицания и оператора не-необходимости. В диссертации аксиоматизация этого оператора сформулирована как нормальное расширение НК° логики НКО. Результат получен путём погружения логики НК° в логику НКсоответствующую оператору не-необходимости, при помощи естественной трансляции. Ключевым моментом в доказательстве является сведение семантики Крипке логики НК° к семантике логики НКО'. Далее, пользуясь аналогичной методикой, в качестве промежуточного шага была найдена аксиоматизация композиции —О' интуиционистского отрицания и оператора невозможности в наименьшей логике, в которой этот оператор является оператором необходимости. Наконец, последним шагом получена аксиоматизация композиции —-1 интуиционистского отрицания и отрицания Раутли в качестве нормального расширения НК^ логики НКО. Для доказательства этого результата потребовалось перейти к классам конечных шкал логик ./V* и НКчто стало возможным благодаря технике гибридных исчислений, развитой при доказательстве разрешимости логики ./V*.

Как известно, интуиционистское отрицание само по себе может быть

интерпретировано как модальный оператор невозможности [11]. Кроме того, было показано, что оператор двойного интуиционистского отрицания является частным случаем оператора необходимости. Этот результат был получен независимо Сотировым и Дошеном. Метод Сотирова [21] похож на тот, который был описан выше, а именно, в нём используется погружение одной системы в другую при помощи естественной трансляции. Метод, предложенный Дошеном [9], заключается в том, чтобы аксиоматизировать фрагмент без интуиционистского отрицания интуиционистской модальной логики, оператор необходимости в которой эквивалентен оператору двойного интуиционистского отрицания. Одним из приложений оператора двойного интуиционистского отрицания является теорема Гливенко (см., например, [8, теорема 2.47]), которая гласит, что формула А принадлежит классической логике тогда и только тогда,

когда формула--А принадлежит интуиционистской. Аналог теоремы

Гливенко для логики А"* был доказан в [18]. В связи с вышесказанным, интерес представляет вопрос об аксиоматизации оператора двойного отрицания Раутли. В диссертации сформулирована аксиоматизация данного оператора в качестве нормального расширения А^ логики НК□. Как мы выясним, существует множество аналогий между логиками А"* и А/"", однако в диссертации доказано одно важное различие. Точнее, показано, что логика А/"" обладает дизъюнктивным свойством, тогда как логика А* им не обладает.

Перейдём к описанию структуры диссертации.

Глава 1 целиком посвящена некоторым необходимым предварительным сведениям.

В разделе 1.1 сформулированы интуиционистская логика/п^, четыре интуиционистские модальные логики Гейтинга-Крипке НКП, НКО, НКП' и НКОа также логика Гейтинга-Оккама N*. Под логикой в

диссертации мы понимаем множество её теорем, отношение выводимости, названное в работе отношением синтаксического следования, при таком подходе является производным.

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

В разделе 1.3 изложены основные сведения, касающееся алгебраической семантики логики А"*. Как уже было упомянуто, соответствующие алгебры носят название алгебр Гейтинга-Оккама (отсюда же возникло и название логики) и представляют собой алгебры Гейтинга с дополнительным оператором отрицания, удовлетворяющим тождествам

-ч(сс V у) = -»ее Л ->г/, ->0 — 1,

Л у) = -<х V —»7/, ->1 = 0.

В разделе сформулирована теорема о полноте логики N* относительно ЯО-алгебр, а также дуальный изоморфизм между классом всех нормальных расширений логики и классом подмногообразий многообразия всех НО-алгебр. Далее изложен критерий подпрямой неразложимости НО-алгебр, в котором явным образом участвует оператор, полученный композицией интуиционистского отрицания и отрицания Раутли. В конце раздела задана связь между алгебраической семантикой и семантикой Крипке для логики.

Раздел 1.4 посвящён гибридному исчислению для Int, которое позднее будет расширено до исчисления для логики N*, а также ещё одной интуиционистской модальной логики. Исчисление представляет собой формализованную процедуру построения контр-модели для произвольной формулы. Утверждения о полноте и корректности данного исчисления могут быть использованы для получения нового доказательства свойства конечных моделей и разрешимости интуиционистской логики.

Предметом изучения главы 2 является класс конечных шкал для логики Гейтинга-Оккама.

В разделе 2.1 исчисление, заданное в разделе 1.4 для интуиционистской логики, расширено до исчисления для N*, доказаны утверждения о его полноте и корректности относительно заданной семантики, откуда выведено, что логика полна относительно некоторого класса конечных шкал специального вида и разрешима.

В разделе 2.2 класс шкал, относительно которого получена полнота логики N* в разделе 2.1, использован для того, чтобы доказать её разрешимость более прос