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

Одинцов Сергей Павлович

Конструктивные отрицания и

паранепротиворечивость

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

алгебра и теория чисел

Автореферат

диссертации на соискание ученой степени

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

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

Работа выполнена в Институте математики им. С.Л. Соболева СО РАН.

Официальные оппоненты:

доктор физико-математических наук, профессор, член-корреспондент РАН Беклемишев Лев Дмитриевич доктор физико-математических наук, профессор Максимова Лариса Львовна доктор физико-математических наук, профессор Чагров Александр Васильевич

Ведущая организация:

Красноярский государственный университет.

Защита диссертации состоится 22 марта 2007 г. в 11 час. 30 мин. на заседании Диссертационного Совета Д 003.015.02 при Институте математики им. С.Л. Соболева СО РАН по адресу: 630090, Новосибирск-90, пр. Акад. Коптюга, 4.

С диссертацией можно ознакомиться в библиотеке Института математики им. С.Л. Соболева СО РАН.

Автореферат разослан “ ” февраля 2007 г.

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

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

Актуальность темы. Как следует непосредственно из названия, проблематика данной работы сочетает концепции паранепротиворечивости и конструктивной логики. Поэтому в самом начале мы скажем несколько слов о двух упомянутых концепциях. Паранепротиворечивые логики это такие логики, которые допускают противоречивые, но нетривиальные теории, т.е. логики, позволяющие осуществлять нетривиальные выводы из противоречивого множества гипотез. Логики, в которых все противоречивые теории тривиальны, будут называться избыточными.

Отмеченное свойство паранепротиворечивых логик позволяет использовать их в разнообразных ситуациях, когда приходится иметь дело с феноменами, имеющими отношение, в той или иной степени, к логическому понятию противоречивости. К числу таких ситуаций мы можем отнести следующие: накопление информации в компьютерных базах данных; различные научные теории; законы и иные юридические документы; описание фантастических (и иных несуществующих) объектов; описание контрафактических ситуаций и т.д. Изучение феномена паранепротиворечивости может быть основано на различных философских предпосылках (см., например, [23]). Мы отметим лишь один фундаментальный аспект исследований в области паранепротиворечивости, прекрасно выраженный Д. Нельсоном [21, с.209]: “Как в классической, так и в интуиционистской логике все противоречия эквивалентны. Это делает в принципе невозможным рассмотрение подобных сущностей в математике. Мне не ясно, действительно ли необходима столь радикальная позиция в отношении противоречия.” Отвергая принцип “противоречие влечет все что угодно” (ex contraditione quodlibet), паранепротиворечивая логика позволяет изучать феномен противоречия сам по себе. Именно этот формально логический аспект паранепротиворечивости будет в центре внимания представленного исследования.

Конструктивная логика это логика конструктивной математики, логика, ориентированная на работу с универсумом конструктивных математических объектов. Общим для различных вариантов конструктивной математики является отказ от использования концепции актуальной бесконечности и признание существования только таких объектов, которые построены на основе концепции потенциальной осуществимости. Переход от классической логики к конструктивной сопровождается изменением смысла логических связок. Например, А.А. Марков [5] следующим образом определяет конструктивную дизъюнкцию: “Конструктивному пониманию существования математического объекта соответствует конструктивное понимание дизъюнкций предложений вида “P или Q”. Такое предложение тогда считается установленным, когда хотя бы одно из предложений P, Q установлено как верное.” Разумеется, данное понимание дизъюнкции не позволяет признать закон исключенного третьего и приводит к отказу от классической логики. В рамках конструктивной логики сформировались две важнейшие концепции отрицания, которые и рассматриваются в данной диссертации. При этом стоит оговорится, что наши исследования носят классический, а не конструктивный характер.

Каким же образом понимается отрицание в контексте конструктивной логики? Во-первых, начиная с работ Л.Э.Я. Брауера отрицание утверждения P, ¬P, понимается как сокращение утверждения “предположение P ведет к противоречию”. Заметим, что такое понимание отрицания хорошо согласуется с концепцией паранепротиворечивости, так как оно вовсе не предполагает принципа ex contradictione quodlibet, влекущего за собой тривиализацию противоречивых теорий. Первый вариант формализации интуиционистской логики, предложенный А.Н. Колмогоровым [1] еще в 1925 году, был паранепротиворечивым. Тем не менее, А. Гейтинг был уверен, что использование ex contradictione quodlibet допустимо в интуиционистских рассуждениях, и добавил аксиому ¬p (p q) к своему варианту Li интуиционистской логики [15]. Только в 1937 году И. Иоганссон [17] вновь поставил под вопрос использование ex contradictione quodlibet в конструктивных рассуждениях и предложил систему, которая стала впоследствии называться логикой Иоганссона или минимальной логикой. Обозначим эту логику Lj. Аксиоматика Lj получается вычеркиванием ex contradictione quodlibet из стандартного списка аксиом интуиционистской логики, иными словами, имеет место соотношение Li = Lj + {¬p (p q)}. Фактически, Иоганссон вернулся к Колмогоровскому варианту интуиционистской логики. Точнее, {, ¬}-фрагмент логики Lj совпадает с пропозициональным фрагментом системы Колмогорова [1].

К сожалению, логика Lj в течение долгого времени находилась вне внимания специалистов по паранепротиворечивости. Традиционно это мотивировалось следующим “паранепротиворечивым парадоксом” логики Lj. Хотя формально логика Lj не является избыточной, т.е. допускает нетривиальные противоречивые теории, мы можем доказать в Lj для любых формул и, что Это означает, что связка отрицания теряет смысл в противоречивых Ljтеориях, поскольку в таких теориях доказуемо отрицание любой формулы. Таким образом, противоречивые Lj-теории это, по существу, позитивные теории. Следует отметить, что исследования в области паранепротиворечивости в течение долгого времени были направлены на поиск “наиболее естественной системы” паранепротиворечивой логики (см. [16, с.147]), в наибольшем объеме сохраняющей свойства классической логики. Что привело, впрочем, к созданию достаточно экзотических логик. В известной логике Н. Да Косты, например, нельзя определить логическую связку, обладающую свойствами конгруэнции, что делает весьма проблематичным развитие математики над такой логикой. Поэтому в последнее время все большее внимание уделяется изучению паранепротиворечивых аналогов известных логических систем. И в этом отношении логика Иоганссона Lj безусловно заслуживает внимания как паранепротиворечивый аналог интуиционистской логики Li.

