Континуальность решетки расширений модальной логики двух отношений эквивалентности

Краткие сообщения

УДК 510.6

КОНТИНУАЛЬНОСТЬ РЕШЕТКИ РАСШИРЕНИЙ МОДАЛЬНОЙ ЛОГИКИ ДВУХ ОТНОШЕНИЙ ЭКВИВАЛЕНТНОСТИ

М. М. Измайлов1

В статье строится континуум различных логик над S5  S5, что доказывает тот факт, что мощность решетки расширений логики двух отношений эквивалентности Ext(S5  S5) является континуумом.

Ключевые слова: модальная логика, соединение логик, расширения логик, логика отношения эквивалентности.

A continuum of different modal logics over S5  S5 is constructed in the paper, which proves that the capacity of the lattice of all normal extensions of the logic of two equivalence relations Ext(S5  S5) is a continuum.

Key words: modal logic, fusion of logics, extensions of logics, logic of equivalence relation.

Введение. В работе Волтера [1] доказывается вложимость расширений логики T в расширения логики S5  L, где L — логика двухэлементной рефлексивной цепи. Отсюда следует континуальность решетки расширений Ext(S5  L). Для произведения S5 х S5 также известно, что решетка расширений этой логики состоит из счетного числа логик, которые к тому же конечно-аксиоматизируемы [2]. Для логики S5  S5 вопрос о мощности решетки ее расширений оставался открытым. В данной работе мы докажем, что решетка расширений модальной логики S5  S5 имеет мощность континуума.

Основные понятия. Напомним, что набор формул L называется логикой, если он содержит все тавтологии и замкнут относительно правил вывода modus ponens и подстановки. Модальная логика L называется нормальной, если она содержит аксиому

AK = D(p ^ q) ^ (Dp ^ Dq) и замкнута относительно правила D-введения:

если ф £ L, то Dф £ L.

Шкалой Крипке называется набор (W, R\ ,...,Rn), где W — непустое множество миров, Ri С W х W. Оценка V на шкале Крипке (W, R\,...,Rn) — это функция, которая каждой переменной ставит в соответствие подмножество W. Модель Крипке — это шкала Крипке с оценкой на ней. Говорят, что переменная p истинна в мире x модели M: M,x = p, если x £ V(p). Истинность формул определяется по индукции следующим образом:

M,x ¥ ±,

M, x = ф V ф & M, x = ф или M,x = ф,

M, x = -ф & M, x ¥ ф, M, x = Diф &Уу £ W(xRiy ^ M, x = ф).

Говорят, что формула ф общезначима в мире x шкалы Крипке F, если для любой оценки V на этой шкале (F, V),x = ф. Формула общезначима в шкале, если она общезначима в каждой точке этой шкалы.

Минимальная модальная логика, содержащая аксиому AK, обозначается K. Под K ф Г, где Г — множество формул, понимается наименьшая нормальная модальная логика, содеражая K и Г. Логика S5 определяется так:

S5 = K ф {Dp ^ p, Dp ^ DDp,p ^ D^p}.

Общезначимость формул Dp ^ p, Dp ^ DDp,p ^ D^p в шкале Крипке F = (W, R) равносильна соответственно рефлексивности, тразитивности и симметричности отношения R. Таким образом, S5 —

1 Измайлов Максим Марселевич — студ. каф. математической логики и теории алгоритмов мех.-мат. ф-та МГУ, e-mail: izmaxim@gmail.com.

логика шкал, где R — отношение эквивалентности. Кластером называется класс эквивалентности по отношению R.

Напомним, что соединение (fusion) Л1  Л2 одномодальных нормальных логик Л1, Л2 определяется как наименьшая двумодальная логика, содержащая аксиомы Л1 для первой модальности и аксиомы Л2 для второй.

Произведение логик Л1 х Л2 есть логика множества шкал Крипке {F1 х F2IF1 = Л1,^2 = Л2}, где Fi х F2 = (W1 х W2, R1 ,R'2), причем (Ж1 ,X2)R'1 (У1,У2) & X1 Ry и X2 = У2, (X1,X2)R2 (V1,V2) & X2R2V2 и X1 = У1.

Логика Л2 называется расширением логики Л1, если Л1 С Л2. Решеткой расширений модальной логики Л1 называется множество всех модальных логик, содержащих ее: Ext^1) = {Л2|Л1 С Л2}.

Расширения логики Л действительно образуют полную решетку:

еП =

inf{Лг|г е i} = р|{Лг|г е i}.

Пересечение логик, очевидно, тоже будет логикой, причем пересечение логик, содержащих Л, также содержит Л. Наибольшим элементом в этой решетке является противоречивая логика (которая содержит все формулы). Напомним, что для того, чтобы утверждать, что Ех1(Л) — полная решетка, этих свойств достаточно, так как

8ир{Л;\г Е I} = М{Л|УгЛ^ С Л}.

Континуальность решетки расширений. Теорема 1. Ех^£5  £5) имеет мощность континуума.

Доказательство. Для доказательства будет достаточно выписать последовательность формул {ф1, г = 1, 2,...}, таких, что для каждого I С N

£5  £5 ф {ф^г Е I} К ф^, если 3 Е I.

Тогда расширения Л/ = £5£5ф{ф^1 Е I} будут такие, что Л/ = ЛJ при I = .]. Следовательно, мощность множества таких логик равна мощности множества подмножеств натурального ряда, т.е. континууму. Для построения фп потребуются формулы

аН;п = Ир: V П(р1 ^ Р2) V ... V П(р1 ЛЛ ... Л Рп ^ Рп+1), п ^ 0.

