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

• Дробышевич, Сергей Андреевич
• кандидат наук
• 2013

Оглавление диссертации кандидат наук Дробышевич, Сергей Андреевич

Оглавление

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3.3.1 Логика HKf

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

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

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

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

3.4.1 Логика HKf

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

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

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

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

4.1 Логика N»

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

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

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

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

Литература

Введение диссертации (часть автореферата) на тему «Логика Гейтинга - Оккама и негативные модальности»

Введение

Результаты, изложенные в диссертации, так или иначе связаны с так называемой логикой Гейтинга-Оккама 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, использован для того, чтобы доказать её разрешимость более простым способом, основанным на методе фильтрации для интуиционистской логики и классических нормальных модальных логик. Основной особенностью данного метода фильтрации является то, что в нём использовано не одно, а сразу несколько отношений эквивалентности, по которым факторизуется данная модель.

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

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

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

В разделе 3.2 получена аксиоматизация композиции интуиционистского отрицания и не-необходимости в качестве оператора необходимости. Изложим кратко ход доказательства: сначала в разделе сформулировано нормальное расширение НК° логики НКП-, затем выделен класс шкал, относительно которого полна эта логика; после доказано, что всякая формула А принадлежит логике НК° тогда и только тогда, когда ти(А) принадлежит НКП1, где ти трансляция, которая проносится через все немодальные связки и такая, что ти(ПА) = — П'ти(А). В доказательстве явным образом используется семантика заданной логики.

В разделе 3.3 сначала показано, что композиция интуиционистского отрицания и невозможности в логике НКО' не является оператором необходимости, а затем сформулировано наименьшее расширение ДТ^0' логики НК О', в котором данная композиция оператором необходимости является. Аксиоматизация этого оператора получена как нормальное расширение НК° логики НКП, доказательство проводится аналогично описанному выше.

В разделе 3.4 дано решение для основной задачи главы. Для начала сформулировано нормальное расширение НК° логики НКП и выделен класс шкал, ей соответствующий. Далее для логики НК° адаптировано гибридное исчисление для логики А*, описанное в разделе 2.1, откуда выведена полнота логики относительно некоторого класса конечных

шкал специального вида и разрешимость. Далее этот класс конечных шкал использован для доказательства того, что логика НК° действительно задаёт аксиоматизацию композиции интуиционистского отрицания и отрицания Раутли. Заметим, что выполнены включения

НКП с с НК° с нкг°,

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

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

В разделе 4.1 введено нормальное расширение Л^ логики НКП и при помощи метода канонических моделей доказана её полнота относительно шкал, в которых для интерпретации оператора необходимости используется монотонная функция на множестве всех миров.

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

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

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

Результаты, полученные во второй главе диссертации, опубликованы в [36] и [37]; в третьей главе — в [39]; в четёртой главе — в [38].

Глава 1

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

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

Зафиксируем счётное множество пропозициональных переменных Prop := {ро?РъР25 • • • }> элементы которого мы обычно будем обозначать символами р, q или г (возможно с индексами).

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

• р £ For& для всякого р £ Prop;

• для любого г £ {1,..., т} выполнено

Аи ..., АПг е ForL => fi(Au ..., АПг) е ForL. В случае щ — 0 последнее условие вырождается в fi е For

Зафиксируем пропозициональный язык X1 := {Л, V, —_!_}, состоящий из бинарных связок конъюнкции, дизъюнкции и импликации и

константы абсурда, соответственно. Кроме того, зафиксируем унарные связки □, О, О', — необходимости, возможности, ненеобходимости, невозможности и отрицания Раутли, соответственно, и положим L6 := U {5} для ö £ {□, О, О', -.}.