Второй важнейший подход к понятию отрицания в конструктивной логике это концепция сильного отрицания. Отметим, что именно сильное отрицание является действительно конструктивным. Конструктивная логика с сильным отрицанием была предложена Д. Нельсоном в 1949 году [20]. Истинность негативного утверждения может быть установлена в интуиционистской и минимальной логике только опосредованно, через сведение к абсурду. Вследствие этого интуиционистское и минимальное отрицания обладают следующим свойством, не удовлетворительным с конструктивной точки зрения. Если доказуемо отрицание конъюнкции ¬( ), то из этого факта не следует, что одна из формул ¬ или ¬ доказуема. В упомянутой работе Д. Нельсон предлагает новую конструктивную концепцию отрицания. Основная идея состоит в том, что ложность (фальсифицируемость) атомных утверждений может быть установлена непосредственно, так же, как их истинность (верифицируемость). Это приводит к двум параллельным конструктивным процедурам, сводящим истинность и ложность сложных утверждений к истинности или ложности их компонент. В результате Д. Нельсон получает логическую систему, обладающую таким свойством:

где обозначает связку отрицания, а выводимость в системе Нельсона. В настоящее время данное свойство рассматривается как характеристическое свойство конструктивного отрицания, а отрицания Нельсоновского типа называются сильными. В [20] была предложена избыточная логика, которую мы будем обозначать N3, паранепротиворечивый вариант логики Нельсона N4 предложен в [7].

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

Кроме того, она может быть использована для разрешения некоторых известных логических парадоксов (см. [34, 36]). В то же время, ее изучению было уделено несравненно меньше внимания, чем избыточной N3.

В частности, семантические исследования N4 ограничивались семантикой Крипке. Отсутствовала какая-либо специфическая информация о классе N4-расширений, за исключением сведений о классе расширений логики N3. Стоит отметить, что последний класс изучался достаточно интенсивно (см.[14, 18, 28, 29, 30]).

Итак, имеются две избыточные логики Li и N3, и их паранепротиворечивые аналоги Lj и N4. В диссертации установлено, что Li точно вкладывается в Lj, а N3 точно вкладывается в N4. Таким образом, отказ от аксиомы избыточности не приводит к потере выразительных возможностей логики. Здесь встает вопрос о том, какими новыми выразительными возможностями обладают логики Lj и N4 по сравнению с избыточными Li и соответственно N3, а также насколько регулярно устроен этот набор новых возможностей? В настоящей работе мы постараемся дать ответ на этот вопрос исследуя решетки расширений логик Lj и N4.

Изучение классов расширений различных логик таких, например, как интуиционистская логика Li (см., например, [8]), нормальная модальная логика K4 [12, 13] и т.д., играет чрезвычайно важную роль в развитии современной логики. В первой части диссертации представлен первый опыт систематического изучения решетки расширений паранепротиворечивой логики, а именно логики Lj. Установлена важная черта, отличающая класс Lj-расширений от классов расширений избыточных логик Li и K4. Класс Jhn всех нетривиальных расширений минимальной логики имеет нетривиальную и интересную глобальную структуру (он трехмерный, в некотором смысле), что позволяет свести его описание, до определенной степени, к хорошо изученным классам промежуточных и позитивных логик. Точнее, класс Jhn является дизъюнктным объединением трех классов: класса промежуточных логик Int, который содержит только избыточные логики; класса Neg, состоящего из негативных логик, т.е. логик с вырожденным отрицанием, содержащих схему ¬p; и класса Par собственно паранепротиворечивых расширений логики Lj, содержащего все логики, не попавшие в первые два класса.

Заметим, что негативные логики дефинициально эквивалентны позитивным.

Для любой логики L Par, можно определить ее интуиционистский напарник Lint (негативный напарник Lneg ) как наименьшую логику из класса Int (соответственно, из класса Neg), содержащую логику L.

Имеются сильные трансляции (т.е. трансляции, сохраняющие отношение следования) логик Lint и Lneg в исходную паранепротиворечивую логику L. Логика Lint может быть получена также присоединением ex contradictione quodlibet к L. Таким образом, упомянутая трансляция логики Lint показывает, что обычные избыточные рассуждения моделируются в паранепротиворечивой логике. В то же время, как было отмечено выше, важным преимуществом паранепротиворечивых логик является возможность различать противоречия, которые не эквивалентны друг другу. В случае класса Lj-расширений структура противоречий паранепротиворечивой логики L эксплицируется в виде формальной системы, а именно, в виде ее негативного напарника Lneg. Сильная трансляция логики Lneg в L может быть задана посредством оператора противоречия C() := ¬. Поэтому логика Lneg действительно может рассматриваться как логика противоречий логики L. Ответ на вопрос о том, в какой степени Lint и Lneg определяют исходную логику L, дается с помощью специального представления j-алгебр, задающих алгебраическую семантику логики Lj.

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

Во второй части диссертации исследуется решетка расширений паранепротиворечивой логики Нельсона. Здесь существенную роль играет не только интерес к логике Нельсона как альтернативной формализации интуиционистской логики, но и желание проверить, применим ли к этому новому объекту подход, разработанный в первой части работы? И ответ на этот вопрос является положительным, хотя будет обнаружено также существенное отличие структур решеток расширений минимальной логики и паранепротиворечивой логики Нельсона.

