Источник INRIA научно-исследовательский центр
В этой статье мы исследуем теорию вывода многозначных логик с алгебраической точки зрения. Нашей целью является фор- мулировка критерия применимости к произвольной многозначной логике предложенного в [9] метода резолюций на основе теоремы представления Пристли для дистрибутивных решеток с операто- рами. Данный метод резолюций, как и все существующие методы резолюций, симулирует разрешающую процедуру первопорядко- вой логики предикатов, по причине чего любой резолютивный вывод может быть эквивалентным образом представлен, например, в гильбертовском исчислении соответствующей логики. Отличительной особенностью данного метода, благодаря которой он в ряде случаев более эффективен, чем гильбертовский, является использование специальных меток, которые ограничивают область оценки многозначной формулы некоторым подмножеством множества истинностных значений.
Правило бинарной резолюции на основе дуальности Пристли
выглядит следующим образом (ср. [9, следствия 5 и 6]):
Из посылок ({α}:Lt )∨C1 и ({β}:Lf )∨C2 выводится C1∨C2 при усло-
вии, что α,β∈D(A) и α ≤ β,
где запись {α}:Lt (или {α}:Lf ) обозначает, что многозначный
литерал L общезначим (соответственно, опровержим) на множе-
стве истинностных значений α; C1 и C2 суть дизъюнкции литера-
лов с метками указанного вида; D(A) есть множество всех главных
фильтров на алгебре истинностных значений A рассматриваемой логики, упорядоченное по включению. Для краткости изложения мы предполагаем, что L, C1 и C2 уже унифицированы. Заметим, что упомянутое правило резолюции по сути своей остается класси- ческим, изменения касаются только структуры литералов.
109
Основные определения метода резолюций для классической логики предикатов первого порядка остаются неизменными, про- исходит только структурная трансформация многозначных лите- ралов в многосортные классические, поэтому в этой статье не при- водятся подробные определения понятий метода резолюций. Вме- сто этого мы указываем на основополагающую монографию по методу резолюций и автоматическому доказательству теорем в классической первопорядковой логике предикатов [3].
MV-алгебры, исследуемые в этой статье, не определяются.
Определение MV-алгебр см., например, работу [5].
Отметим некоторые работы, близкие по тематике к данной ста- тье. Оригинальные теоремы представления для конечнозначных логик были установлены в [4], где в отличие от [9] и данной работы рассматривались квазимногообразия алгебр истинностных значений, а не многообразия. Также в связи с логиками Лукасе- вича и соответствующей теоремой представления для дистрибу- тивных решеток с оператором резидуации (см. [9]) следует упомя- нуть статью [10], где была доказана полнота бесконечнозначной логики Лукасевича относительно реляционной семантики с тер- нарным отношением достижимости на множестве миров. В свою очередь, в [10] были использованы результаты статьи [1].
В более ранней работе [2] мы уже рассматривали методы резо- люций с отмеченными формулами (т.е. с формулами, имеющими метки) для многозначных логик, однако предложенный нами под- ход был иным, требующим осуществления трудоемких рутинных операций по преобразованию формул к виду, пригодному для под- становки в правило. Поэтому мы считаем, что подход, исследуе- мый в данной статье, более ценен в случае, когда вывод осуществ- ляет человек, а не машина.
Так называемые натуральные теоремы представления (см. [9]), к которым относится и теорема Пристли, мотивированы сле- дующими соображениями. Пусть L – это некоторая логика. Если L полна и непротиворечива относительно класса M матриц, и этот класс матриц может быть представлен как множество подмно- жеств реляционных структур в классе R, тогда реляционные структуры в R являются возможными кандидатами для определе- ния класса KM,R моделей Крипке для L. В частности, при опреде- ленных условиях полнота и непротиворечивость логики L относи- тельно класса KM,R есть прямое следствие полноты и непротиворе- чивости L относительно M.
110
Пусть M – это класс матриц. В ряде случаев можно показать (см. [9, теоремы 13 и 14]), что существует класс R реляционных структур таких, что выполняется следующее условие:
(i) для каждой структуры K∈R верно O(K) = (AK, VK)∈M,
где AK – это алгебра подмножеств множества возможных
миров структуры K, а VK – множество выделенных миров
структуры K;
(ii) для каждой матрицы M = (A, V)∈M, если O(D(M)) =
(AD(M), VD(M)), то существует инъективный гомоморфизм i: A→AD(M) такой, что i−1(VD(M))⊆V.
Ниже мы приведем основные понятия, необходимые для фор-
мулировки базовой теоремы (см. [9]).
Непустое подмножество F решетки L называется фильтром, если для любых x,y∈F x∧y∈F, и для любых x,y∈L, если x∈F и x≤y, тогда y∈F. Фильтр F, максимальный относительно свойства 0∉F,
называется ультрафильтром. Фильтр F называется главным, если F≠L и для всех x,y∈L, если x∨y∈F, тогда x∈F или y∈F. Далее, назовем порядковым фильтром множество Fx={y: y≥x}, где x,y∈L.
Обозначим операцию замыкания произвольного множества как
C. Множество A называется замкнутым, если оно совпадает со своим замыканием C(A), и открытым – если его дополнение замкнуто.
Класс B открытых подмножеств пространства X называется базисом X, если каждое открытое подмножество X есть объедине- ние некоторых множеств, принадлежащих B. Класс B0 открытых подмножеств пространства X называется подбазисом X, если класс
B, состоящий из пустого множества ∅, самого пространства X и всех конечных пересечений вида B1∩…∩Bn, где B1,…,Bn∈B0, есть
базис пространства X.
Пусть X и Y – пространства. Взаимно однозначное отображе- ние f: X→Y, сохраняющее операцию замыкания, т.е. удовлетво- ряющее f(C(A)) = C(f(A)), для каждого множества A⊆X, и f−1(C(B)) = C(f−1(B)), для каждого B⊆Y, называется гомеоморфизмом
X на Y.
Определим дуал Пристли для ограниченной дистрибутивной решетки L как частично упорядоченное топологическое простран-
ство D(L)=(FP(L), ⊆, τ), где FP(L) – это множество главных фильтров на L, а τ – это топология, т.е. система замкнутых под-
111
множеств, порожденная подбазисом, состоящим из множеств вида
Xa={F∈FP(L): a∈F}, для всех a∈L, а также из их дополнений.
Пусть A – это ограниченная дистрибутивная решетка. Гомо-
морфизмом (антиморфизмом) на A называется функция k:A→A,
сохраняющая (обращающая) порядок. Гемиморфизмом относи-
тельно дизъюнкции на A называется функция f: An → A, прини-
мающая значение 0, если любой ее аргумент принимает значение
0, и, если ее i-тый аргумент равен a1∨a2, равная дизъюнкции двух
функций f, у которых на i-тых аргументных местах находятся a1 и
a2 соответственно. Гемиморфизм относительно конъюнкции опре-
деляется двойственным образом: в предыдущем определении 0
заменяется на 1, а дизъюнкция – на конъюнкцию. Гемиантимор-
физмом относительно дизъюнкции на A называется функция g: An
→ A, принимающая значение 0, если любой ее аргумент прини-
мает значение 1, и, если ее i-тый аргумент равен a1∧a2, равная
дизъюнкции двух функций g, у которых на i-тых аргументных
местах находятся a1 и a2 соответственно. Гемиантиморфизм отно-
сительно конъюнкции также определяется двойственным образом.
Обозначим как Σ класс всех гомоморфизмов, антиморфизмов,
геми(анти)морфизмов относительно дизъюнкции и геми(анти)-
морфизмов относительно конъюнкции на произвольной ограни-
ченной дистрибутивной решетке A.
Следующая теорема (см. [9, теорема 14]) устанавливает экви- валентную форму представления для ограниченных дистрибутив- ных решеток с операторами.
ченная дистрибутивная решетка L с операторами из множества Σ изоморфна решетке O(D(L)) открыто-замкнутых порядковых фильтров на D(L). Изоморфизм f: L→O(D(L)) задается как f(x)={F: F∈FP(L) и x∈F}.
Для анализа свойств операторов дистрибутивных решеток в [8] применялся аппарат канонических расширений, позаимствован- ный в свою очередь из модальных логик. Для формулировки кри- терия применимости метода резолюций на основе дуальности Пристли нам необходимо дать некоторые определения и привести основные результаты, касающиеся многозначных логик и канони- ческих расширений (см. [8], [9], [6]).
В [8] каноническим расширением дистрибутивной решетки A с операторами из Σ названа решетка O(D(A)). Имея это в виду,
допустим, что V – это многообразие (т.е. класс алгебр, удовлетво-
112
ряющих одной и той же системе тождеств) ограниченных дистри-
бутивных решеток с операторами в классе Σ. Тогда многообразие
V замкнуто относительно канонических расширений, если оно имеет свойство O(D(A))∈V для любой решетки A∈V. (В [6]
используется более общее понятие канонического расширения.)
Пусть J – это множество индексов, а U⊆P(J) – ультрафильтр,
где P(J) обозначает множество всех подмножеств J. Пусть {Xj: j∈J}
– это семейство реляционных структур одного и того же типа R,
где Xj=(Xj, {Rj}R∈R) для каждого j. Зададим отношение эквива-
лентности ≈U, определенное для всех x,y∈Πi∈J Xj как x≈Uy, е.т.е.
{j∈J: xj=yj}∈U.
Для каждого семейства реляционных пространств {Xj: j∈J}
(где Xj = (Xj,{Rj}R∈R) для каждого j) и для каждого ультрафильтра
U⊆P(J) факторструктура ((Πi∈J Xj)/ ≈U, {RU}R∈R)
называется ультрапроизведением семейства {Xj: j∈J} относи-
тельно U, где RU обозначает факторотношение по ≈U, т.е.
RU(|x1|U,…, |xn|U), е.т.е. {j∈J: Rj(x1j,…,xnj)}∈U.
Теорема 2 ([8, Следствие 22]). Пусть K – это класс упорядочен- ных Σ-структур, замкнутых относительно ультрапроизведений, и пусть K+ = {O(X): X∈K}. Тогда замыкание K+ относительно
гомоморфных образов, подалгебр и прямых произведений, т.е. многообразие, порожденное K+, замкнуто относительно канони- ческих расширений.
Следующие теоремы были доказаны в более общей форме в [9] как теоремы 9 и 11 соответственно. В нашей более узкой формули- ровке они устанавливают тот факт, что, благодаря изоморфизму по теореме представления для ограниченных дистрибутивных реше- ток с операторами, любая алгебра A истинностных значений одной из соответствующих многозначных логик может быть запечатлена в более экономной форме как дуал Пристли D(A). Этот факт существенен для эффективного метода резолюций.
Теорема 3. Пусть A – ограниченная дистрибутивная решетка. Тогда отображения и отношения на D(A) могут быть опреде- лены каноническим образом.
Теорема 4. Пусть X = D(A) – конечное частично упорядоченное множество. Тогда операторы на O(X) могут быть определены каноническим образом.
Пусть Z+ и Z− – это соответственно множества всех неотрица-
тельных и неположительных целых чисел. Алгебра Чена C (см. [5,
стр. 474]) определяется как (C, ⊕, ¬, 0), где C – это решетка вида C
= {(0, a): a∈Z+} ∪ {(1, b): b∈Z−}.
113
Нулем данной решетки является элемент (0, 0), а единицей – (0, 1). На решетке задается лексикографический порядок. Опера- ция сложения определяется как
⎧ (0,a+b), если i+j=0 (i,a)⊕(j,b) = ⎨ (1,0∧(a+b)), если i + j = 1
⎩ (1,0), если i+j=2,
а операция отрицания определяется как ¬(i,a) = (i+21, −a), где +2
обозначает операцию сложения по модулю 2.
Пусть f – алгебраическая операция. Определим fσ как нижний
предел sup inf f, а fπ – как верхний предел inf sup f (более точное
определение см. [6]). Тогда каноническим расширением алгебры A
будет алгебра, полученная из A в результате применения σ или π
ко всем ее операциям и вложения A в полную решетку.
Лемма 1 ([6]). Пусть C=(C, ⊕, ¬, 0) – это алгебра Чена и пусть
f=⊕. Тогда fσ≠fπ.
В силу лемм 2 и 3, аксиома MV-алгебры (MV6) ¬(¬x⊕y)⊕y =
¬(¬y⊕x)⊕x не является канонической, поэтому аксиома бесконеч-
нозначной логики Лукасевича ((P→Q)→Q) → ((Q→P)→P) невы-
водима методом резолюции на основе теоремы представления
Пристли (см. правило во введении).
Лемма 2 ([6]). Тождество (MV6) не выполняется в
Cσ=(Cσ,⊕σ,¬σ,0).
Лемма 3 ([6]). Тождество (MV6) не выполняется в
Cπ=(Cπ,⊕π,¬π,0).
Доказательство. (⇒) Так как любое многообразие MV-алгебр,
порожденное бесконечным классом MV-алгебр, содержит алгебру
Чена C (см. [5, стр. 474]), то в силу лемм 2 и 3 не существует бес- конечно порожденных канонических многообразий MV-алгебр. Этот факт по контрапозиции доказывает данную часть теоремы.
(⇐) В силу теорем 3 и 4 мы можем задать операторы на O(D(A)) каноническим образом. По определению отображений σ и π операторы на O(D(A)) будут сохранять аксиомы MV-алгебры.
Это доказывает корректность правила резолюции.
В следующей теореме дано решение проблемы, поставленной в
[7], т.е. основной проблемы настоящей статьи.
Метод резолюций на основе теоремы представления Пристли
114
корректен относительно произвольной многозначной логики, если и только если многообразие V, порожденное ее алгеброй A истинностных значений, замкнуто относительно канонических
расширений, т.е. для всех A′∈V верно, что O(D(A′))∈V.
Доказательство. (⇒) Вследствие теоремы 2, многообразие, поро-
ждённое алгеброй классов эквивалентности произвольной много-
значной логики, замкнуто относительно канонических расшире-
ний, если эта алгебра находится в классе ограниченных дистрибу-
тивных решёток с операторами в классе Σ.
(⇐) Предположим теперь, что многообразие V, порождённое
алгеброй A, незамкнуто относительно канонических расширений,
т.е. существует A′∈V такая, что O(D(A′))∉V. Следовательно, в V
существует алгебра, каноническое расширение которой не удовле-
творяет тождествам алгебры A. Отсюда, алгебра A порождает мно- гообразие V такое, что метод резолюций некорректен относительно логики, для которой данное многообразие является характеристическим.
Отметим, что, согласно данной теореме, алгебра истинностных значений рассматриваемой логики не обязана быть конечной. Сле- довательно, метод резолюций может быть применим и к некото- рым бесконечнозначным логикам.
В теореме 6 нами был сформулирован критерий применимости метода резолюций на основе теоремы представления Пристли к многозначным логикам с произвольными алгебрами истинностных значений.
В [9] было показано, что существует общая схема теорем пред-
ставления как для решеток с операторми из класса Σ, так и для по-
лурешеток с операторами из этого класса. По этой схеме, в частно-
сти, можно получить теорему представления для дистрибутивных решеток с оператором резидуации ([9, теорема 17]), к которым принадлежат и MV-алгебры – семантические аналоги логики Лукасевича. Но так как представление решеток с резидуацией осуществляется там посредством топологических дуалов, имею- щих принципиально иную структуру (в частности, с тернарными отношениями на топологических пространствах), чем дуалы При- стли, то использованное нами в статье определение канонических расширений не может быть применено для создания метода резо- люций в случае логик, основанных на дистрибутивных решетках с оператором резидуации. В силу этого представляет теоретический интерес понятие канонического расширения для таких логик. В
115
случае нахождения подходящей формулировки, можно было бы эффективно решить вопрос о замкнутости соответствующих мно- гообразий относительно представлений, и тогда появилось бы основание для построения метода резолюций для многозначных логик (например, логик Геделя и логик Лукасевича) и релевантных логик по аналогии с методом резолюций для многозначных логик на основе теоремы представления Пристли.
1. Карпенко А.С. Фактор-семантика для бесконечнозначной логики
Лукасевича // Неклассические логики. М.: ИФАН, 1985. С. 20-26,.
2. Комендантский В.Е. Метод резолюций в смешанной логике Поста // Труды XVI научно-исследовательского семинара логического центра ИФРАН. М.: ИФРАН, 2002. С. 64-74.
3. Чень Ч., Ли Р. Математическая логика и автоматическое доказатель-
ство теорем. М.: Мир, 1983.
4. Anshakov O., Rychkov S. On Finite-Valued Propositional Logical Calculi // Notre Dame Journal of Formal Logic. 1994. Vol. 36, № 4. P. 606-629.
5. Chang C.C. Algebraic analysis of many valued logics // Trans. Amer. Math.
Soc. 1958. Vol. 88. P. 467-490.
6. Gehrke M., Priestley H.A. Non-canonicity of MV-algebras // Houston
Jounal of Mathematics, 2002.
7. Komendantsky V. On automated theorem proving by means of represen- tation theory in Lukasiewicz logics // Smirnov’s Readings. 4 international conference. Moscow: IPhRAS, 2003. P. 78-79.
8. Sofronie-Stokkermans V. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I. // Studia Logica. 2000. Vol 64, № 1. P. 151-172.
9. Sofronie-Stokkermans V. Representation Theorems and the Semantics of Non-classical Logics, and Applications to Automated Theorem Proving // Beyond Two: Theory and Applications of Multiple Valued Logic. Springer,
2003. P. 59-100.
10.Vasyukov V.L. The Completeness of the Factor Semantics for
Lukasiewicz's Infinite-valued Logics // Studia Logica. 1993. Vol. 52. P.
143-167.
116