Содержание к диссертации
Введение
1 Истинностно-функциональные семантики 14
1 Семантика голосования 17
2 Перерандомизирующая семантика 20
3 Семантика сходства 21
4 Семантика рисков, или диалоговая семантика 26
5 Семантика допустимости 28
6 Рассуждения в теории меры 32
7 Семантика приближений 33
8 Импликация 36
9 Отрицание 39
2 Формализация многозначных логик 41
1 Логика высказываний 41
2 Логика первого порядка 44
3 Алгебра 48
4 Вывод 51
5 Логика отмеченных формул 56
6 Секвенциальные и табличные исчисления 59
7 Резолюция 64
3 Функциональный анализ многозначных логик 66
1 Основные понятия 66
2 Критерии полноты и 5-полноты 70
3 Предикатная характеризация-замкнутых классов 73
4 Метод резолюций для смешанной логики Поста 76
1 Смешанная логика Поста PostL 78
2 Резолюция для PostL 81
3 Замечания 86
5 Теорема Чена 88
1 Идеалы, отношения конгруэнтности и проблема представления 89
2 Линейно упорядоченные MV-алгебры 93
3 Упорядоченная абелева группа G[c] 96
4 Применение к бесконечнозначной логике Лукасевича 103
6 Метод резолюций на основе теоремы представления дистрибутивных решёток с операторами 104
1 Дуальность по Пристли 105
2 Модели, основанные на дуале Пристли 115
3 Автоматическое доказательство теорем 118
4 Канонические расширения 120
7 Эффективное доказательство теорем в логиках Лукасевича 126
1 Логика Лукасевича и линейная алгебра 126
2 Первый метод проверки общезначимости 132
3 Второй метод 134
Заключение 137
- Семантика рисков, или диалоговая семантика
- Секвенциальные и табличные исчисления
- Предикатная характеризация-замкнутых классов
- Идеалы, отношения конгруэнтности и проблема представления
Введение к работе
Многозначные логики появились в 20-х годах XX века в работах Поста и Лукасевича. Несколько позднее было предложено ещё несколько многозначных логик, таких как логика Бочвара, логики Гёделя, логика Клини. Интересный библиографический экскурс в многозначные логики можно найти в [7]. Изобретение этих логик было мотивировано разными задачами. Так, Лукасевич и Бочвар исходили из философских предпосылок, вводя третье значение в свои логики для формализации неполного или противоречивого знания; Пост и Гёдель руководствовались более техническими соображениями, когда обобщали классическую логику в n-значных системах; Клини же просто искал удобный формализм для анализа понятия частично определённой рекурсивной функции. Однако все эти логики объединяет важная отличительная особенность: в них ме-татеоретически заложена концепция, которую называют истинностной функциональностью. Согласно ей, всякое высказывание имеет некоторое значение истинности, и это значение может быть однозначно вычислено некоторой заранее определённой функцией по значениям входящих в это высказывание подвысказываний. Так, в случае конъюнкции А А Б высказываний А и В искомой функцией будет некоторая функция /л от значения А и значения В.
Если логика истинностно-функциональна, это непосредственно означает существование метода вычисления значения истинности для любого высказывания, записанного на языке этой логики. В этом состоит привлекательная в техническом смысле сторона многозначных логик: по любой формуле можно легко сказать, что она «значит». Сохраняется ли эта при-
влекательность многозначных логик в теории вывода? К сожалению, нет, поскольку с ростом числа истинностных значений растёт и то внимание, которое им приходится уделять, а в это время падает эффективность рассуждений.
Что же в таком случае делать, если возникают задачи, требующие многозначного решения? Отказаться от истинностной функциональности и перейти в другую концепцию? Как следует из данной работы, этого делать не нужно, поскольку полученные в ней результаты позволяют эффективно строить выводы, оставаясь в рамках концепции многозначности.
Степень разработанности проблемы. В нашей стране было получено большое количество результатов в области многозначных логик. Среди них можно особо отметить следующие: вычисление Яблонским всех пред-полных классов функций для трехзначной логики Поста в 1954 году, а также нескольких классов для случая к ^ 4 значений в 1958 году; доказательство существования /с-значных замкнутых классов функций, не имеющих конечного базиса, для к > 2, найденное Яновым и Мучником в 1959 году (см. [30]); определение функциональных свойств логик Лукасевича Финном [4] в 1970 году; получение метода аксиоматизации произвольных конечнозначных логик Аншаковым и Рычковым [1] в 1982 году; установление Карпенко [9] связи импликации Лукасевича с классами простых чисел в 1999 году; построение Косовским и Тишковым [17] секвенциальных исчислений для классов конечнозначных логик в 2000 году. Также можно указать оригинальное доказательство полноты бесконечнозначной логики Лукасевича относительно реляционных семантик с тернарным отношением достижимости, полученное Васюковым в [88]. За рубежом многозначная логика в наше время является сложной разветвлённой отраслью науки. Многие работы общетеоретического характера публикуются не отдельными авторами, а коллективами авторов, например, статья по секвенциальным исчислениям с метками для конечнозначных логик [36] или монография по алгебраическим основаниям многозначных логик [46].
Актуальность темы диссертации. Сегодня для бесконечнозначных
логик не существует хорошо обоснованной теории доказательств, хотя для
конечнозначных логик табличные исчисления без сечений были построены
ещё Руссо [80] в 1967 году. Некоторые исчисления для бесконечнозначных
логик Лукасевича всё же определяются в литературе, например, Агуц-
цоли и Чиабаттони [31] в 2000 году строят секвенциальное исчисление
для бесконечнозначной логики, опирающееся на идею Мундичи о сводимо-
^ сти проблемы разрешимости с бесконечнозначной логики на подходящий
класс конечнозначных логик, и, следовательно, основанное на исчисле-
Г ниях для конечнозначных логик. В 2001 году Софрони-Стоккерманс [85]
г';! К предложила метод доказательства теорем для большого класса многознач-
ных логик, основанный на теореме представления алгебр истинностных
значений. Кроме своей эффективности, этот метод интересен ещё и тем,
что в нём посредством структур Крипке устанавливается соответствие
между многозначными и модальными логиками. К сожалению, метод [85]
неприменим к ряду широко распространённых бесконечнозначных логик.
Данный метод исследован в диссертации, и на основе этого исследования w
сделан вывод о возможности его обобщения на класс бесконечнозначных
логик на основе подходящей теоремы представления алгебр истинностных
. ' значений.
.І і
Цель диссертационного исследования — формирование единого подхода к теории вывода многозначных логик на основе изучения их семантик и исчислений.
Предмет исследования — это логические семантики различных видов, логические исчисления для многозначных логик, теории, в которых формализована концепция многозначности, и модели таких теорий.
Методы исследования. В работе используется логическая техни-
if ка, как традиционная, например, секвенциальные логические исчисления,
так и нетрадиционная: исчисления с «отмеченными формулами», S-классификация замкнутых классов функций многозначных логик, дуальные многозначным семантикам топологические модели. Автором работы вводится оригинальный метод на основе исчисления резолюций для доказательства теорем в многозначных логиках с линейно упорядоченными
множествами истинностных значений.
Структура и объём работы. Диссертация состоит из введения, семи глав, заключения, приложения и списка литературы.
В первой главе — «Истинностно-функциональные семантики» — осуществляется содержательное философское истолкование концепции истинностной функциональности, лежащей в основе явления многозначности. Раскрывается понятие истинностно-функциональной семантики, приводятся наиболее распространённые варианты таких семантик, и среди них: семантика голосования, семантика сходства, семантика рисков, семантика допустимости, семантика приближений.
Во второй главе — «Формализация многозначных логик» — даются строгие определения понятий многозначной теории вывода, таких как: логика высказываний, логика первого порядка, абстрактная алгебра, логический вывод, формула с метками, логическое исчисление (секвенциальное, табличное, гильбертовское, резолютивное).
Третья глава — «Функциональный анализ многозначных логик»
— содержит изложение основных результатов анализа и классификации
функций многозначных логик в классе функций n-значных логик Поста.
Приводятся определения замкнутых и .^-замкнутых классов функций
многозначных логик, а также критерии полноты и «S-полноты для этих
классов. Даётся предикатная характеризация 5-замкнутых классов по
Марченкову.
Четвёртая глава — «Метод резолюций для смешанной логики Поста»
— посвящена исследованию так называемой смешанной логики Поста
PostL, предложенной Косовским и Тишковым [17], и обобщающей в своём
исчислении свойства класса исчислений всех n-значных логик Поста. В
этой главе автором строится корректное исчисление резолюций в духе [35]
для смешанной логики Поста.
В пятой главе — «Теорема Чена» — впервые на русском языке даётся полное оригинальное доказательство теоремы Чена о полноте бесконечнозначной логики Лукасевича относительно многообразия MV-алгебр.
Шестая глава — «Метод резолюций на основе теоремы представления дистрибутивных решёток с операторами» — освещает проблематику представления алгебр многозначных логик и знакомит с методом поиска доказательства теорем многозначных логик, основанном на результате [83]. В данной главе мы исследуем теорию вывода многозначных логик с алгебраической точки зрения. Результатом исследования является формулировка критерия применимости к произвольной многозначной логике предложенного в [85] метода резолюций на основе теоремы представления Пристли для дистрибутивных решёток с операторами.
В седьмой главе — «Эффективное доказательство теорем в логиках Лукасевича» — приводятся некоторые оптимизационные методы доказательства теорем в логиках Лукасевича. В частности, для бесконеч-нозначной логики Лукасевича Ьк0 даётся метод (см. [37]), основанный на теореме Мак-Нотона [19].
В заключении показано, из каких вспомогательных результатов и посылок следуют основные результаты работы. Приводятся научно значимые следствия из основных результатов и общего содержания работы. В особенности указывается на открывающуюся перспективу создания общей теории вывода для большого класса логик, основанных на дистрибутивных решётках или полурешётках с оператором резидуации, т.е. для нечёткозначных логик (включая логики Лукасевича) и релевантных логик.
В приложении доказывается вложимость произвольного пропозиционального немодального гильбертовского исчисления в исчисление резолюций с одноместными предикатами и приводится пример, иллюстрирующий подобное вложение: доказательство рефлексивности импликации в аксиоматической системе {B,C,W,Ki,X3}, рассмотренной в [7], с помощью программы автоматического поиска доказательства теорем OTTER. Таким образом доказано, что данная система аксиом является аксиоматизацией импликативного фрагмента классической логики высказываний.
Обозначения используются стандартные. Выражение, заключённое в фигурные скобки { и }, обозначает множество. Запись {х : Р} читается
как «множество таких элементов х, для которых выполняется условие Р». Выражение вида [х, у], если не оговорено иное, обозначает числовой отрезок от х до у включая сами х иу. Запись [х, у) обозначает отрезок от х до у, включая х, но исключая у. Используются операции, определённые на (частично) упорядоченных множествах: тахМ — максимальный элемент множества М, minM — минимальный элемент множества М, S infM — наибольшая нижняя грань, или инфимум, множества М,
'Л-
sup М — наименьшая верхняя грань, или супремум, множества М. Множества натуральных, целых, рациональных и действительных чисел і | обозначаются, соответственно, N, Z, Q и Ш. Множество подмножеств заданного множества М будет обозначаться как V(M). Для определения функций используется запись вида / : X —> Y, которая читается как «функция /, отображающая множество X на множество У». Иногда функции могут задаваться на разных частях области определения, и тогда условные выражения для каждой части области определения объединяются фигурной скобкой. Выражение хп является сокращением
п раз
* для х х х х, причём п — это неотрицательное целое, ах— это
, разновидность умножения или конъюнкции.
" I Принимаются обозначения, доопределяемые в конкретных контекстах:
Form — множество всех формул (языка данной логики), Var — множество всех переменных, Term — множество всех термов. Для предикатных
" констант в первопорядковой логике и для пропозициональных переменных
употребляются символы P,Q,R,Pi,Qi,Ri,...; для произвольных формул
— А, В, С, А\, В\, Сі, Как правило, количество аргументов предикат
ных и функциональных констант не указывается. Обозначения могут быть
нестандартными, если это способствует более лёгкому чтению текста.
Предпошлём теперь формализованным изысканиям краткое содержательное истолкование смысла истинностных значений многозначных логик.
Возьмём такое упорядочение истинности (или упорядочение уверенности) на множестве истинностных значений {0,1}, которое сопоставляет О
т т
/
JL F
Рис. 1: Упорядочение истинности, упорядочение знания и решетка ЧЕТВЕРКА.
с наименьшей истинностью, или уверенностью, а 1 — с наибольшей. Будем писать F вместо ОиТ вместо 1, как в левой части рисунка 1.
Совершенно иная интерпретация истинностных значений, принятая в исследованиях искусственного интеллекта и программировании, — это упорядочение знания (или упорядочение информации), где 0 означает отсутствие знания, а 1 — всезнание. Будем писать ± вместо ОиТ вместо 1, см. центральную часть рисунка 1. С философской точки зрения, в интерпретации этого типа находит своё отражение эпистемологическая неопределённость.
Полезно иметь оба упорядочения в многозначной логике одновременно. Вслед за работой [38] вообразим, что у нас есть множество распределенных агентов, работающих над одной проблемой. Каждый агент дает двухзначный ответ из множества {T,F}, упорядоченного по истинности. А что делать, если какой-то агент не дал ответа, или же разные агенты дали разные ответы? В первой ситуации мы ничего не знаем, а поэтому должны взять истинностное значение JL; во втором случае мы берем значение Т, чтобы смоделировать общее, даже противоречивое знание. Уникально определенные значения F и Т находятся в середине. В результате получается решетка алмаза знания, изображенная в правой части рисунка 1. Эта решетка вместе с порожденными ей многозначными логиками исследуется в многочисленных статьях, начиная возможно с Лукасевича [67, 18], который считал получающуюся логику модальной, осуществляя попытку создания модели аристотелевской модальной силлогистики. Лукасевич
JL Рис. 2: Семизначная решетка для моделирования транзисторов MOS.
рассматривал импликацию, полученную с помощью резидуации точной нижней грани решетки, а также с помощью нескольких одноместных связок для добавления/удаления/перестановки истинных значений. Они оба, и в [18], и в [38], используют отрицание, которое переставляет JL и Т, F и Т. Решетка алмаза знания в частности удобна для передачи паранепро-тиворечивого знания, т.е. для осуществления вывода в противоречивых ситуациях [38].
Решетка знания становится решеткой алмаза знания, если повернуть ее на 90 градусов против часовой стрелки. Получается, что такие пересекающиеся решетки, где присутствуют оба вида упорядочения одновременно, могут быть обобщены из четырехзначного случая, см., например, [54].
Истинностные значения иногда мотивируются областями применения и имеют технический, а не логический смысл. Вот пример, взятый из [62]: у транзистора MOS на входе и выходе уровень сигнала разный из-за физического эффекта деградации. Эта ситуация моделируется семизначной логикой с N = {F,T,F',T',T,T',±} и порядком ^ изображенным на рис. 2. Значения Т и F соответствуют полным сигналам, тогда как F' и Т" соответствуют деградированным сигналам. В неисправной контактной схеме сигналы могут столкнуться в узле,
давая результирующие сигналы Т и Т\ Значение JL соответствует неподключенным узлам («отсутствие сигнала»). При данных условиях узел, в котором встречаются два сигнала жиг/, вычисляется просто как точная верхняя грань в решетке индуцированной порядком ^. Заметим, что у нас есть две решетки алмаза знания, соединенных вершинами друг друга. Транзисторы MOS моделируются пропозициональными связками в логике, чья семантика определяется техническими характеристиками специфических транзисторов. В статье Эсакиа [28] была дана естественная алгебраическая характеризация этой логики с помощью т.н. булевых каскадов. Получающаяся логика является суперинтуиционистской, она удовлетворяет ослабленному закону Пирса.
В заключение упомянем о двух применениях многозначной логики в философских аргументах: первое — это парадокс кучи и его разрешение в логике Лукасевича. Парадокс может быть запёчатлён в следующей импровизированной аксиоматической системе:
(А) Одна крупинка песка не является кучей.
(Ві) Добавляя одно зернышко песка к і зернышкам, которые еще не куча, кучу не получим.
(С) 100000 зернышек песка являются кучей.
Утверждения (Л), (#1)11^99999 и (С) классически противоречивы. Изменение размера (Ві) до, скажем, кучи из 27000 зерен выглядит неправдоподобно, так же как и выбрасывание (А) либо (С). В логике Лукасевича можно разрешить данный парадокс допустив, что (Ві) меньше истины. Довольно частое применение (Ві) истощает «доверие», заложенное в заключении, и таким образом разрешает парадокс.
Более важным является результат Хайека и Париса [60] о формализации парадокса лжеца (задаваемого, например, предложением «Это предложение ложно.») на базе логики Лукасевича, с применением многозначного предиката истинности. Показано, что идея использования многозначного предиката приводит к непротиворечивому определению
истинностного предиката в арифметике Пеано, которое, как известно, невозможно в классической логике. Интересно, что арифметика может оставаться классической, и только определение истины должно быть многозначным.
Семантика рисков, или диалоговая семантика
В [52] Жиль предложил семантику для уровня истинности высказывания, основанную на понятии риска, который навлекает на себя агент, утверждающий, что данное высказывание истинно. Рассмотрим случай пропозициональной переменной. Идея состоит в том, что, утверждая Р, агент а рискует оказаться неправым, причём по принятому ранее соглашению «правильный ответ» должен быть подтверждён результатом некоторого испытания. Так, например, можно заранее принять, что рыночный тип экономики на самом деле прогрессивный, если первое же государство, которое мы рассмотрим, будет соответствовать данному высказыванию, или, скажем, если большинство из опрошенной достаточно репрезентативной группы людей согласятся с ним, и ложно — в против-i iJ . ном случае. Отсюда не может существовать требования, что каждый раз в результате испытания агент будет получать один и тот же ответ. Цена ошибки, т.е. риск агента а, такова, что он в случае ошибки должен выплатить противнику один кредит (иными словами, противник получит одно очко). Конечно, в такой обстановке было бы бессмысленно для а утверждать что бы то ни было, так как при этом нет надежды на выигрыш. Аналогично известному случаю из теории вероятностей под названием «Голландское пари»1, мы тем не менее можем представить, что противник готов заплатить а п кредитов, чтобы тот утверждал Р. Очевидно, что если п = 1, то а с готовностью будет утверждать Р, в то время как, если п = О, а скорее воздержится от утверждения, что Р истинно, потому что в противном случае он всё равно не получил бы никакой выгоды.
Dutch book (англ.); начало жизни этого термина в теории вероятностей относят к работе Рамсея [78]. Таким образом, инфимум множества таких п є [0,1], для которых а согласился бы сделать утверждение, служит мерой величини риска агента а, утверждающего Р (обозначим как (Р)). Также очевидно, что если ос уверен в том, что испытание, которое он проведёт, подтвердит Р, тогда можно ожидать, что эта величина риска будет мала, и наоборот. Поэтому в качестве уровня истинности переменной Р для агента а можно взять
Данные рассуждения очень похожи на Голландское пари в теории вероятностей (ср. [78], см. также [82]). И в самом деле, здесь (Р) идентифицируется с субъективной вероятностью события Р, которую агент а может вычислить просто на основании частоты предшествующих случаев. Различия появляются, однако, при рассмотрении сложных высказываний, содержащих связки. Согласно Жилю, нужно придерживаться следующих правил для утверждения: а, утверждающий - А, обязуется заплатить противнику один кредит, если противник утверждает А, при этом противник обязан заплатить штраф в один кредит агенту а, если А оказалась ложной. а, утверждающий AV В, обязуется утверждать или А, или В, выбор делает а. а, утверждающий А А В, обязуется утверждать или А, или В, выбор делает противник а. И вновь, пусть (А) является инфимумом множества п Є [0,1] таких, что получив плату в размере п кредитов, а согласится утверждать А. Допуская, что а обладает разумными предпочтениями, мы можем рассуждать об (А) следующим образом. Если п (А), тогда а скорее предпочёл бы проиграть п кредитов, нежели утверждать А, в то время как, если п {А), а предпочёл бы скорее утверждать А, нежели проиграть п кредитов. С этой точки зрения мы можем видеть в приведённом правиле для -v4, что п (- А), только если а предпочёл бы, чтобы противник утверждал А, нежели выиграл 1 — п, или, что то же самое, а предпочёл бы проиграть 1 — п, нежели утверждать А самому. Отсюда мы видим, что В случае правила для AWB, если п {AVB}, тогда а скорее предпочтёт избрать одну формулу из Л и В и утверждать её, чем потерять п кредитов, поэтому минимум (А) и (В) должен быть меньше, чем п. Обратно, если этот минимум меньше п, то так как А свободен в выборе дизъюнкта, он предпочтёт утверждать А V В, нежели потерять п кредитов. Значит, В терминах уровней истинности агента а эти тождества могут быть записаны в уже знакомой нам форме: т.е. в форме равенств семантики связок первого типа. Те же самые идеи, что понятие уровня истинности связано с риском агента, были высказаны в более поздней статье [53], где однако вместо риска фигурирует полезность агента. Идея этой семантики, рассмотренной в [69], состоит в отождествлении уровня истинности, который агент а присвоил бы высказыванию А, с той лёгкостью, с которой а может принять А, или убедиться в А. Эта лёгкость измеряется просто по соотношению множества независимых доводов, которые имеются у а за или против А, к тем из них, которые говорят за А. Первоначально у агента а предполагается наличие конечного множества W миров, и довод за (против) пропозициональной переменной Р есть в точности мир х Є W, такой что х [= Р (соответственно, х Р). Довод за конъюнкцию А А В — это пара (аі,а2), где ах — довод за А, и а2 — довод за В, в то время как довод против конъюнкции А А В — это пара (аі,а2), где либо а і есть довод против А, и а2 является элементом некоторого выделенного множества ZB миров-заполнителей, присутствие которых указывает агенту среди всего прочего, что это довод а\ против первого конъюнкта, либо а2 есть довод против В, и а% является элементом некоторого выделенного множества ZA миров-заполнителей с аналогичными свойствами. Сходным образом, довод за дизъюнкцию А V В — это пара (аг, а2), где либо а\ есть довод за А, и а2 является элементом некоторого выделенного множества ZB миров-заполнителей, либо а2 есть довод за В, и а,\ является элементом некоторого выделенного множества ZA миров-заполнителей, в то время как довод против дизъюнкции А У В — это пара (ai,a2), где аг — довод против А, и а2 — довод против В.
Секвенциальные и табличные исчисления
Секвенциальное доказательство с корнем, помеченным Г, называется секвенциальным доказательством секвенции Г (в исчислении SC). Различные секвенциальные исчисления обладают разнообразными структурными и геометрическими условиями, которые ограничивают число и внешний вид выводов и таким образом характеризуют соответствующие логики. Например, уже в статье Генцена [51] интуиционистская логика была получена с помощью ограничения суккцедентов до самое большее одноэлементных множеств. Присутствие или отсутствие этих структурных условий у секвенциальных исчислений определяет два различных прочтения секвенций. Первый случай (с наличием структурных условий) традиционен в теории доказательств, при этом антецеденты и суккце-денты — обычно множества или последовательности объектов. В таких исчислениях секвенции вида Лі,..., Ат =Ф ь ..., Вп интерпретируются как где х — это некоторая разновидность конъюнкции или произведения, а + — разновидность дизъюнкции или суммы.
Для некоторых многозначные логики, включая логики Геделя, Лука-севича и паранепротиворечивую логику J% такие исчисления секвенций были построены в [47, 77, 33]. Все они являются внутренними.
Для того, чтобы осуществлять выводы в многозначных логиках требуется как-то расширить базовый аппарат секвенциальных исчислений. Одним из возможных расширений является класс гиперсеквенциальных исчислений. Они получаются из секвенциальных исчислений допущением конечного множества секвенций вместо единичных секвенций. Гиперсеквенция — это выражение вида где каждая есть обычная секвенция. В гиперсеквенциях символ «» обычно интерпретируется как дизъюнкция. Несколько конечно-и бесконечнозначных логик, включая логику Лукасевича, логику Геделя, логику С Уркварта были аксиоматизированы с использованием аналитических гиперсеквенциальных исчислений в [33, 34, 44].
В классической логике по теореме дедукции (2.9) эквивалентно согласно [80] обозначает утверждение «существует такое число г, являющееся элементом множества истинностных значений N, при котором множество ТІ содержит формулу А, обладающую свойством f={ г} А».
Схема табличного правила — это пара (А,С), где А — схема формул, называемая посылкой, а С — непустое семейство непустых множеств схем формул, называемое заключением. Элементы С называются расширением. Схема правила замыкания — это множество схем формул. Например, одна из типичных схем правил в классической логике — это схема.
Табличное исчисление — это множество схем табличных правил и схем правил замыкания. Каждое табличное исчисление ТС индуцирует отношение выводимости на множествах формул Ф. Дерево табличного доказательства, или просто таблица, для множества формул Ф — это дерево, помеченное формулами и определенное индуктивно: 1. Пустое дерево — это таблица для Ф. 2. Если Т — таблица для Ф, тогда таблицей будет и дерево, получающееся из Т добавлением к ней вершины, помеченной формулой А Є Ф, и соединением новой вершины ребром с концевой вершиной некоторой ветви дерева Т. 3. Если Т — таблица для Ф, А — ярлык ветви В дерева Т и А — это посылка в подстановочном случае правила исчисления ТС с расширениями С, тогда таблица для Ф получается добавлением к В дополнительно \С\ поддеревьев, каждое из которых содержит в качестве меток только формулы из расширения С.
Ветвь В, чьи ярлыки — это надмножество подстановочного случая правила замыкания исчисления ТС, называется замкнутой. Таблица замкнута, если все ее ветви замкнуты. Замкнутая таблица для Ф — это табличное доказательство множества формул Ф.
Семантика отмеченных секвенций Г определяется так: f= Г, если и только если \/АеТА. Подстановочные случаи секвенциальных аксиом соответствуют общезначимым формулам, а схемы секвенциальных правил сохраняют общезначимость: если все посылки правила общезначимы, то заключение тоже общезначимо. Другими словами, секвенциальные правила — это КНФ-представления их посылок. По индукционному предположению получается корректность секвенциального исчисления: существование секвенциального доказательства с корнем Г влечет общезначимость секвенции Г.
Табличные доказательства двойственны секвенциальным: пусть Г = {Iff [A : \S\A Є Г}. Табличное доказательство показывает, что множество формул Г невыполнимо, из чего следует общезначимость Г. Следовательно, подстановочные случаи табличных правил сохраняют выполнимость: если посылка выполнима, тогда по крайней мере в одном расширении все формулы выполнимы. Табличные правила — это ДНФ-представления их посылок. Таблица замыкается, если каждая ее подтаблица невыполнима. Как и следование, секвенциальные и табличные правила могут быть получены из теорем 2.2 и 2.3. Если определить Sr3,Ski как в теорме 2.2, тогда следующие секвенциальное правило и табличное правило корректны и полны относительно связки, входящей в посылку, при условии, что множество знаков полно относительно S:
Предикатная характеризация-замкнутых классов
В этой главе мы исследуем многозначную смешанную логику Поста PostL, которая была введена в (17]. Смешанная логика Поста — это логика многосортного языка, её предикаты задаются выражениями вида Ра- с, где а, 6, с — положительные целые числа. Мы снабжаем эту логику правилом резолюции, необходимым для автоматического доказательства теорем. Так как PostL является логикой конечнозначных предикатов на основе неравенств, метод резолюций для этой логики может быть применён также к вычислениям систем неравенств с переменными по рациональным числам, записанных на PostL. Логика PostL определяется в параграфе 1, где мы приводим её секвенциальное исчисление. Секвенциальное определение удобно с точки зрения представления множеств формул как конечных дизъюнкций для обработки их по правилу резолюции. Мы определяем внутренний и внешний языки. В параграфе 2 мы даём функцию перевода S, которая отображает многозначные формулы PostL в их интерпретации в 2-значных формулах классической первопорядковой логики. Итак, PostL определима в классической первопорядковой логике (результат был доказан теоремой 8.3.2 в [17]). В параграфе 2 мы также даём доказательство непротиворечивости и полноты многозначной бинарной резолюции на неравенствах логики PostL. Логика PostL обладает хорошими прикладными характеристиками. Исчисление PostL предназначено для работы одновременно с несколькими сложными системами аксиом. Предположим, что некто присваивает разные степени истинности предикатам, взятым из разных наук. Далее, учитывая введённое разделение предикатов на классы, соответствующие различным наукам, этот некто объединяет несколько теорий в рамках одной системы аксиом, и это при том, что некоторые из взятых аксиом могут противоречить друг другу в классическом смысле. Например, возьмём математику и историю. Утверждениям математики придадим максимальное положительное истинностное значение, а утверждениям истории - некоторое неотрицательное значение из множества истинностных значений. Таким образом мы можем различить факты из разных теорий и избавиться от противоречий внутри всей системы аксиом. В последующем изложении мы используем рациональные числа из секторов рациональных чисел в качестве логических значений для представления знания в сложных системах теорий.
В литературе принят подход к многозначной резолюции, который имеет много общего с подходом, представленным здесь, а также в статьях [64, 13] автора данной работы. В [56] было введено понятие отмеченного дизъюнкта. Отмеченный дизъюнкт — это дизъюнкция многозначных литералов, помеченных непустыми множествами истинностных значений. Там же указывается, что отмеченные дизъюнкты не зависят от логики, из которой они произошли. По сути, отмеченные дизъюнкты не содержат ни одной многозначной связки и просто являются характерным языком для обозначения многозначных интерпретаций. Этот подход к многозначной резолюции был разработан в [31], [57] и [85]. Подход на основе линейных неравенств (см. [17]), который мы используем в настоящей главе, близок к подходу отмеченных формул, за исключением той детали, что линейные неравенства естественнее формализуют линейные порядки на множествах истинностных значений.
У логики PostL есть два уровня. На первом уровне рассматрваются формулы многозначной логики. Множество истинностных значений и интерпретация логических связок определяются во внутренней сигнатуре. Предметные переменные — многосортные. На втором уровне имеется единственный предикат сравнения значения внутренних формул с нулём. Внешний язык не содержит функциональных символов. Множество внешних предметных переменных совпадает с множеством внутренних предметных переменных. Итак, формулы этого уровня — это формулы двузначной логики.
Определение 4.1 (Внутренний синтаксис). Внутренний языкЪгп содержит множество Ktnt = {±k/c j к Є [a, b), a, 6, /с, с Є Z+, a b, с 0} логических констант для непустого множества Pmt предикатных символов, помеченных положительными целыми числами а, 6, с, множество Omt предметных переменных, множество Fmt функциональных символов, множество логических связок Cmt — {- , V, Л, — , -н-} и множество кванторов Qmt = {V, 3}. Внутренний терм t состоит из функциональных символов из Ftnt и предметных переменных из ОтЬ. Внутренний атом Pa b c(ti,... ,tn) содержит внутренние термы и предикатные символы из Pmt. Внутренняя предикатная формула либо является внутренним атомом, либо составлена из атомов и кванторов из Qmt и логических связок из Cint.
Будем говорить, что формула А — это формула сорта а, Ь, с, если все её предикатные символы имеют вид с. Формула А построена над множеством сортов S, если сорта всех переменных в А находятся в S.
Определение 4.2 (Внешний синтаксис). Внешний язык Lext содержит множество логических констант Kext = {0,1}, множество логических связок Cext = {-i,V,A,— , - ,? :}, где : — это трёхместная условная логическая связка "если-тс иначе", Qext = {V, 3}, единственный предикатный символ сравнения с нулём и единственный функциональный символ + сложения рациональных чисел — значений внутренних формул. Неравенство PostL — это выражение вида (0 А), где А — внутренняя предикатная формула, или выражение Ai+A2, где Лі и А — предикатные формулы. Внешние предикатные формулы PostL состоят из неравенств PostL со связками из Cext и кванторами из Qext. Для формул вида - (0 А) мы будем использовать сжатую запись (О - А). Можно записывать формулы в общем случае как (0 - А), где - єК }.
Определение секвенции мы уже давали на стр. 59. Это определение сохраняется в исчислении логики PostL с некоторыми уточнениями. Во-первых, принимаются только секвенции с пустым антецедентом. Во-вторых, списки формул интерпретируются как последовательности, т.е., в отличие от множеств, учитывается каждое вхождение формулы в список (чтобы обратить на это внимание, формулы в списках вместо запятых отделяются пробелами).
Идеалы, отношения конгруэнтности и проблема представления
Многозначные логики имеют естественные алгебраические семантики. Такими семантиками могут служить, например, ограниченные решётки или полурешётки с дополнительными операторами, или же только частично упорядоченные полугруппы или моноиды. Существуют связи между структурными правилами логик и свойствами их алгебраических моделей. Наряду с алгебраическими моделями существуют реляционные модели Крипке, которые обычно имеют гораздо более простую структуру, нежели алгебраические модели. Общая идея установления связи между алгебраической и крипкевской семантиками состоит в использовании теорем представления булевых алгебр, дистрибутивных решёток и полурешёток с дополнительными операторами в виде алгебр множеств.
Основываясь на полученных данным способом моделях Крипке, Соф-рони-Стоккерманс в [85] обосновала метод автоматического доказательства теорем по резолюции для конечнозначных логик с алгебрами истинностных значений в виде дистрибутивных решёток с операторами. В последующих работах Софрони-Стоккерманс расширила сферу применения теорем представления на другие типы неклассических логик, см., например, [86].
В этой главе будет рассмотрен перевод в конъюнктивную нормальную форму и процедуры автоматического доказательства теорем в конечно-значных логиках, у которых алгебрами истинностных значений являются дистрибутивные решётки с операторами особого типа. Одним из преимуществ дистрибутивных решёток с «хорошими» операторами является существование для этих решёток удобных теорем представления, таких как теорема Пристли. Изложенный здесь метод перевода формул в КНФ основан на дуалах Пристли — алгебрах, дуальных по Пристли исходным алгебрам истинностных значений.
Напомним некоторые определения главы 2. Пропозициональная матрица A0 = (N, (ов)вє&) пропозиционального языка L0 состоит из непустого множества истинностных значений N и семейства {ое)в @ операций на N таких, что NarW — N для каждой (од)ве&- \N\ обозначает количество элементов в N. Если L = (0, Л, аг) — первопорядковый язык, то первопо-рядковая матрица — это тройка A = (N, (о )$е, (9А)АЄЛ), где (N, {ов)ве&) — пропозициональная матрица для (0,ar), a q\ : V+(N) — N для каждого Л Є Л, где V+(N) — это множество всех непустых подмножеств N. q\ называется функцией распределения квантора Л.
Моделью Крипке логики С называется тройка М = (W, R, V), где W есть непустое множество, именуемое множеством миров, R есть двухместное отношение на W, а V есть функция оценки на W, отображающая множество атомарных формул логики С в множество подмножеств множества W. Структурой Крипке называется пара К = (W, Я), где W и R определены выше. Реляционной структурой называется множество с заданными на нём отношениями. Так называемые естественные теоремы представления (см. [86]), к которым относится и теорема Пристли, мотивированы следующими соображениями. Пусть С — это некоторая логика. Если С полна и непротиворечива относительно класса М матриц, и этот класс матриц может быть представлен как множество подмножеств реляционных структур в классе R, тогда реляционные структуры в R являются возможными кандидатами для определения класса KM,R моделей Крипке для С. В частности, при определённых условиях полнота и непротиворечивость логики С относительно класса Кмд есть прямое следствие полноты и непротиворечивости относительно М.
Пусть М — это класс матриц. В ряде случаев можно показать (см. [86], теоремы 13 и 14), что существует класс R реляционных структур, таких что выполняется следующее условие ( ): (1) Ниже мы приведём основные понятия, необходимые для формулировки базовой теоремы (см. [86], [25]). Непустое подмножество F решётки L называется фильтром, если для любых х,у Є F имеет место х Л у є F, и для любых #, у Є L, если х Є F и х у, тогда у F. Фильтр F, максимальный относительно свойства О . F, называется ультрафильтром. Фильтр F называется главным, если F ф L и для всех х,у L, если х V у Є F, тогда х F или у Є F. Далее, назовём порядковым фильтром множество Fx = {у : у х}, где х, у Є L. Множество А называется замкнутым, если оно содержит все объединения любых своих подмножеств, и открытым — если его дополнение замкнуто. Обозначим операцию замыкания произвольного множества как С. Множество с определённой на нём операцией замыкания называется пространством. Класс В открытых подмножеств пространства X называется базисом X, если каждое открытое подмножество X есть объединение некоторых множеств, принадлежащих В. Класс Во открытых подмножеств пространства X называется подбазисом X, если класс В, состоящий из пустого множества 0, самого пространства X и всех конечных пересечений вида Bi П П В„, где Bi,..., В„ В0, есть базис пространства X. Пусть X и У — пространства. Взаимно однозначное отображение / : X — Y, сохраняющее операцию замыкания, т.е. удовлетворяющее f{C(A)) = С(/(Л)), для каждого множества А X, и f-1(C(B)) = C{f 1{B)), для каждого В С Y, называется гомеоморфизмом X на Y. Определим дуал Пристли для ограниченной дистрибутивной решётки L как частично упорядоченное топологическое пространство D{L) = (FP(L),C,r), где FP(L) — это множество главных фильтров на L, а г — это топология, т.е. система замкнутых подмножеств, порождённая подбазисом, состоящим из множеств вида Ха — {F Є FP(L) : а Є F}, для всех а Є L, а также из их дополнений.
Пусть А — это ограниченная дистрибутивная решётка. Гомоморфизмом (антиморфизмом) на А называется функция к : А — А, сохраняющая (обращающая) порядок. Гемиморфизмом1 относительно дизъюнкции на А называется функция / : Ап — А, принимающая значение 0, если любой её аргумент принимает значение 0, и, если её г-тый аргумент равен а\ V а2 равная дизъюнкции двух функций /, у которых на г-тых аргументных местах находятся аг и а% соответственно. Гемимор-физм относительно конъюнкции определяется двойственным образом: в предыдущем определении 0 заменяется на 1, а дизъюнкция — на конъюнкцию. Гемиантиморфизмом относительно дизъюнкции на А называется функция g : Ап — А, принимающая значение 0, если любой её аргумент Термин «гемиморфизм» был введён Халмошем в [61]. Понятие использовалось для представления оператора необходимости в модальной логике.