Введём ряд соглашений о записи формул. Как обычно, будем писать (А о В) вместо о (А, В) для о £ {Л, V, —>} и 6А вместо J(А) для Ö £ {□, О, О',->}. Договоримся опускать внешние скобки в записи формул. Будет полагать, что импликация связывает формулы сильнее, чем конъюнкция и дизъюнкция: так, например, запись А А В —>■ С V D будет обозначать формулу ((А А В) —>• (С V D)). Также мы часто не будем уточнять, о формулах какого языка идёт речь, в случаях, когда это не будет создавать недоразумений.

Подформулой формулы А назовём любое подслово слова А, которое само является формулой. Множество всех подформул формулы А обозначим Sub(A).

Зададим аксиоматизацию интуиционистской логики Int. Список аксиом интуиционистской логики состоит из следующих формул:

II. р —(g —> р); 12. (р Ад) -»• р;

13. (р (д г)) -> ((р ->• д) (р —г)); /4. (р A q) g;

/5. (р ->• g) ->■ ((р г) ->• (р (д А г))); /6. р ->• (р V д);

17. (р -> г) ((g г) -> ((р V д) —> г)); /8. д -> (р V д); /9. _L р.

Единственным правилом вывода для Int является modus ponens:

А, А В

MP.

В

Мы будем отождествлять логики с множествами их теорем, таким образом, множество формул Ь одного из заданных языков назовём ло-

гикой, если оно замкнуто относительно МР и правила подстановки:

где запись А{р\,... ,рп) обозначает формулу А и то обстоятельство, что все пропозициональные переменные, входящие в А, содержатся в множестве {pi,... ,рп}, а A(Bi,..., Вп) — результат одновременной подстановки вместо всех вхождений переменной Pi в формулу А формулы Bi для каждого г 6 {1,..., п}. Ясно, что А(В\,..., Вп) является формулой.

В связи с этим соглашением, интуиционистской логикой Int будем называть наименьшую логику в языке ¿Л, содержащую формулы 11-19.

Как и в случае формул, мы часто не будет уточнять в каком языке сформулирована логика.

При помощи интуиционистской константы абсурда стандартным образом можно определить интуиционистское отрицание

Зададим теперь аксиоматизации логик Гейтинга-Крипке НКП, НКО, НКП', НКО', соответствующих модальным операторам необходимости, возможности, не-необходимости и невозможности [5, 10].

Пусть 5 G {□,<>, □', О'}. Список аксиом логики HKÖ в языке Ls получается добавлением формул ¿»1 и <52 к списку аксиом Int, где:

Правилами вывода для НКП и НКО являются МР и соответствующее монотонное правило:

SR.

А{Въ...,Вп)

□ 1. D(p->p);

□2. Пр Л Hq D(p Л q)-

O'l. О' -(p^p);

0'2. O'pAO'q 0'(pVq).

01. - 0-(p-+p);

02. O(pVq) ОpVOq;

п'2. п'(р Л q) П'р v n'q-

RH.

В

RO.

A^B

□Л □ В

OA^OB

правилами вывода для НКП' и НКО' — МР и соответствующее правило контрапозиции:

А В А В RH'. ——-—; RO ■

а в WA' ' О'В О'А

Зададим аксиоматизацию логики N* в языке Список аксиом N* получается добавлением к аксиомам Int следующих формул:

N1. ^pA^q -i(pVg); N2. - (р р);

N3. -п(р Л д) —)■ V -ig; A4.

Правила вывода для А"* — МР и правило контрапозиции для отрицания Раутли:

АТ„ А-> В NR.

Отметим следующее обстоятельство: если заменить в модальных аксиомах логики НКП' символ на -1, а в модальных аксиомах НКО' — О' на -I, и объединить эти списки, то мы получим в точности список аксиом логики А™. При такой замене правила контрапозиции ЯП1 и ЯО' переходят в правило контрапозиции для отрицания Раутли. В связи с этим можно считать, что отрицание Раутли является модальным оператором, который объединяет свойства оператора не-необходимости логики НКП' и оператора невозможности логики НКО'.

