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

Оглавление
1 Введение 4
1 Reductio ad absurdum 20
2 Минимальная логика. Синтаксис и семантика. 21
3 Логика классической опровержимости 37
3.1 Свойство максимальности логики Le .................... 39
3.2 Изоморфы логики Le.................................... 43
4 Класс расширений минимальной логики 50
4.1 Расширения логики Le'................................. 50
4.1.1 Интуиционистские и негативные напарники расширений логики Le'..................................... 56
4.2 Интуиционистские и негативные напарники расширений минимальной логики......................................... 59
4.2.1 Негативные напарники как логики противоречий 65
4.3 Три размерности класса Par............................ 66
5 Адекватная алгебраическая семантика для расширений
минимальной логики 70
5.1 Логика Гливенко....................................... 70
5.2 Представление j-алгебр................................ 73
1
*
5.3 Логики Сегерберга и их семантика.......................... 77
5.4 Семантика Крипке для паранепротиворечивых расширений логики Щ.................................................. 98
6 Негативно эквивалентные логики 102
6.1 Определения и простейшие свойства.......................102
6.2 Логики, негативно эквивалентные промежуточным .... 106
6.3 Классы негативной эквивалентности.......................109
6.4 Структура Лп+ с точностью до негативной эквивалентности 114
7 Абсурдность как унарный оператор 126
7.1 Введение................................................126
7.2 Ье и модальная логика Лукасевича........................130
7.3 Парадокс минимальной логики и обобщенная абсурдность 136
7.4 А- и С-представления....................................143
7.4.1 Определения и первые результаты...................143
7.4.2 Логика СЬиК ......................................151
7.4.3 Логика Сета Р1....................................156
II Сильное отрицание 162
8 Различные виды семантики для паранепротиворечивой логики Нельсона 163
8.1 Логики N4 и К4Х и их простейшие свойства................165
8.2 Семантика Фиделя........................................169
8.3 Твисг-структуры.........................................174
8.3.1 Вложение логики N3 в N4...........................178
8.4 Ш-Решетки...............................................182
8.5 Многообразие N4^11161^..................................185
2
8.6 Логика N41 и N41-решетки...............................194
9 N41-PemeTKH 198
9.1 Структура N41-pemeTOK .................................201
9.2 Гомоморфизмы и подпрямо неразложимые N4x-peiueTKH . 209
10 Класс расширений логики N41 222
10.1 Ш41 и lnt+............................................222
10.2 Структура решетки £N4X................................233
10.3 Избыточные и нормальные напарники.....................244
10.4 Структура решеток СN4C и £N4XC........................251
10.5 Теоремы переноса для класса N4x-pacnmpeHHft ..........265
Глава 1
Введение
Как следует непосредственно из названия, проблематика данной работы сочетает концепции паранепротиворечивости и конструктивной логики. Поэтому в самом начале мы скажем несколько слов о двух упомянутых концепциях. Паранепротиворечивые логики — это такие логики, которые допускают противоречивые, но нетривиальные теории, т.е. логики, позволяющие осуществлять нетривиальные выводы из противоречивого множества гипотез. Логики, в которых все противоречивые теории тривиальны, будут называться избыточными (столь вольным способом мы переведем уже устоявшийся английский термин explosive, ввиду того, что дословный перевод, “взрывающийся”, обладает степенью экспрессии чрезмерной для научного текста). Отмеченное свойство паранепротиво-речивых логик позволяет использовать их в разнообразных ситуациях, когда приходится иметь дело с феноменами, имеющими отношение, в той или иной степени, к логическому понятию противоречивости. К числу таких ситуаций мы можем отнести следующие: накопление информации в компьютерных базах данных; различные научные теории; законы и иные юридические документы; описание фантастических (и иных несуществующих) объектов; описание контрафактических ситуаций и т.д. Для первого знакомства с проблематикой паранепротиворечивости можно порекомендовать обзор Г. Приста [65], появившийся во втором издании
Handbook of Philosophical logic. Изучение феномена паранепротиворечивости может быть основано на различных философских предпосылках (см., например, [66]). Мы отметим лишь один фундаментальный аспект исследований в области паранепротиворечивости, прекрасно выраженный Д. Нельсоном. В работе [60, с.209] Д. Нельсон отмечает: “Как в классической, так и в интуиционистской логике все противоречия эквивалентны. Это делает в принципе невозможным рассмотрение подобных сущностей в математике. Мне не ясно, действительно ли необходима столь радикальная позиция в отношении противоречия.” Отвергая принцип “противоречие влечет все что угодно” (ex contraditione quodlibet), па-ранепротиворечивая логика позволяет изучать феномен противоречия сам по себе. Именно этот формально логический аспект паранепротиворечивости будет в центре внимания представленного исследования.
Обратимся теперь к конструктивной логике. Довольно часто конструктивная логика отождествляется с формализацией интуиционистской логики, предложенной А. Гейтингом [40]. Однако смысл этого понятия значительно шире. Конструктивная логика — это логика конструктивной математики, логика, ориентированная на работу с универсумом конструктивных математических объектов. Общим для различных вариантов конструктивной математики является отказ от использования концепции актуальной бесконечности и признание существования только таких объектов, которые построены на основе концепции потенциальной осуществимости. Различные способы понимания последней концепции дают начало различным направлениям конструктивной математики (см., например, [2]) и, соответственно, различным вариантам конструктивной логики. В любом случае, переход от классической логики к конструктивной сопровождается изменением смысла логических связок. Например, А.А. Марков [5] следующим образом определяет конструктивную
дизъюнкцию: ‘‘Конструктивному пониманию существования математического объекта соответствует конструктивное понимание дизъюнкций — предложений вида "Р или Q\ Такое предложение тогда считается установленным, когда хотя бы одно из предложений Р, Q установлено как верное.” Разумеется, данное понимание дизъюнкции не позволяет признать закон исключенного третьего и приводит к отказу от классической логики. В рамках конструктивной логики сформировались две важнейшие концепции отрицания, которые и рассматриваются в данной диссертации. При этом стоит оговорится, что наши исследования носят классический, а не конструктивный характер.
Каким же образом понимается отрицание в контексте конструктивной логики? Есть два основных подхода. Во-первых, начиная с работ Л.Э.Я. Брауера отрицание утверждения Р, -1 Р. понимается как сокраг щение утверждения “предположение Р ведет к противоречию”. Заметим, что такое понимание отрицания хорошо согласуется с концепцией паранепротиворечивости, так как оно вовсе не предполагает принципа ех contradictione quodlibet, влекущего за собой тривиализацию противоречивых теорий. Первый вариант формализации интуиционистской логики, предложенный А.Н. Колмогоровым [1] еще в 1925 году, был паранепро-тиворечивым. В этой работе Колмогоров резонно замечает, что принцип ex contradictione quodlibet (в форме -»р —»► (р —>► q)) появился только в формальном представлении классической логики и не используется в обычной математической практике. Тем не менее, А. Гейтинг был уверен, что использование ex contradictione quodlibet допустимо в интуиционистских рассуждениях, и добавил аксиому -»р —► (р —» q) к своему варианту Li интуиционистской логики [40]. Только в 1937 году И. Иоганссон [43] вновь поставил под вопрос использование ex contradictione quodlibet в конструктивных рассуждениях и предложил систему, которая стала впо-
следствии называться логикой Иоганссона или минимальной логикой Обозначим эту логику Ьр. Аксиоматика 1^ получается вычеркиванием ех сопЬгаИсИопе quodlibet из стандартного списка аксиом интуиционистской логики, иными словами, имеет место соотношение 1л = Щ 4- {-^р (р —► <?)}. В [43] Иоганссон доказал, что многие свойства отрицания, доказуемые в логике Гейтинга 1л, сохраняются и в его системе Ьд. Фактически, Иоганссон вернулся к Колмогоровскому варианту интуиционистской логики. Точнее, {—*, -*}-фрагмент логики Ь} совпадает с пропозициональным фрагментом системы Колмогорова [1]. А.Н. Колмогоров рассматривал логику первого порядка, но в языке, который содержит только две пропозициональных связки, импликацию и отрицание.
К сожалению, логика Ц в течение долгого времени находилась вне внимания специалистов по паранепротиворечивости. Традиционно это мотивировалось следующим “паранепротиворечивым парадоксом” логики Iф Хотя формально логика Ь) не является избыточной, т.е. допускает нетривиальные противоречивые теории, мы можем доказать вЦ для любых формул у? И что
“V ы
Это означает, что связка отрицания теряет смысл в противоречивых 1у теориях, поскольку в таких теориях доказуемо отрицание любой формулы. Таким образом, противоречивые Ц-теории — это, по существу, позитивные теории. Следует отметить, что исследования в области паранепротиворечивости в течение долгого времени были направлены на поиск “наиболее естественной системы” паранепротиворечивой логики (см. [42, с. 147]), в наибольшем объеме сохраняющей свойства классической логики. Что привело, впрочем, к созданию достаточно экзотических логик. В известной логике Н. Да Косты, например, нельзя определить логическую связку, обладающую свойствами конгруэнции, что делает весьма
проблематичным развитие математики над такой логикой. Поэтому в последнее время все большее внимание уделяется изучению паранепроти-воречивых аналогов известных логических систем. И в этом отношении логика Иогансеона Ц безусловно заслуживает внимания как паранепро-тиворечивый аналог интуиционистской логики Ы.
Перейдем ко второму главному подходу к понятию отрицания в конструктивной логике, концепции сильного отрицания. Отметим, что именно сильное отрицание является действительно конструктивным.
Как это часто случается с наиболее фундаментальными понятиями, концепция сильного отрицания была развита независимо несколькими авторами, использовавшими различные мотивации. Конструктивная логика с сильным отрицанием была предложена впервые Д. Нельсоном в 1949 году [59]. Истинность негативного утверждения может быть установлена в интуиционистской и минимальной логике только опосредованно, через сведение к абсурду. Вследствие этого интуиционистское и минимальное отрицания обладают следующим свойством, не удовлетворительным с конструктивной точки зрения. Если доказуемо отрицание конъюнкции -I(<р Л то из этого факта не следует, что одна из фор-
мул -• или ->гр доказуема. В упомянутой работе Д. Нельсон предлагает новую конструктивную концепцию отрицания. Основная идея состоит в том, что ложность (фальсифицируемость) атомных утверждений может быть установлена непосредственно, так же, как их истинность (ве-рифицируемость). Это приводит к двум параллельным конструктивным процедурам, сводящим истинность и ложность сложных утверждений к истинности или ложности их компонент. В результате Д. Нельсон получает логическую систему, обладающую таким свойством:
если Л ^), то Ь~ или -0, где ~ обозначает связку отрицания, а Ь — выводимость в системе Нель-
сона. В настоящее время данное свойство рассматривается как характеристическое свойство конструктивного отрицания, а отрицания Нельсоновского типа называются сильными. Генценовское исчисление, эквивалентное системе Нельсона, было разработано независимо Ф. фон Кучера [50]. Системы, близкие к логике с сильным отрицанием, появляются также в работе Ж.П. Клива [24], который строил логику первого порядка, соответствующую алгебре неточных множеств С. Кернера [47]. Пара-непротиворечивый вариант системы Нельсона был предложен лишь в 1984 году в работе [9], где было коротко упомянуто, что вычеркивание схемы аксиом р р —> ф) из системы Нельсона приводит к кон-
структивной логике, которая может успешно применяться для работы с противоречивой информацией. Стоит отметить также, что сам термин “сильное отрицание” связан не с идеей непосредственной фальсификации утверждений, а с соотношением между сильным и интуиционистским отрицанием в избыточном варианте системы Нельсона [59]. В этой логике интуиционистское отрицание -» определяется через сильное следующим образом -цр •= Ч> Ч>- Как следствие верна импликация ~ р —► -><р, показывающая, что отрицание ~ сильнее, чем интуиционистское отрицание. В паранепротиворечивой версии логики Нельсона интуиционистское отрицание не может быть определено через сильное, а упомянутое соотношение между этими отрицаниями не имеет места. Тем не менее, термин “сильное отрицание” употребляется по традиции и в этом случае.
Теперь несколько слов об обозначениях рассматриваемых логик. Логику с сильным отрицанием и ее паранепротиворечивый вариант Нельсон обозначал N и (см. [59, 9]). В системе обозначений М. Дана [32] эти логики получают имена N и ВГуГ] , соответственно. Мы же будем следовать иной традиции, наиболее распространенной в данное время (см., например, [88]), и обозначать избыточную логику Нельсона через N3, а
паранепротиворечивую логику Нельсона через N4. Эти обозначения связаны с семантикой Крипке для данных логик, которая была разработана для N3 Р.Томасоном [83] и Р. Роутли [75]. Как и в случае интуиционистской логики, Ш-шкалы — это предпорядки. Однако ввиду того, что верификация и фальсификация трактуются в N3 независимо, NЗ-мoдeли имеют две оценки, v+ для верификации и v~ для фальсификации, с дополнительным условием v+(p) C\v~{p) = 0, т.е. атомное утверждение не может верифицироваться и фальсифицироваться одновременно. Опуская это условие, мы получим семантику для N4. Нетрудно проверить (см. [72]), что пара оценок (v+,v~) может быть заменена многозначной оценкой, трех-значной (true, fake, neither) для N3 и четырех-значной (true, false, neither, both) для N4. Именно это определяет выбор обозначений для данных логик.
Разумеется, логика N4 более привлекательна с прикладной точки зрения, так как она позволяет работать с противоречивой информацией. Кроме того, она может быть использована для разрешения некоторых известных логических парадоксов (см. [87]). В то же время, ее изучению было уделено несравненно меньше внимания, чем избыточной N3. В частности, семантические исследования N4 ограничиваются семантикой Крипке. Отсутствует какая-либо специфическая информация о классе N4-расширений, за исключением сведений о классе расширений логики N3. Стоит отметить, что последний класс изучался достаточно интенсивно ( см.[39, 48, 77, 78, 79]).
Итак, имеются две избыточные логики Li и N3, и их паранепроти-воречивые аналоги Lj и N4. В диссертации установлено, что Li точно вкладывается в Lj, а N3 точно вкладывается в N4. Таким образом, отказ от аксиомы избыточности не приводит к потере выразительных возможностей логики. Здесь встает вопрос о том, какими новыми вы-
разительными возможностями обладают логики Lj и N4 по сравнению с избыточными Li и соответственно N3, а также насколько регулярно устроен этот набор новых возможностей? В настоящей работе мы постараемся дать ответ на этот вопрос исследуя решетки расширений логик Lj и N4.
Изучение классов расширений различных логик таких, например, как интуиционистская логика Li (см., например, (22]), нормальная модальная логика К4 [36, 37] и т.д., играет чрезвычайно важную роль в развитии современной логики. В первой части диссертации представлен первый опыт систематического изучения решетки расширений паранепро-тиворечивой логики, а именно логики Lj. Установлена важная черта, отличающая класс Lj-расширений от классов расширений избыточных логик Li и К4. Класс Jhn имеет нетривиальную и интересную глобальную структуру (он трехмерный, в некотором смысле), что позволяет свести его описание, до определенной степени, к хорошо изученным классам промежуточных и позитивных логик. Точнее, класс Jhn является дизъюнктным объединением трех классов: класса промежуточных логик Int, который содержит только избыточные логики; класса Neg, состоящего из негативных логик, т.е. логик с вырожденным отрицанием, содержащих схему ->р; и класса Par собственно паранеггротиворечивых расширений логики Lj, содержащего все логики, не попавшие в первые два класса.
Jhn = Int U Neg U Par.
Заметим, что негативные логики дефинициально эквивалентны позитивным.
Для любой логики L € Par, можно определить ее интуиционистский напарник (негативный напарник Lnty) как наименьшую логику из класса Int (соответственно, из класса Neg), содержащую логику L. Имеются сильные трансляции (т.е. трансляции, сохраняющие отно-
шение следования) логик Lint и в исходную паранепротиворечивую логику L. Логика Lint может быть получена также присоединением ех contradidione quodlibet к L. Таким образом, упомянутая трансляция логики Ьш показывает, что обычные избыточные рассуждения моделируются в паранепротиворечивой логике. В то же время, как было отмечено выше, важным преимуществом паранепротиворечивых логик является возможность различать противоречия, которые не эквивалентны друг другу. В случае класса Lj-расширений структура противоречий паранепротиворечивой логики L эксплицируется в виде формальной системы, а именно, в виде ее негативного напарника Сильная трансляция логики Ьпед в L может быть задана посредством оператора противоречия С(<р) := <р A Поэтому логика L^ действительно может рассматриваться как логика противоречий логики L.
Мы завершим исследование класса Jhn изучением отношения негативной эквивалентности между логиками из Jhn. Логики L\,L2 €,Jhn негативно эквивалентны, если они имеют одно и то же негативное отношение следования, т.е. X hj^ -»<р, если и только если X \~i2 -up для любых множества формул X и формулы <р. Негативная эквивалентность логик из класса Lj эквивалентна также утверждению, что эти логики имеют то же самое семейство противоречивых множеств формул. С конструктивной точки зрения эти факты означают, что две негативно эквивалентные логики имеют одинаковые концепции отрицания и противоречия.
В заключительной главе первой части диссертации мы предложим способ преодолеть вышеупомянутый парадокс минимальной логики. Это будет сделано заменой константы i. на унарный оператор абсурдности A(tp) и последующим определением отрицания как редукции к такой
обобщенной абсурдности:
-нр:= <р -> А{<р).
Идея подобного определения возникает из сравнения оператора противоречия в логике классической опровержимости Карри Ье [28], наибольшем паранепротиворечивом расширении минимальной логики, и оператора необходимости в модальной логике Лукасевича Ь [52, 53]. Мы докажем, что один из модальных парадоксов логики Ь в точности соответствует тому факту, что оператор абсурдности является константой, как в Ье. Более того, оказывается, что в некоторых хорошо известных системах паранепротиворечивых логик отрицание может быть задано именно этим способом. Например, в логике СЬгДО Д. Батенса [13,14] и в максимальной паранепротиворечивой логике Сета Р1 [80, 67] отрицание может быть представлено как сведение к унарному оператору абсурдности.
Во второй части диссертации исследуется решетка расширений паранепротиворечивой логики Нельсона. Здесь существенную роль играет не только интерес к логике Нельсона как альтернативной формализации интуиционистской логики, но и желание проверить, применим ли к этому новому объекту подход, разработанный в первой части работы? И ответ на этот вопрос является положительным, хотя будет обнаружено также существенное отличие структур решеток расширений минимальной логики и паранепротиворечивой логики Нельсона.
В связи с паранепротиворечивой логикой Нельсона возникает вопрос, в каком языке следует рассматривать эту логику. Избыточная логикаN3 рассматривается обычно в языке (V, А, ——») с символами для двух отрицаний, сильного ~ и интуиционистского Причем интуиционистское отрицание, вообще говоря, излишне, так как может быть определено через сильное. При переходе к паранепротиворечивой логике N4 интерпретация -I не ясна, поэтому кажется естественным рассматривать язык
с единственным отрицанием Такой вариант паранепротиворечивой логики Нельсона мы будем обозначать N4. Тем не менее, как мы увидим, присутствие в языке интуиционистского отрицания наряду с сильным естественно и желательно. Консервативное расширение логики N4 в языке (V, А, —►, ±) с дополнительными аксиомами для константы _!_
будет обозначаться N4 . Интуиционистское отрицание определяется в N4^ обычным образом, -мр := <р —► _1_.
Для изучения класса £N4 (£№41) расширений логики Нельсона N4 ^41) необходима адекватная алгебраическая семантика. Нужно найти определяющее логику N4 (N4^ многообразие алгебр такое, что существует дуальный изоморфизм между решеткой подмногообразий данного многообразия и решеткой N4^4 )-расширений. Для избыточной логики N3 такую семантику задает многообразие ^-решеток, которое достаточно хорошо изучено [69, 34, 35, 39, 77, 78, 86]. N4-peшeтки, введенные автором в [116], определяют семантику этого типа для логики N4. Алгебраическая семантика для К41 задается N41-peшeткaми, естественной модификацией К4-решеток. Интересная особенность И4(и К41)-решеток состоит в том, что они имеют целый фильтр выделенных значений.
Преимущество языка с интуиционистским отрицанием становится явным, когда мы начинаем исследование классаК41-расширений. Его строение существенно отличается от строения класса ЗЬп. Прежде всего, в отличие от Лт, содержащего целый подкласс Neg противоречивых логик, логика N4 не имеет нетривиальных противоречивых расширений. Несмотря на то, что логика К4Х паранепротиворечива, она допускает только локальные противоречия. Присоединение к К41 противоречия как схемы формул имеет своим результатом тривиальную логику. Тем не менее, класс £^Ч4Х разбивается на подклассы избыточных, нормальных
логик и логик общего вида. Это разбиение отражает локальную структуру противоречий в К4х-моделях и подобно разбиению класса Лт на подклассы промежуточных, негативных и собственно паранепротиворе-чивых логик. Именно присутствие в языке константы ± позволяет определить класс нормальных логик, соответствующий классу негативных логик в решетке ^-расширений.
Заметим, что отношение негативной эквивалентности, играющее важную роль при изучении класса расширений минимальной логики, вырождается при переходе к К4-расширениям. Два расширения логики N4 (К4Х) негативно эквивалентны, если и только если они равны.
Опишем теперь более точно структуру диссертации. Глава 2 содержит определения важнейших логик из класса Лт и необходимые сведения об алгебраической семантике и семантике Крипке для расширений минимальной логики. Глава 3 посвящена логике классической опровер-жимости, наибольшему паранепротиворечивому расширению логики Ь), играющему ключевую роль в исследовании класса Ц-расширений.
В главе 4 мы исследуем логику Ье' = Ц + {Л V (Л —► р)} и доказываем, что класс расширений этой логики совпадает с классом всех возможных пересечений промежуточных и негативных логик. Более того, каждая логика Ьу расширяющая Ье', имеет единственное представление в виде пересечения промежуточной логики Ь\ и негативной логики 1/2. Логику Ь\ (соответственно, 1/2) мы назовем интуиционистским (соответственно, негативным) напарником логики Ь. Далее, понятия интуиционистского и негативного напарников обобщаются на класс всех ^-расширений. При этом класс Ра г собственно паранепротиворе-чивых Гд-расширений разбивается на попарно непересекающиеся семейства 5рес(Б1,/^), состоящие из всех ЛОГИК имеющих ЛОГИКИ 1\ и 1/2 В качестве своих интуиционистского и, соответственно, негативного напар-
ников. Каждое из семейств Spec(L\, L2) образует интервал в решетке Par с наибольшей точкой Lif)L2. Таким образом, изучение структуры класса Jhn сводится к изучению интервалов вида Spec[L\, L2).
Следующая глава посвящена нахождению удобного представления j-алгебр, которое позволяло бы определять положение различных логик внутри интервалов Spec(L\,L2)- Эффективность полученного представления демонстрируется его применением к многочисленным расширениям минимальной логики, рассматривавшимся К. Сегербершм [76].
В главе б мы вводим отношение =пед негативной эквивалентности логик и, модифицировав технику формул Янкова, доказываем, что решетка Spec(Li, L2)/ =пед изоморфна интервалу Spec(Lk,!^). Мы покажем также, что каждый интервал Spec(L[, L2) содержит бесконечно много классов негативной эквивалентности, а в Jhn имеется континуум различных классов негативной эквивалентности.
Последняя глава первой части диссертации, глава 7, посвящена изучению унарного оператора абсурдности.
Глава 8 начинает вторую часть диссертации, посвященную сильному отрицанию. В первом параграфе определяются два варианта пара-непротиворечивой логики Нельсона. Логика N4 определяется в языке (V, А, —~), где ~ — символ для сильного отрицания, а логика N41 — в языке (V, А,—>,^,1) с дополнительной константой J_. При этом N41 — консервативное расширение как N4, так и интуиционистской логики. Избыточная логика N3 получается присоединением к N4 аксиомы избыточности ~ р —> (р —> q). Причем, полагая ± :=~ (ро —> Ро) можно доказать в N3 дополнительные аксиомы логики N41.
Во втором параграфе логика N4 характеризуется с помощью структур Фиделя [35]. Это непосредственное обобщение результата М. Фиделя из [35] для логики N3. Структуры Фиделя представляют собой импли-
кативные решетки с выделенным семейством одноместных предикатов.
В третьем параграфе семантика N4 задается с помощью твист-структур над импликативными решетками (см. [34, 86]). Причем теорема полноты следует из доказанной здесь же эквивалентности структур Фиделя и твист-структур. Твист-структура — это алгебраическая система, задаваемая на декартовом квадрате импликативной решетки. Причем операции этой структуры согласованы на первой координате с операциями импликативной решетки и “скручены” на второй.
Далее, в 4-м параграфе устанавливается, что класс алгебр изоморфных твист-структурам допускает теоретико-решеточное определение. Введен класс N4-решеток. Доказано, что всякая твист-структура является N4-решеткой, а всякая N4-peшeткa Л изоморфна твист-структуре над А*, импликативной решеткой, определяемой как фактор-решетка Л по конгруэнции специального вида. Откуда следует, что N4 характеризуется К4-решетками.
В следующем параграфе доказывается, что К4-решетки образуют многообразие и устанавливается дуальный решеточный изоморфизм между решеткой £N4 расширений логики N4 и решеткой подмногообразий многообразия 1^4.
В заключительном параграфе главы 8 ранее полученные результаты переносятся на логику N4 и решетку ее расширений £К41. При этом твист-структуры определяются над алгебрами Гейтинга и для любой ^1-решетки Л фактор-структура Л^ также будет алгеброй Гейтинга. Назовем Ах, базисной алгеброй N41-peшeтки А.
В главе 9 развиты начала алгебраической теории ^^-решеток в объеме, необходимом для исследования решетки расширений логики В частности получено представление К41-решеток в виде алгебр Гейтинга с выделенными фильтром и идеалом. Определена пара сопряженных
функторов между категориями N41-решеток и алгебр Рейтинга. Доказано, что если гомоморфизм базисных алгебр может быть поднят HaN4x-решетки, то это делается единственным образом. Показано, что конгруэнции на N41-penieTKe находятся во взаимно однозначном соответствии с импликативными фильтрами. Установлен изоморфизм решеток конгруэнций N4x-pemeTKH и ее базисной алгебры. Как следствие, описаны подрямо неразложимые N41-penieTKH как решетки с подпрямо неразложимой базисной алгеброй. В терминах описанного выше представления сформулирован критерий вложимости и описаны фактор-алгебры N41-решеток.
В заключительной 10-й главе изучается строение решетки N41-pac-ширений, при этом обнаруживается несомненное сходство со строением класса расширений минимальной логики. Хотя различия в строении этих двух классов логик также существенны. Первое из этих отличий состоит в том, что N41 не содержит противоречивых нетривиальных расширений. Минимальная же логика имеет целый класс противоречивых расширений, изоморфный классу расширений позитивной логики.
В главе исследованы связи между логикой L, расширяющей N41, и ее интуиционистским фрагментом. В решетке £N4X расширений логики N41 определены подклассы избыточных логик Ехр, нормальных логик Nor и логик общего вида Gen, играющие роль аналогичную классам Int, Neg и Par в решетке расширений минимальной логики. Исследованы связи между классами Exp, Nor и Gen с помощью определения избыточных и нормальных напарников для логик из класса Gen.
Даны первые приложения развитой теории решетки К41-расширений. Во-первых, полностью описана решетка расширений логики N4XC, получающейся присоединением аксиомы Дам мета к N41. Доказано, что все ее расширения разрешимы и конечно аксиоматизирумы, а по произ-
вольной формуле можно определить, какое расширение логики ^ХС она аксиоматизирует.
Во-вторых, описаны табличные, предтабличные логики и логики, обладающие интерполяционным свойством Крейга в решетке расширений логики N4-4
Часть I Reductio ad absurdum
♦
to
20
*
Глава 2
Минимальная логика. Синтаксис и семантика.
В первой части диссертации, посвященной минимальной логике, мы будем рассматривать логики и дедуктивные системы, сформулированные в следующих языках.
£+ := {л, у, -*}, С1 := С+ U {!}, Г := £+ U {-}.
Расширения минимальной логики допускают эквивалентные представления в языках С1 и СТ.
Логикой мы называем множество формул, замкнутое относительно правил подстановки и modus ponens. Как правило, мы будем задавать логики как множества теорем дедуктивных систем Гильбертовского типа с правилами подстановки и modus ponens. Поэтому для задания логики будет достаточно перечислить ее аксиомы. Если L — логика, а X — множество формул в том же самом языке, то L + X обозначает наименьшую логику, содержащую L и X. Символом + будем обозначать также операцию взятия точной верхней грани в решетках логик. Отношение X \-l (р означает, что формула р может быть получена из элементов X и L с помощью правила modus ponens.
Обозначим через J7* тривиальную логику, т.е. множество всех формул
21
языка С*, * € {+,±,->}.
Определим ряд важнейших логик. Отметим, что при выборе обозначений мы следовали монографии В. Раутенберга [72].
Позитивная логика Lp — это наименьшая логика в языке С+ содержащая следующие аксиомы:
1 ■ Р->{<!-> Р)
2. (p-y(q~* г)) -> ((р -»?)-> (р -* г))
3- (р A q) -* р
4. (pAq)-+q
5. (р —> q) —> [(j> г) —* (р —> (q Л г)))
6. р-> (pVg)
7. q-*(pVq)
8. (р -> г) ->((5 ->г) -»((р V д) -+ г))
Отметим, что позитивная логика удовлетворяет теореме дедукции:
X и {<р} l-Lp lp & X\-Lp
В доказательстве этой теоремы существенным образом используются аксиомы 1 и 2 позитивной логики, а также то, что modus ponens является единственным правилом вывода. Этим условиям удовлетворяют все логики, рассматриваемые в настоящей диссертации, поэтому теорема дедукции остается верной для всех рассматриваемых ниже логик.
Классическая позитивная логика Lk+ также определяется в языке С+ и может быть аксиоматизирована относительно Lp одной из следующих аксиом:
Р ({ря) Р) Р (закон Пирса)
E. p V (p —> q) (обобщенный закон исключенного третьего)
Версия Lj1 минимальной логики в языке CL задается приведенными выше аксиомами 1-8. Эквивалентная версия минимальной логики Lp в языке СГ с символом отрицания задается аксиомами 1-8 и следующей аксиомой:
А. (р —» q) —»► ((р —j► -лq) —» ->р) (reductio ad absurdum)
Чтобы придать точный смысл утверждению об эквивалентности двух версий минимальной логики, определим трансляцию в из языка СГ в язык С1 и обратную трансляцию р из С1 в /Г следующим образом.
Для любой (р € формула 9{р) языка С1 получается из р заменой
каждой подформулы вида -*ф на подформулу ф —*► _L. Если р Е TL, то р(<р) — это формула в языке полученная из р заменой каждого вхождения константы J_ на подформулу ->(р —► р), где р — фиксированная пропозициональная переменная. Для множества формул X С обозначим через 0(Х) множество {0(р) \ р Е X}. Соответственно, для ХСЯ полагаем р(Х) := {р(р) | <р € X}.
Предложение 2.0.1 1. Для любых множества формул X С Т" и
формулы р Е верно X Ьц- р, если и только если 0(Х) hLj±
Более того, Lj(-</?<-► рд(р) для любой формулы р.
2. Для любых множества формул X С TL и формулы <р G верно р, если и только если р(Х) Ьц- р(р).
Более того, Lj1 Ь р вр{р) для любой формулы р.
□
Таким образом, определенные выше трансляции сохраняют дедуктивные свойства, а последовательное применение двух трансляций дает формулу, эквивалентную исходной. Ввиду этих фактов мы может свободно
переходить от языка С1 к языку £“* и обратно. В дальнейшем мы опускаем индексы в обозначении минимальной логики и не будем уточнять с какой из ее версий мы работаем в данный момент. Точно также мы будем поступать и с расширениями минимальной логики.
Интуиционистская 1л и минимальная негативная логика Ьп аксиоматизируются относительно минимальной логики в языке С1 следующим образом:
IЛ = Ц + {±-*р}, Ьп = Ц + {±};
а в языке £“*:
и = Ц + {^р -> (р -> д)}, Ьп = У + {-.р}.
Классическая логика Ьк, логика классической опровержимости Ье и максимальная негативная логика Ьтп задаются присоединением к интуиционистской логике 1л, минимальной логике Ьд и, соответственно, минимальной негативной логике Ьп закона Пирса Р либо обобщенного закона исключенного третьего Е.
Ьк = 1л+{рУ(р -> д)}, Ье = ^+{рУ(р -> д)}, Ьтп = Ьп+{рУ(р -» д)}.
Позитивные фрагменты логик Ьк, Ье и Ьтп совпадают с классической позитивной логикой, тогда как позитивные фрагменты логик Ы, Ь} и Ьп совпадают с позитивной логикой.
Ьк+ = ЬкпЯ’ = ЬеП/'+ = ЬтпПЯ-,
Ьр = ЫП.Г+ = ЦП?+ =1пГ\?+.
Все введенные логики, кроме позитивной и классической позитивной, являются расширениями минимальной логики. Класс всех нетривиальных расширений логики Ц обозначим Лт, класс всех расширений —
Лт+. Ясно, что класс логик Лт+ образует решетку, причем точной верхней гранью логик Ь\ и является логика Ь\ +а точной нижней гранью — пересечение логик Ь\ П 1у2- Для произвольной логики Ь, решетку ее расширений с решеточными операциями + и П мы обозначаем £Ь.
Предложение 2.0.2 Следующие формулы доказуемы вЬу
1. -г-|(р V -чр)
2. (р —► —•д) - — ->р)
3. (р -> я) - > (-,9 _> -,р)
1 г > £ -» ->(рЛд)
5. ~'(Р V я) (~'Р А -19)
6. р-*-,-,р
7; -'{Р А ->р)
8. (рУд) -* -’(-’Р А ->д)
9. (р Дд) -*• V -1?)
10. (р->9) -> • -,(р А ->9)
и. ((р -»д) V ' г) -> ((р V г) ->(д V г))
□
Для доказательства этого утверждения читатель может заглянуть в тот или иной учебник классической логики, например, [56], и заметить, что приводимые там стандартные доказательства перечисленных выше формул используют только аксиомы логики IО*.
Следующее предложение дает информацию о результатах присоединения к логике Ц различных новых аксиом.
Предложение 2.0.3 [76, р.50]
1. Ьк = ц + {<р} , где <р — одна из следующих формул:
(a) -иир -> р;
(b) (-.р -> д) -»(-•<? -* р);
(c) (->р -» -I?) -»(?-»р);
(Л) -'{-'Р Л -’<?) —»■ (р V д);
->(-’р V ->д) -> (рЛд);
(7; -|(рЛ->д) —»(р —» д)-
2. Ьк ф Ц + {р V -чр} = Ы + {(р -»д) -»(->р V д)}.
3. Ц + {р V -чр} # У + {-чр V 1->р} = Ц + {-1(р Л?)-* (-чр V ->д)}.
4- Ы = Ц + {(->р V д) —»(р —» д)}.
□
Ниже мы приведем необходимые определения и факты об алгебраической семантике пропозициональных логик. Более детальную информацию читатель может найти в [71, 72].
Пусть Д — алгебра в языке £+и{1} (£1и{1}, £"’и{1}) с дополнительной константой 1 для единственного выделенного элемента. Отображение V : {ро,Р1, Л из множества пропозициональных переменных
в универсум алгебры Д называется А-оценкой. Каждая Д-оценка расширяется естественным образом на множество всех формул. Формула <р истинна в Д, пишем А |= если = 1 для любой Д-оценки V. Истинную в Д формулу называем также тождеством алгебры Д.
Очевидно, множество формул ЬА := {(р | Д \= (р} является логикой, которую мы будем называть логикой алгебры А. Логика класса алгебр К — это пересечение логик алгебр из класса /С, ЬК := [){ЬА \ А £ К}.