В связи с паранепротиворечивой логикой Нельсона возникает вопрос, в каком языке следует рассматривать эту логику. Избыточная логика N3 рассматривается обычно в языке,,,, ¬ с символами для двух отрицаний, сильного и интуиционистского ¬. Причем интуиционистское отрицание, вообще говоря, излишне, так как может быть определено через сильное. При переходе к паранепротиворечивой логике N4 интерпретация ¬ не ясна, поэтому кажется естественным рассматривать язык с единственным отрицанием. Такой вариант паранепротиворечивой логики Нельсона мы будем обозначать N4. Тем не менее, как мы увидим, присутствие в языке интуиционистского отрицания наряду с сильным естественно и желательно. Консервативное расширение логики N4 в языке,,,, с дополнительными аксиомами для константы будет обозначаться N4. Интуиционистское отрицание определяется в N4 обычным образом, ¬ :=.

Для изучения класса EN4 (EN4 ) расширений логики Нельсона N4 (N4 ) необходима адекватная алгебраическая семантика. Нужно найти определяющее логику N4 (N4 ) многообразие алгебр такое, что существует дуальный изоморфизм между решеткой подмногообразий данного многообразия и решеткой N4(N4 )-расширений. Для избыточной логики N3 такую семантику задает многообразие N -решеток, которое достаточно хорошо изучено [24, 10, 11, 14, 28, 29, 33]. N4решетки, введенные автором в [58], определяют семантику этого типа для логики N4. Алгебраическая семантика для N4 задается N4 решетками, естественной модификацией N4-решеток. Интересная особенность N4(и N4 )-решеток состоит в том, что они имеют целый фильтр выделенных значений.

Преимущество языка с интуиционистским отрицанием становится явным, когда мы начинаем исследование класса N4 -расширений. Его строение существенно отличается от строения класса Jhn. Прежде всего, в отличие от Jhn, содержащего целый подкласс Neg противоречивых логик, логика N4 не имеет нетривиальных противоречивых расширений.

Несмотря на то, что логика N4 паранепротиворечива, она допускает только локальные противоречия. Присоединение к N4 противоречия как схемы формул имеет своим результатом тривиальную логику. Тем не менее, класс EN4 разбивается на подклассы избыточных, нормальных логик и логик общего вида. Это разбиение отражает локальную структуру противоречий в N4 -моделях и подобно разбиению класса Jhn на подклассы промежуточных, негативных и собственно паранепротиворечивых логик. Именно присутствие в языке константы позволяет определить класс нормальных логик, соответствующий классу негативных логик в решетке Lj-расширений.

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

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

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

Практическая ценность. Работа носит теоретический характер. Ее результаты могут найти и находят (см. [6]) применение в дальнейших исследованиях паранепротиворечивых логик, прежде всего решеток расширений минимальной логики и паранепротиворечивой логики Нельсона. Еще одной областью приложений являются логические основания искусственного интеллекта и одно из таких приложений дано в [22].

Основные результаты. В работе получены следующие основные результаты:

1. Установлено разбиение класса Jhn на классы промежуточных логик Int, негативных логик Neg и собственно паранепротиворечивых логик Par. Исследованы связи между классами Int, Neg и Par.

Для этой цели каждой логике L Par сопоставлены ее интуиционистский Lint и негативный Lneg напарники.

2. Получено представление произвольной j-алгебры в виде A f B, где A Гейтингова, B негативная алгебры, f нижний полурешеточный гомоморфизм из B в A. C помощью этого представления описана алгебраическая семантика логик Сегерберга и исследованы соотношения между ними.

3. Описано строение класса Jhn с точностью до негативной эквивалентности.

4. Установлено, что интервалы вида Spec(L1, L2 ) бесконечны. Найдено достаточное условие континуальности интервала этого вида.

5. На основе анализа парадокса минимальной логики предложено определение отрицания через унарный оператор абсурдности. Исследована возможность представления в таком виде отрицания в логике Батенса CLuN и логике Сета P 1.

6. Описана семантика логик N4 и N4 в терминах N4-решеток, соответственно, N4-решеток. Доказано, что N4-(N4 -)решетки представимы в виде твист-структур над импликативными решетками (алгебрами Гейтинга).

7. Установлено, что N4-(N4 -)решетки образуют многообразие и найден конечный базис тождеств этого многообразия. Установлен дуальный решеточный изоморфизм между решеткой расширений логики N4 (N4 ) и решеткой подмногообразий многообразия N4N4 -)решеток.

8. Развиты начала алгебраической теории N4 -решеток. В частности получено представление N4 -решеток в виде алгебр Гейтинга с выделенными фильтром и идеалом. В терминах этого представления получен критерий вложимости N4 -решеток и описаны факторы N4 -решеток. Охарактеризованы подпрямо неразложимые N4 -решетки.

9. В решетке EN4 расширений логики N4 определены подклассы избыточных логик Exp, нормальных логик Nor и логик общего вида Gen, играющие роль аналогичную классам Int, Neg и Par в решетке расширений минимальной логики. Исследованы связи между классами Exp, Nor и Gen.

10. Полностью описана решетка расширений логики N4 C, получающейся присоединением аксиомы Даммета к N4. Доказано, что все ее расширения разрешимы и конечно аксиоматизирумы, а по произвольной формуле можно определить, какое расширение логики N4 C она аксиоматизирует.

11. Описаны табличные, предтабличные логики и логики, обладающие интерполяционным свойством Крейга в решетке расширений Апробация. Результаты работы неоднократно докладывались на семинарах “Алгебра и логика” и “Нестандартные логики” Новосибирского госуниверситета, семинаре лаборатории логических систем ИМ СО РАН, Международных конференциях "Мальцевские чтения"(пленарный доклад в 2004 году). Результаты работы были представлены на 1-м Конгрессе по паранепротиворечивости, г. Гент, 1997; Международном симпозиуме памяти С.Яськовского, г.Торунь, 1998; Международной конференции “Смирновские чтения”, г.Москва, 1999; 1-м и 2-м Польско-фламандских симпозиумах по логике и формальной онтологии, г.Торунь, 1999 и г.Гент, 2000; XLVI-й Конференции по истории логики, г.Краков, 2000; Летней европейской школе по логике, языку и информации, г.Тренто, 2002; Международном симпозиуме “Отрицание в конструктивных логиках”, г.Дрезден, 2004 (пленарный доклад); 1-м Конгрессе по универсальной логике, г.Монтре, 2005.