Логику Ь С Рог^ для (5 € {□, О, О', -п} назовём нормальной, если она замкнута относительно соответствующего модального правила (правила ЯП в случае 5 = □, правила А^Д в случае 6 = и так далее). Всякую логику Ь в языке &1- будем считать нормальной.

В диссертации мы будем иметь дело только с нормальными логиками, каждая из которых будет однозначно задана при помощи своего списка аксиом. В частности, логикой НК5 для 5 6 {□, О, О'} назовём наименьшую нормальную логику в языке £5, содержащую аксиомы

интуиционистской логики Int и формулы (51 и ¿2, а логикой N* — наименьшую нормальную логику в языке /Р, содержащую все аксиомы Int вместе с формулами N1-N4.

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

Введём сокращение

Л о В := (А ^ В) А (В А).

Стандартным образом при помощи аксиом интуиционистской логики и модального правила вывода (если оно есть) можно показать, что всякое нормальное расширение логики НК5 для ö 6 {□,<>, □',<>'} и логик N*, Int замкнуто относительно следующего правила замены эквивалентных:

Л~В (1.1)

С (А) <^С(В)'

Договоримся понимать под записью А\ о • • • о Ап для о е {л, V} формулу А\ при п = 1; при п > 1 положим

Аг о ■.. о Ап := ((Ах о • • • о Ап.х) о Ап).

С каждой логикой Ь свяжем отношение синтаксического следования Ьс,, а именно, для множества формул Г и формулы А положим Г Ь^ А, если и только если найдётся последовательность формул А\,..., Ап такая, что Ап = А и для всякого г £ {1,... ,п} либо Д 6 Ь и Г, либо найдутся < г такие, что А^ = А^ —>• А{ (в таком случае говорим, что А( получается из А^ и Ак по правилу МР).

В качестве сокращения будем писать Г Ь^ А для множеств формул Г и Д в том и только в том случае, когда существуют формулы Вг,..., Вт е Д такие, что Г \~ь В\ V • • • V Вт.

Везде далее мы будем писать Г1?..., Гп А вместо Г^и - • -иГп А и \~1, А вместо 0 А, а также опускать фигурные скобки при одноэлементных множествах.

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

Кроме того, для любой логики L, содержащей Int, верна [8] следующая теорема о дедукции для МР:

Список литературы диссертационного исследования кандидат наук Дробышевич, Сергей Андреевич, 2013 год

Литература

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

[2] Blackburn P., Benthem van J. Modal Logic: A Semantic Perspective // ETHICS. 1988. V. 98. P. 501-517.

[3] J. Berman. Distributive lattices with an additional unary operation // Aequationes Math. 1977. V. 16. P. 165-171.

[4] Bozic M., Dosen K. Axiomatizations of intuitionistic double negation // Bull. Sect. Logic Univ. Lodz. 1983. V. 12, № 2. P. 99-104.

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

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

[7] 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.

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

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

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

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

[12] 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.

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

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

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

[16] Kearnes K.A., Willard R. Residually finite, congruence meet semidistributive varieties of finite type have a finite residual bound // Proc. Amer. Math. Soc. 1999. V. 127. № 10. P. 2841-2850.

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

[18] Odintsov S.P. Glivenko theorem for N*-extension // Sib. Electron. Math. Izv. 2011. V. 8. P. 365-368.

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

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

[21] 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.

[22] 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.

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

[24] Urquhart A. Distributive lattices with a dual homomorphic operation // Studia Logica. 1979. V. 38. P. 201-209.

[25] Urquhart A. Distributive lattices with a dual homomorphic operation. II // Studia Logica. 1981. V. 40. P. 391-209.

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

[27] Vakarelov D. Consistency, Completeness and Negation // Paraconsistent

Logics: Essays on the Inconsistent / Eds. G. Priest, R. Routley, J. Norman. München: Philosophia Verlag, 1989. P. 328-363.

[28] 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.

[29] Wolter F. Superintuitionistic companions of classical modal logics // Studia Logica. 1997. V. 58. P. 229-259.

[30] 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.

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

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

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

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

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

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

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

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

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

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

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

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