Лемма 1. Формула аН;п общезначима в точке х шкалы Крипке Е тогда и только тогда, когда из х достижимо не более чем п различных точек.

Доказательство. Пусть из точки х достижима п +1 различная точка У1,У2,...,уп+1. Построим модель Крипке М = (Е, V), такую, что М,х аН;п, т.е. М,х \ —аН;п. Запишем отрицание аН;п в явном виде:

-аН;п = 0-Р1 Л 0(Р1 Л -Р2) Л ... Л ♦(р: Л Р2 Л рз ... Л Рп Л -Рп+1), п ^ 0.

Чтобы построить М, нам нужно только построить оценку V, такую, что М,х \ — аНп. Оценка должна быть следующей: V(рп) = {у^\к > п}. Тогда М,уп \ р1 Л ... Л рп-1 Л —рп, и поэтому М,х \ —аН;п.

Пусть теперь М, х \ —аН;п. Тогда по определению ♦ найдутся у1,..., уп, такие, что хКу1,..., хКуп+1 и уг \ Р1 Л ... Л р-1 Л —Рг. Если г < 3, то уг \ —Рг, а уз \ Рг, значит, уг = у] при г = 3.  Теперь можно написать формулы фп,п ^ 1:

фп = ((0102)п-101(а Л 02(—а Л Ь) Л 02(—а Л —Ь))) акп+ь Здесь формула аН;п+1 записана в языке с !.

Лемма 2. Пусть Е = (Ш, Я1,Я2) \ £5  £5. В точке х общезначима формула фп тогда и только тогда, когда в х верно следующее условие: если из х по отношению

Кг о К2 о Кг о    о Д2 о

2га-1

достигается Я2-кластер из более чем двух точек, то ^(х) ^ п +1.

Доказательство. Пусть Е,х \ фп, и {«, Ь, и} — ^-кластер, который достигается из х по Я* (или его часть). Допустим, Я1 (х) > п +1. Тогда существует оценка V, такая, что (Е, V),х аН;п+1. Множество переменных, входящих в формулу ф, обозначим Уаг(ф). Так как а,Ь Е Уаг(аНп+1), то для а и Ь можно

задать свою оценку, сохранив при этом свойство (Г, V),х ¥ аНп+1. Зададим оценку а,Ь на точках в,Ь,п таким образом, чтобы посылка формулы фп была верна в х. Это очевидно можно сделать. Пусть в — та точка из кластера, которая достигается из х по Я*. Тогда можно положить V(а) = {в}, V(Ь) = {в^}. Обратно, пусть Г,х ¥ фп. Для какой-то оценки V имеем (Г, V),х \ —фп. Значит,

и

),х \ -а^п+ь

Согласно (1), из х по отношению Я* достигается Я2-кластер из более чем двух точек (потому что никакие две из формул а, —аЛЬ, —аЛ—Ь не могут быть истинны одновременно в одной точке). Из (2) по предыдущей лемме следует, что из х достигается более п + 1 точки по отношению Яь I

Построим шкалы Крипке Г \ 55  £5, такие, что Г^ ¥ ф^ и Г \ фj, если ] = г. Тогда мы получим Л/ = ЛJ при I = .]. Шкала Г показана на рисунке.

/+2 точки

Большой R1 -кластер справа из i + 2 точек назовем C. В любой точке x из C достигается ^-кластер размера 3 через композицию Ri о R2 о ... о Ri из 2n — 1 отношений. Также в x отрицается формула alti+i, так как кластер состоит из i + 2 элементов. Значит, в x отрицается формула фг.

Для j > i имеем Fi \ фу, так как Fi \ altj+i при j > i. Если j < i, то посылка формулы фj не будет верна в C. Значит, в C верна фу. В остальных точках Fi она тоже верна, потому что в них верна формула altj+i для любых j ^ 1. На этом доказательство завершается.

Упомянутое в лемме 2 свойство записывается на языке первого порядка. Модальная логика называется Д-элементарной, если класс ее моделей есть класс моделей теории первого порядка. Модальная логика называется элементарной, если класс ее моделей описывается предложением первого порядка. Логики Л/ Д-элементарны. Поэтому имеет место

Следствие. Среди расширений S5  S5 имеется континуум Д-элементарных логик.

Логики S5  altn обозначаются S5n; такими логиками исчерпываются все расширения S5. На самом деле имеет место более сильный результат.

Теорема 2. Ext(S5  S5з) имеет мощность континуума.

В доказательстве теоремы 1 в шкалах Fi нет кластеров по отношению R2 размера больше 3 точек. Поэтому эти шкалы удовлетворяют более сильному условию: Fi \ S5  (S5  alts). Из этого и следует утверждение данной теоремы.

Заключение. Мы показали, что, даже когда одномодальные логики Л1 и Л2 просты и решетки их расширений описываются очень просто (одна из них может быть даже конечна), решетка расширений соединения этих логик может содержать довольно много логик. Ext(S5) состоит из счетного набора логик S5n = S5  altn, расширения S5з — это просто две логики S52 и S5i, а их соединение содержит континуум логик.

Работа над статьей поддерживалась грантом Президента РФ НШ-845.2008.1.

СПИСОК ЛИТЕРАТУРЫ

1. Wolter F. What is the upper part of the lattice of bimodal logics? // Stud. log. 1994. 53, N 2. 235-242.

2. Bezhanishvili N, Marx M. All proper normal extensions of S5-square have polynomial size model property // Stud. log. 2004. 78, N 3. 443-457.

Поступила в редакцию 05.04.2010