Введение к работе
Тематика диссертации. Результаты, изложенные в диссертации, связаны с так называемой логикой Гейтинга — Оккама N*. Логика N* была введена в качестве дедуктивной базы для фундированной семантики логических программ с отрицаниями в [5], где она была определена как расширение логики К. Дошена N. Логика N [9, 10], в свою очередь, представляет собой попытку сформулировать логику, отрицание -> в которой было бы слабее, чем отрицание минимальной логики Иохансонна J — для этого роль связки отрицания в логике играет модальный оператор невозможности весьма общего вида, тогда как позитивные связки конъюнкции Л, дизъюнкции V и импликации —> интерпретируются как в позитивной логике Pos.
Аксиомы логики Гейтинга — Оккама позволили определить в ней интуиционистскую константу абсурда _1_, в связи с чем в диссертации логика N* задана как интуиционистская модальная логика, немодальный фрагмент которой совпадает с интуиционистской логикой Int, сформулированной в языке С := {Л, V, —>, _1_}, а единственное отрицание обозначается -> и представляет собой негативный модальный оператор. Как обычно, интуиционистской отрицание может быть определено через константу абсурда как —А := А —> _1_.
Наиболее распространёнными операторами модальных логик являются позитивные модальные операторы необходимости и возможности, на ряду с которыми можно рассматривать также дуальные негативные модальные операторы невозможности и не-необходимости. Как известно, над классической логикой все четыре типа операторов могут быть определены друг через друга при помощи классического отрицания, что позволяет свести изучение нормальных операторов перечисленных типов к изучению всевозможных расширений наименьшей классической нормальной модальной логики К, названной в честь С. Крипке.
Для интуиционистских модальных логик не существует общепризнанного аналога логики К, задающего базу для изучения нормальных модальных операторов, тем не менее, были предприняты различные попытки ввести общую теорию интуиционистских модальных логик. Так, например, В. Сотировым была определена интуиционистская модальная логика IMPL [19], единственный модальный оператор которой задавался исключительно правилом экстенсиональности. Другой подход был предложен К. Дошеном и М. Божичем [3, 8], которые ввели че-
тыре различные системы интуиционистских модальных логик, каждая из которых соответствовала своему типу модального оператора: НКП\ — необходимости, НК() — возможности, НКП\' — не-необходимости и НК()' — невозможности. При этом предполагалось, что каждая из четырёх систем будет играть ту же роль для интуиционистских модальных логик соответствующих оператору заданного вида, как и логика К для классических модальных логик. В диссертации используется подход Божича и Дошена для работы с интуиционистскими модальными логиками, при этом четыре перечисленные логики мы будем называть логиками Гейтинга — Крипке. В качестве общего обзора по интуиционистским модальным логикам можно порекомендовать [24].
Помимо модального оператора невозможности, модальный оператор не-необходимости также может служить естественным обобщением понятия отрицания. Такой подход можно найти, например, в работе Р. Сильвана [20], где была введена логика ССШ, из семантической интерпретации которой видно, что отрицание в ней является некоторым модальным оператором не-необходимости.
Оба подхода (т.е. отрицание как невозможность и отрицание как не-необходимость) присутствуют в работах Д. Вакарелова [21, 22] (см. также [23]), которым была предпринята попытка ввести общую (хотя и не исчерпывающую) классификацию отрицаний. Базовыми типами отрицаний в классификации Вакарелова являлись так называемые регулярные и корегулярные отрицания, при этом отрицание первого типа можно трактовать как оператор невозможности, а второго — как оператор не-необходимости. Стоит отметить, что Вакарелов строил свою теорию отрицаний над дистрибутивными логиками (т.е. логиками, чья алгебраическая семантика задаётся дистрибутивными решётками) для того, чтобы избавиться от влияния характера импликации на отрицание. Однако эта теория легко может быть обобщена до интуиционистских или классических модальных логик.
Интересной особенностью отрицания логики N* является то, что новые (относительно логики N) аксиомы логики позволяют интерпретировать отрицание в ней не только как модальный оператор невозможности, но и как модальный оператор не-необходимости. Более того, отрицание в логике N* в точности является оператором, объединяющим свойства оператора невозможности логики НК()' и оператора ненеобходимости логики НКП\'. В классификации Вакарелова отрицание логики N* соответствует отрицанию, которое является одновременно
нормальным и конормальным. В данной диссертации мы будем называть отрицание логики N* отрицанием Раутли в связи с тем, что для его интерпретации в семантике Крипке используется антимонотонная функция * — подход, широко распространённый в работах по релевантным логикам (см., например, [17]).
Одним из фундаментальных свойств логик является разрешимость. Логика называется разрешимой, если существует процедура, позволяющая по произвольной формуле определить, принадлежит ли она логике. Часто доказательство разрешимости логики сводится к доказательству того, что она обладает свойством конечных моделей, то есть что она полна относительно некоторого класса конечных шкал Крипке. В диссертации установлено, что логика N* обладает свойством конечных моделей и разрешима, причём представлено два независимых доказательства этих утверждений. В первом строится гибридное исчисление для логики, то есть исчисление, в синтаксисе которого явным образом присутствуют элементы семантики логики. Анализ класса конечных шкал, относительно которого получена полнота этим методом, позволяет провести более простое доказательство, основанное на методе фильтрации для интуиционистской логики и классических модальных логик [6].
Доказав полноту логики относительно какого-то класса шкал, естественным представляется вопрос о том, можно ли получить сильную полноту логики относительно данного класса. В диссертации рассмотрена более широкая ситуация и показано, что не существует класса конечных шкал, относительно которого сильно полна логика N*. Приведённое доказательство основано на теореме Джёбяка [12], который показал, что всякая нетривиальная суперинтуиционистская логика или классическая нормальная модальная логика сильно полна относительно некоторого класса конечных шкал тогда и только тогда, когда она таблична. Напомним, что логика таблична, если она задаётся одной конечной шкалой. В диссертации доказано аналогичное утверждение для расширений логики N*, названое теоремой Джёбяка для N*.
СП. Одинцовым было доказано [14], что оператор — -> логики N*, полученный композицией интуиционистского отрицания и отрицания Раутли, является частным случаем оператора необходимости. Этот оператор, кроме того, был использован в [14] для формулировки критерия подпрямой неразложимости алгебр Гейтинга — Оккама, которые задают адекватную алгебраическую семантику логики N*. Композиция операторов является одним из простейших способов введения новых опера-
торов. Естественным примером являются уже упомянутые дуальности над классической логикой. В соответствии с вышесказанным возникает естественный вопрос о том, какие свойства модального оператора необходимости соответствуют упомянутой композиции интуиционистского отрицания и отрицания Раутли. Точнее, была поставлена задача аксиоматизации оператора —->, полученного композицией интуиционистского отрицания и отрицания Раутли, в качестве оператора необходимости, решение которой приведено к диссертации.
Как известно, интуиционистское отрицание само по себе может быть интерпретировано как модальный оператор невозможности [9]. Кроме того, было показано, что оператор двойного интуиционистского отрицания является частным случаем оператора необходимости. Этот результат был получен независимо Сотировым [18] и Дошеном [7, 2]. Одним из приложений оператора двойного интуиционистского отрицания является теорема Гливенко (см., например, [6, теорема 2.47]), которая гласит, что формула А принадлежит классической логике тогда и только тогда, когда формула — — А принадлежит интуиционистской. Аналог теоремы Гливенко для расширений логики N* был доказан в [15]. В связи с вышесказанным, интерес представляет вопрос об аксиоматизации оператора двойного отрицания Раутли. В диссертации сформулирована аксиоматизация данного оператора в качестве нормального расширения логики НКП\.
Теоретическая и практическая ценность. Диссертация носит теоретический характер. Её результаты могут быть использованы при дальнейших исследованиях в области интуиционистских модальных логик, а также в рамках спецкурсов для студентов и аспирантов.
Научная новизна. Все основные результаты диссертации являются новыми.
Методы исследования. В диссертации используются методы работы с семантикой Крипке [6], методы универсальной алгебры [4] для работы с алгебраической семантикой логики N*, а также некоторые результаты из области классической логики первого порядка [1]. Кроме того, построенные в диссертации гибридные исчисления основаны на технике табличных исчислений, развитой в [16].
Основные результаты диссертации.
-
Доказано, что логика N* обладает свойством конечных моделей и разрешима. Построено гибридное исчисление для логики N*, доказаны утверждения о его корректности и полноте относительно семантики логики (опубликовано в [30]).
-
Доказан аналог теоремы Джёбяка для расширений логики N*. А именно, показано, что всякое нормальное расширение L логики N* является сильно полным относительно некоторого класса конечных шкал тогда и только тогда, когда L — табличная логика (опубликовано в [31]).
-
Получена аксиоматизация композиции интуиционистского отрицания и отрицания Раутли — -і в логике N* в качестве оператора необходимости (опубликовано в [33]).
-
Получена аксиоматизация оператора двойного отрицания Раутли -1-і в качестве оператора необходимости (опубликовано в [32]).
Второй из основных результатов получен совместно с С. П. Одинцовым при равном участии обеих сторон, остальные результаты получены автором самостоятельно.
Апробация работы. Результаты диссертации докладывались на международных конференциях: «Мальцевские чтения» (Новосибирск, 2009, 2010, 2012), «Logic Colloquium 2011» (Барселона, Испания), «Advances in Modal Logic 2012» (Копенгаген, Дания). Также результаты диссертации докладывались на совместных семинарах ИМ СО РАН и ИГУ «Нестандартные логики» и «Алгебра и логика».
Публикации. Основные результаты опубликованы в работах [25-33], из них [30-33] входят в перечень ВАК российских рецензируемых научных журиалов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук. Работа [31] написана совместно с С. П. Одинцовым при равном участии обеих сторон.
Структура и объем диссертации. Диссертация состоит из введения, четырёх глав, разбитых на разделы, и списка литературы. Список лите-