Публикации. Основные результаты диссертации опубликованы в работах автора [39], [41], [45–48], [52], [55–63].

Структура и объем работы. Диссертация состоит из десяти глав, из которых первая глава является вводной, а оставшиеся разделены на две части (первая часть – главы 2–7, вторая часть – главы 8–10), и списка литературы. Работа изложена на 289 страницах, включает 17 рисунков, список литературы содержит 121 наименование, в том числе работ автора диссертации. В диссертации принята тройная нумерация утверждений, например, номер 4.2.6 означает, что данное утверждение находится во втором параграфе 4-й главы и имеет в этом параграфе номер 6.

СОДЕРЖАНИЕ ДИССЕРТАЦИИ

Глава 1 является вводной, в ней приводится краткая история вопроса, мотивация проводимых исследований и краткий обзор содержания диссертации.

Первая часть диссертации включает в себя главы 2–7 и посвящена концепции отрицания как сведения к абсурду.

Глава 2 содержит определение позитивной логики, минимальной логики и важнейших ее расширений, информацию об алгебраической семантике и семантике Крипке позитивной и минимальной логик и их расширений, а также некоторые факты из универсальной алгебры. Напомним, что минимальная логика Lj может быть получена расширением схем аксиом позитивной логики Lp на язык,,,, при этом отрицание ¬ считается сокращением формулы. Эквивалентным образом, в языке,,, ¬ логика Lj получается присоединением аксиомы (p q) ((p ¬q) ¬p) к аксиомам позитивной логики. Алгебраическая семантика логики Lp задается импликативными решетками, а логики Lj j-алгебрами, представляющими собой импликативные решетки, в которых интерпретируется как произвольный элемент носителя. Алгебра Гейтинга это j-алгебра с наименьшим элементом, а негативная алгебра это j-алгебра с наибольшим элементом. Алгебры Гейтинга задают семантику интуиционистской логики Li = Lj + { p}, а негативные алгебры семантику минимальной негативной логики Ln = Lj + {}.

В главе 3 изучается логика классической опровержимости Le = Lj + {p (p q)}, задается ее алгебраическая семантика и находится простейшая характеристическая модель, содержащая четыре элемента.

Задается разбиение класса Jhn всех нетривиальных Lj-расширений на подклассы: класс Int, включающий в себя все промежуточные логики;

класс Neg негативных логик, т.е. логик с аксиомой или, что эквивалентно, ¬p; класс собственно паранепротиворечивых логик Par = Jhn \ (IntNeg). Хорошо известно, что Int = [Li, Lk], где Lk = Li+{p(p q)} классическая логика. Доказано, что два других класса также являются интервалами: Neg = [Ln, Lmn], где Lmn = Ln + {p (p q)} максимальная негативная логика, и Par = [Lj, Le]. Таким образом, Le наибольшее собственно паранепротиворечивое расширение минимальной логики.

Кроме того, в этой главе изучены изоморфы [25] классической и максимальной негативной логик в Le, т.е. способы определения матриц для Lk и Lmn в четырех-элементной модели Le с помощью термальных операций. Полученные изоморфы приводят к следующим трансляциям Lk и Lmn в Le:

Глава 4 посвящена исследованию общей структуры класса Par и его связей с классами Int и Neg. Оказывается, в этом исследовании существенную роль играют определенные выше трансляции. Сначала исследуются семантика и класс расширений логики Le = Lj+{( p)}.

Для j-алгебры A определим алгебру Гейтинга A как подалгебру с носителем {a A | a} и негативную алгебру A как подрешетку с носителем {a A | a } и импликацией x y = (x y).

Установлено, что A |= Le, если и только если A A A. Причем требуемый изоморфизм задается отображением (x) = (x, x ).

С помощью этой характеризации доказывается, что логика L является собственно паранепротиворечивым расширением Le, если и только если L = L1 L2, где L1 Int и L2 Neg. Причем логики L1 и L2 определяются однозначно по L и называются интуиционистским и негативным напарниками логики L. В дальнейшем напарники обозначаются Lint и Lneg соответственно. Напарники транслируются в исходную логику следующим образом:

С учетом того, что Le ¬¬ ( ), определенные в главе 3 трансляции логик Lk и Lmn в Le являются частными случаями трансляций напарников.

Для произвольной логики L Par ее негативный напарник определяются как и выше, а интуиционистский следующим образом:

причем для Le -расширений это определение эквивалентно предыдущему.

Для произвольной логики L Par оператор противоречия C() := ¬ (при расширении C на множества формул считаем C() = {}) задает сильную трансляцию, т.е. трансляцию, сохраняющую отношение следования, из Lneg в L. Тем самым, негативный напарник эксплицирует структуру противоречий логики L.

Отображение L (Lint, Lneg ) является эпиморфизмом решетки Par на прямое произведение Int Neg. Прообраз пары логик L1 Int и L2 Neg относительно этого отображения обозначим Spec(L1, L2 ), т.е.

Оказывается, это множество всегда является интервалом:

где L1 L2 := Lj+{In(), | L1, L2 }. Для логик вида L1 L дана семантическая характеризация и способ построения аксиоматики по аксиомам L1 над Li и аксиомам L2 над Lj.

Мы получили, что класс собственно паранепротиворечивых Lj-расширений распадается на объединение попарно непересекающихся интервалов В этой главе также установлен ряд соотношений между интервалами вида Spec(L1, L2 ), в частности, что любой такой интервал изоморфен верхнему подинтервалу интервала Spec(Li, Ln). А также, что любая логика из Spec(L1, L2 ) аксиоматизируется относительно L1 L2, наименьшей логики интервала, следствиями формулы ( p).

В главе 5 найдено представление j-алгебр, удобное для работы с логиками, расположенными внутри интервалов вида Spec(L1, L2 ). Пусть B алгебра Гейтинга, C негативная алгебра, a f полурешеточный гомоморфизм из C в B, сохраняющий пересечение и наибольший элемент. Определим решетку B f C как подрешетку прямого произведения B C с универсумом Операция задает на B f C структуру j-алгебры.

Установлено, что любая j-алгебра представима в виде B f C. Точнее, для любой j-алгебры отображение (x) = (x, x ) задает изоморфизм С помощью этого представления описана семантика логик Сегерберга [27] и изучены соотношения между ними.

В последнем параграфе этой главы рассмотрена семантика Крипке для расширений минимальной логики и для j-шкал Крипке определены аналоги алгебр A и A.

Глава 6 посвящена изучению отношения негативной эквивалентности на расширениях минимальной логики. Говорим, что L1 негативно меньше чем L2, пишем L1 neg L2, если для любых множества формул X и формулы выполняется следующая импликация:

Логика L1 негативно эквивалентна L2, L1 neg L2, если L1 neg L и L2 neg L1. Главным результатом главы является описание структуры классов негативной эквивалентности. Пусть Jhn+ := Jhn {F}, где F тривиальная логика, т.е. множество всех формул. Определим neg :=neg / neg. Справедливы следующие утверждения:

1. Jhn+ / neg, neg Spec(Lk, Ln) {F},.

2. Для любых L1 Int и L2 Neg имеем Для доказательства этих утверждений используется техника формул Янкова, применяемая обычно для построения семейств логик мощности континуум. Ее удобство в данном случае обусловлено тем, что для не-негативных подпрямо неразложимых моделей логик из Spec(Lk, L2 ) формулы Янкова являются отрицаниями.

В этой главе получены также результаты о мощности интервалов Spec(L1, L2 ). Структура интервала Spec(Lk, Lmn) описана полностью, это линейный порядок типа ( + 1). Поскольку Spec(Lk, Lmn) простейший из интервалов вида Spec(L1, L2 ), то и любой интервал вида Spec(L1, L2 ) будет бесконечным.

Если негативный напарник L2 имеет счетное число конечных моделей, попарно не вложимых друг в друга, то Spec(L1, L2 ) имеет мощность континуума. В доказательстве этого результата формулы Янкова используются стандартным образом.

Глава 7 завершает исследование концепции отрицания как сведения к абсурду. Как было упомянуто ранее, минимальная логика долгое время была вне поля зрения специалистов по паранепротиворечивости из-за парадокса минимальной логики, состоящего в том, что из противоречия выводимо любое отрицание. Это приводит к вырождению отрицания в противоречивых Lj-теориях. Ввиду этого обстоятельства представляется естественным завершить исследование отрицания как сведения к абсурду анализом парадокса минимальной логики. Установлено, что оператор противоречия C() := ¬ в логике классической опровержимости в точности соответствует оператору необходимости в модальной логике Лукасевича L. Фактически это означает, что определяя логику L Лукасевич взял за основу столь малый набор свойств модальностей, что он не позволяет отличить необходимость от оператора противоречия. Показано, что эта аналогия между противоречием и необходимостью может быть продолжена. С одной стороны, определен класс C-логик с примитивной связкой C и отрицанием, определяемым как ¬ := C(). С другой стороны выделен модальный парадокс логики L такой, что оператор противоречия в C-логике L свободен от этого парадокса, если и только если сама логика L свободна от парадокса минимальной логики. Таким образом, более естественные свойства оператора C с точки зрения модальной логики приводят к более естественному отношению выводимости с точки зрения паранепротиворечивой логики.

Эти рассуждения приводят к идее рассмотрения отрицания как сведения к унарному оператору абсурдности. Во второй части главы уточняется, каким образом отрицание может быть представлено через унарный оператор абсурдности, а также проводится различие между операторами абсурдности и противоречия. Для двух известных систем паранепротиворечивой логики, логики Батенса CLuN и максимальной паранепротиворечивой логики Сета P 1, подробно исследован вопрос о представимости отрицания в этих логиках через операторы абсурдности и противоречия.

Глава 8 начинает вторую часть диссертации, посвященную сильному отрицанию. В первом параграфе определяются два варианта паранепротиворечивой логики Нельсона. Логика N4 определяется в языке,,,, где символ для сильного отрицания, аксиомами позитивной логики и следующими аксиомами сильного отрицания:

Логика N4 это логика в языке,,,, с дополнительной константой и дополнительными аксиомами Логика N4 является консервативным расширением как N4, так и интуиционистской логики.

Избыточная логика N3 получается присоединением к N4 аксиомы избыточности p (p q). Причем, полагая := (p0 p0 ) можно доказать в N3 дополнительные аксиомы логики N4.

Сложность работы с логиками N4 и N4 обусловлена тем, что доказуемая эквивалентность не обладает свойствами конгруэнции. Из эквивалентности формул не следует эквивалентность их сильных отрицаний. Конгруэнцией будет лишь доказуемая сильная эквивалентность Во втором параграфе логика N4 характеризуется с помощью структур Фиделя [11]. Это непосредственное обобщение результата М. Фиделя из [11] для логики N3. Структуры Фиделя представляют собой импликативные решетки с выделенным семейством одноместных предикатов.

В третьем параграфе семантика N4 задается с помощью твист-структур (см. [10, 33]). Причем теорема полноты следует из доказанной здесь же эквивалентности структур Фиделя и твист-структур. Основное определение параграфа следующее.

Определение 1. Пусть A = A,,,, 1 импликативная решетка.

1. Полная твист-структура над A это алгебра с твист-операциями, определяемыми для (a, b), (c, d) AA следующим образом:

2. Твист-структура над A это произвольная подалгебра B полной твист-структуры A такая, что 1 (B) = A, где 1 проекция на 1-ю координату.

3. Семейство всех твист-структур над A обозначается S (A).

Оценка в твист-структуре определяется как обычно. Семантическое отношение следования |= над твист-структурами определяется следующим образом. Пусть множество формул, формула, а B твист-структура. Отношение |=B выполняется, если и только если для любой оценки v структуры B условие 1 v() = 1 для всех влечет 1 v() = 1. Отношение |= означает, что |=B для всех твист-структур B.

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

Определение 2. Алгебра A = A,,,, называется N4-решеткой, если выполнено следующее.

1. Редукт A,,, является алгеброй Де Моргана, т.е. A,, дистрибутивная решетка (неограниченная в общем случае) и выполняются следующие тождества: (p q) = p q и p = p.

является предпорядком на A.

3. Отношение, где a b если и только если a b и b a, является конгруэнцией относительно операций,,, а фактор-алгебра A := A,,, / является импликативной решеткой.

b a, где решеточный порядок на A.

Главное отличие N4-решеток от N -решеток [24] в определении отношения, что является основным источником трудностей и находит отражение в определении истинности на N4-решетках.

Доказано, что всякая твист-структура является N4-решеткой, а всякая N4-решетка A изоморфна твист-структуре над A. Истинность формулы в N4-решетке определяется как истинность тождества =, или, что эквивалентно, как истинность в матрице A, DA, где DA = {a A | a a = a}. Это определение согласуется с определением истинности на твист-структурах, откуда следует, что N4 характеризуется N4-решетками.

В следующем параграфе доказывается, что N4-решетки образуют многообразие VN4, и устанавливается дуальный решеточный изоморфизм между решеткой EN4 расширений логики N4 и решеткой подмногообразий многообразия VN4.

В заключительном параграфе главы 8 ранее полученные результаты переносятся на логику N4 и решетку ее расширений EN4. При этом твист-структуры определяются над алгебрами Гейтинга и для любой N4 -решетки A фактор-структура A также будет алгеброй Гейтинга.

Назовем A базисной алгеброй N4 -решетки A.

В главе 9 развиты начала алгебраической теории N4 -решеток.

Если A алгебра Гейтинга, фильтр на A, содержащий фильтр плотных элементов, а идеал на A, то существует твист-структура T w(A,, ) S (A) с носителем Более того, любая твист-структура над A представима в таком виде.

Это представление N4 -решеток обобщает результат А.Сендлевского для N -решеток [29] и играет ключевую роль в дальнейших исследованиях.

Далее, в этой главе определяется пара сопряженных функторов между категориями N4 -решеток и алгебр Гейтинга. Доказывается, что если гомоморфизм базисных алгебр может быть поднят на N4 -решетки, то это делается единственным образом. Показано, что конгруэнции на N4 -решетке находятся во взаимно однозначном соответствии с импликативными фильтрами. Установлен изоморфизм решеток конгруэнций N4 -решетки и ее базисной алгебры. Как следствие, описаны подрямо неразложимые N4 -решетки как решетки с подпрямо неразложимой базисной алгеброй. В терминах описанного выше представления сформулирован критерий вложимости и описаны фактор-алгебры N4 решеток.

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

В первом параграфе изучаются связи между решеткой EN4 и решеткой суперинтуиционистских логик Int+. Главными объектами изучения являются оператор, сопоставляющий каждой логике L EN4 ее интуиционистский фрагмент (L), а также операторы отображающие суперинтуиционистскую логику L в концевые точки прообраза 1 (L), который является интервалом. Для любой L Int+ верно Во втором параграфе изучается общая структура решетки EN4.

Сначала полностью описывается интервал 1 (Lk), который содержит пять элементов и среди них RM3, обогащение известной логики RM константой ; эквивалентное представление L3 трех-значной логики Лукасевича; B, обогащение четырех-значной логики Белнапа B4 импликацией. Как следствие доказывается, что N4 не содержит противоречивых нетривиальных расширений. Это существенное отличие структуры решетки EN4 от структуры класса Jhn. Минимальная логика имеет целый класс противоречивых расширений, изоморфный классу расширений позитивной логики.

Обозначим N4N := N4 + {¬¬(p p)} и выделим в EN4 следующие подклассы:

Пусть L EN4. Говорим, что логика L является избыточной, если L Exp. Назовем L нормальной, если L Nor. Наконец, если L Gen, говорим, что L логика общего вида.

Класс Nor играет роль аналогичную классу Neg в решетке расширений минимальной логики. При этом нетривиальность пересечения Exp Nor является неизбежным следствием отсутствия противоречивых расширений у N4. Отметим, что интервал Exp Nor изоморфен решетке Int+.

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

В четвертом параграфе полностью описаны решетки расширений логик N4 C := N4 + {C} и N4C := N4 + {C}, которые получаются присоединением к N4 и соответственно N4 линейной аксиомы Даммета C := (p q) (q p). Интерес к этому результату имеет следующее объяснение.

Во-первых, сравнение структур решеток EN4 C и EN4C наглядно показывает, как разрушается регулярная структура решетки расширений логики N4, описанная в этой главе, при удалении интуиционистского отрицания. В частности, в классе EN4 нельзя определить нормальные логики.

Во-вторых, заслуживает внимание сравнение структур решеток расширений EN4 C, EN3C и ELC, где N3C := N3 + {C}, а LC логика Даммета, получающаяся присоединением к интуиционистской логике аксиомы линейности. Логика Даммета является первым примером предтабличной логики, структура расширений которой была полностью описана [9]. М. Крахт [18] описал структуру расширений логики N3C и показал, что хотя эта логика не является предтабличной, она сохраняет важнейшие свойства предтабличных логик. А именно, все расширения логики N3C конечно аксиоматизируемы и разрешимы. Более того, по данной формуле можно эффективно определить, какое именно расширение логики N3C она аксиоматизирует. Оказывается, класс расширений логики N4 C также удовлетворяет всем этим свойствам. Кроме того, сравнение решеток EN4 C и EN3C наглядно демонстрирует степень сложности решетки расширений паранепротиворечивой логики Нельсона.

В последнем 5-м параграфе этой главы доказаны две теоремы переноса для решетки EN4. Попутно описаны табличные логики в EN4.

Для переноса вполне сознательно выбраны результаты, аналоги который для класса расширений избыточной логики Нельсона N3 уже известны, а именно, полученные Л.Л.Максимовой [3, 4] описания суперинтуиционистских предтабличных логик и суперинтуционистских логик, обладающих интерполяционным свойством Крейга. Сравнение этих результатов для решеток EN3 и EN4 демонстрирует особенности строения класса EN4. Получены следующие результаты. Во-первых, описаны предтабличные логики в EN4, что обобщает результат А. Сендлевского [28] для расширений логики N3. Класс EN4 содержит те же самые предтабличные логики, что и класс EN3, а именно логики вида (L), где L предтабличная суперинтуиционистская логика. Отсутствие новых предтабличных логик в EN4 объясняется отсутствием у N4 противоречивых расширений.

Второй результат состоит в описании логик, обладающих интерполяционным свойством Крейга (CIP ). Ранее В. Горанко [7] доказал, что логика L из EN3 обладает CIP если и только если ее интуиционистский фрагмент (L) обладает CIP и L является наибольшей или наименьшей логикой в EN3 c интуиционистским фрагментом (L). Таким образом, в EN3 ровно 14 нетривиальным логик обладает CIP. При переходе от EN3 к EN4 число нетривиальных логик с CIP снова удваивается. Причем и в этом случае CIP переносится на логики, занимающие (в известном смысле) предельное положение в EN4. Новые логики с CIP в EN4 это в точности логики, у которых интуиционистский фрагмент обладает CIP, и которые являются наименьшими логиками с данным интуиционистским фрагментом в классах Nor или Gen.

Список литературы [1] Колмогоров А. Н. О принципе tercium non datur // Матем. сборник. – 1925. – Т. 32, №4. – С. 646–667.

[2] Кушнер Б.А. Конструктивная математика // Математическая энциклопедия, т.2 / Ред. A. Виноградов. – Москва: Советская энциклопедия, 1977. – С. 1042–1046.

[3] Максимова Л.Л. Предтабличные суперинтуиционистские логики // Алгебра логика. – 1972. – Т. 11, № 5. – С. 552–570.

[4] Максимова Л.Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых алгебр // Алгебра логика. – 1977. – Т. 16, №6. – С. 643–681.

[5] Марков А.А. О конструктивной математике // Тр. ИМ им. Стеклова. – 1962. – Т. 67. – С. 8–14.

[6] Стукачева М.В. Дизъюнктивное свойство и канонические формулы в классе расширений минимальной логики. Диссер. на соискание уч. степени канд. физ.-мат. наук. – Новосибирск, 2006 – [7] Almukdad A., Nelson D. Constructible falsity and inexact predicates // J. Symb. Log. – 1984. – Vol. 49, No. 1. – P. 231–233.

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

[9] Dunn J.M., Meyer R.K. Algebraic completeness results for Dummett’s LC and its extensions // Z. Math. Logic Grundl. Math. – 1971. – Vol. 17, No. 2. – P. 225–230.

[10] Fidel M.M. An algebraic study of a propositional system of Nelson // Mathematical Logic, Proc. of the First Brasilian Conference, Campinas 1977. – Lect. Notes Pure Appl. Math. 39, 1978. – P. 99-117.

[11] Fidel M.M. An algebraic study of logic with constructive negation // Proc. of the Third Brazilian Conf. on Math. Logic, Recife 1979. – 1980. – P. 119–129.

[12] Fine K. Logics containing K4. I // J. Symb. Log. – 1974. – Vol. 39, [13] Fine K. Logics containing K4. II // J. Symb. Logic. – 1985. – Vol. 50, No. 3. – P. 619–651.

[14] Goranko V. The Craig interpolation theorem for propositional logics with strong negation // Stud. Log. – 1985. – Vol. 44, No. 3. – P. 291– [15] Heyting A. Die formalen Regeln der intuitionistischen Logik // Sitzungsber. Akad. Berlin. – 1930. – P. 42–56.

[16] Jakowski S. Propositional calculus for contradictory deductive systems // Stud. Log. – 1969. – Vol. 24. – P. 143–157.

[17] Johansson I. Der Minimalkalkl, ein reduzierter intuitionistischer Formalismus // Compos. Math. – 1937. – Vol. 4. – P. 119–136.

[18] Kracht M. On extensions of intermediate logics by strong negation // J. Philos. Log. – 1998. – Vol. 27, No 1. – P. 49–73.

[19] Lukasiewicz J. A system of modal logic // J. Comput. Systems. – Vol. 1. – P. 111–149.

[20] Nelson D. Constructible falsity // J. Symb. Log. – 1949. – Vol. 14, [21] Nelson D. Negation and separation of concepts // Constructivity in mathematics. – Amsterdam: Notrh-Holland, 1959. – P. 208–225.

[22] Odintsov S.P., Pearce D. Routley semantics for answer sets // Logic Programming and Nonmonotonic Reasoning, 8th International Conference, LPNMR 2005, Diamante, Italy, September 5-8, 2005, Proceedings / Eds. Baral G.Ch, Greco G., Leone N. – LNCS 3662.

– Springer, 2005. – P. 343-355.

[23] Paraconsistent logic. Essays on the inconsistent / Eds. Priest G., Routley R., Norman J. – Mnchen: Philosophia Verlag, 1989. – 716 p.

[24] Rasiowa H. N -lattices and constructive logic with strong negation // Fundam. Math. – 1958. – Vol. 46, No. 1. – P. 61–80.

[25] Rescher N. Many-valued Logic. – N.Y.,1969. – 359 p.

[26] Routley R. Semantical analyses of propositional systems of Fitch and Nelson // Stud. Log. – 1974. – Vol. 33, No.3. – P. 283–298.

[27] Segerberg K. Propositional logics related to Heyting’s and Johansson’s // Theoria. – 1968. – Vol. 34, No.1. – P. 26–61.

[28] Sendlewski A. Some investigations of varieties of N -lattices // Stud.

Log. – 1984. – Vol. 43, No. 3. – P. 257–280.

[29] Sendlewski A. Nelson algebras through Heyting ones // Stud. Log. – 1990. – Vol. 49, No. 1. – P.106-126.

[30] Sendlewski A. Axiomatic extensions of the constructive logic with strong negation and disjunction property // Stud. Log. – 1995. – Vol. 55, No. 3. – P. 377–388.

[31] Sette A.M. On the propositional calculus P 1 // Math. Jap. – 1973. – Vol. 18, No. 3. – P. 173-180.

[32] Thomason R. A semantical study of constructive falsity // Z. Math.

Logik Grundl. Math. – 1969. – Vol. 15, No. 3. – P. 247–257.

[33] Vakarelov D. Notes on N-lattices and constructive logic with strong negation // Stud. Log. – 1977. – Vol. 36, No. 1–2. – P. 109–125.

[34] Wansing H. Semantics-based nonmonotonic inference // Notre Dame J. Formal Logic. – 1995. – Vol. 36, No. 1. – P. 44–54.

[35] Wansing H. Negation // The Blackwell Guide to Philosophical Logic / Ed. Goble L. – Cambridge: Basil Blackwell Publishers, 2001. – P. 415– [36] Wansing H. Diamonds are a Philosopher’s Best Friends // J. Philos.

Log. – 2002. – Vol. 31, No. 6. – P. 591–612.

Работы автора по теме диссертации [37] Одинцов С.П. О связи относительно конструктивных систем с традиционными подходами // Выч. системы. – 1989. – Вып. 129. – Новосибирск, 1989. – С. 172-182.

[38] Одинцов С.П. Пропозициональные относительно конструктивные системы // Выч. системы. – 1997. – Вып. 158. – Новосибирск, 1997.

[39] Одинцов С.П. Изоморфы логики классической опровержимости и их обобщения // Труды научно-исследовательского семинара Логического центра Института философии РАН / Ред. Смирнова Е.Д. – Москва, 1998. – С. 48–61.

[40] Одинцов С.П. Паранепротиворечивые расширения минимальной логики и их логики противоречий // Смирновские чтения, 2я международная конференция/ Ред. Смирнова Е.Д. – Москва, 1999. – С. 58–60.

[41] Одинцов С.П. О негативно эквивалентных расширениях минимальной логики и их логиках противоречий // Логические исследования / Ред. Карпенко А.С. – Москва: Наука, 2000. – С. 119–127.

[42] Одинцов С.П. О логиках Сегерберга // Выч. системы. – 2001. – Вып. 168. – Новосибирск, 2001. – С. 19–52.

[43] Одинцов С.П. O парадоксе минимальной логики // Выч. системы.

– 2001. – Вып. 168. – Новосибирск, 2001. – С. 53–60.

[44] Одинцов С.П. Алгебраическая семантика и семантика Крипке для расширений минимальной логики // Логические исследования [Электронный ресурс]. – 1999, Т. 2. – Режим доступа: http:// www.logic.ru.

[45] Одинцов С.П. Теоремы переноса для расширений паранепротиворечивой логики Нельсона // Алгебра и логика – 2006. – Т. 45, №4 – С. 409–435..

[46] Одинцов С.П. О расширениях логики Нельсона, удовлетворяющих аксиоме Даммета // Сиб. матем. журнал – 2007. – Т. 48, №1. – С. 144-161.

[47] Одинцов С.П. Об одном обобщении принципа reductio ad absurdum // Вестник НГУ, Серия: матем., мех. и информатика. – 2006. – Т. 6, [48] Одинцов С.П. Решетка расширений минимальной логики // Математические труды – 2006. Т. 9, №2. – С. 60–108.

[49] Odintsov S.P. Maximal paraconsistent extension of Johansson logic // First World Congress on Paraconsistency, Abstracts. – Ghent,1997. – P. 111–113.

[50] Odintsov S.P. Maximal paraconsistent extension of Johansson logic // Log. Anal., Nouv. Ser. – 1998. – Vol. 161/163. – P. 107–120.

[51] Odintsov S.P. On j-algebras and j-frames // International Maltsev conference on mathematical logic, Abstracts. – Novosibirsk, 1999. – P. 101–102.

[52] Odintsov S.P. Representation of j-algebras and Segerberg’s logics // Log. Anal., Nouv. Ser. – 1999. – Vol. 165/166. – P. 81–106.

[53] Odintsov S.P. Negation as Absurdity in Paraconsistent Setting // II World Congress on Paraconsistentcy, Juquehy, Brazil, 2000:Abstracts.

– Campinas, 2000. – P. 94–95.

[54] Odintsov S.P. On the Structure of Paraconsistent Extensions of Johansson’s Logic (extended abstract) // CLE-e-prints [Electronic resource]. – 2002. – Vol. 2, No. 7. – Mode of access:

ftp:logica.cle.unicamp.br/pub/e-prints/Odintsov.ps.

[55] Odintsov S.P. On the embedding of Nelson’s logics // Bull. Sect. Log., Univ. Lodz, Dep. Log. – 2002. – Vol. 31, No. 4. – P. 241–250.

[56] Odintsov S.P. Logic of classical refutability and class of extensions of minimal logic // Log. Log. Philos. – 2002. – Vol. 9. – P. 91–107.

[57] Odintsov S.P. Semantical characterization of Nelson’s paraconsistent logic // Smirnov Readings, 4th International Conference / Ed.

Karpenko A.S. – Moscow, 2003. – P. 86–87.

[58] Odintsov S.P. Algebraic semantics for paraconsistent Nelson’s Logic // J. Log. Comput. – 2003. – Vol. 13, No. 4. – P. 453–468.

[59] Odintsov S.P. “Reductio ad absurdum” and Lukasiewicz’s modalities // Log. Log. Philos. – 2003. – Vol. 11. – P. 149–166.

[60] Odintsov S.P. On representation of N4-lattices // Stud. Log. – 2004.

– Vol. 76, No. 3. – P. 385–405.

[61] Odintsov S.P. Negative equivalence of extensions of minimal logic // Stud. Log. – 2004. – Vol. 76, No. 3. – P. 417–442.

[62] Odintsov S.P. On the structure of paraconsistent extensions of Johansson’s logic // J. Appl. Log. – 2005. – Vol. 3, No. 1. – P. 43–65.

[63] Odintsov S.P. The Class of Extensions of Nelson Paraconsistent Logic // Stud. Log. – 2005. – Vol. 80, No. 2-3. – P. 291–320.