Стройный порядок на строго позитивных формулах

Интерес к строго позитивным фрагментам модальных логик возник независимо в трёх различных областях: в универсальной алгебре, в изучении дескрипционных логик и в логике доказуемости.

С точки зрения универсальной алгебры, импликации между строго позитивными формулами соответствуют тождествам в языке нижних полурешеток с несколькими монотонными операторами. Строго позитивные логики при этом соответствуют многообразиям таких алгебр. В частности, в работе Джексона. [12] рассмотрены полурешетки с операторами замыкания. В работе [13] подробно рассматриваются вопросы полноты по Крипке и разрешимости строго позитивных логик.

Дескрипционные логики используются в базах данных, снабженных некоторой способностью делать логические выводы на. основе имеющихся данных (базах онтологий). Так, в базе медицинской терминологии SNOMED СТ применяется строго позитивная логика ££. описанная в работах [14-16], вместе с эффективным разрешающим алгоритмом.

В последнем случае для нескольких логик доказуемости оказалось, что их строго позитивные фрагменты просты и полезны для анализа. Для примера, полимодальная логика. GLP не полна по Крипке [7] и PSPACE-полна [8], в то время как её строго позитивный фрагмент RC одновременно полон по Крипке и полиномиально разрешим [5]. Далее, в работах [9-11] арифметические операторы над теориями рассматриваются как модальности, чтобы на. языке логики описать свойства, этих операторов.

В данной работе мы изучаем отношение следования на строго позитивных формулах как отношение порядка. Теория стройных предпорядков (известных в англоязычной литературе как well-quasi orders) интересна с точки зрения теории множеств и комбинаторики, посколвку многие естественные структуры, такие как порядок на строках и порядок на деревнях [1, 2], оказываются стройными предпорядками. Одна из таких структур, как показано в статье [21], — стройный предпорядок (точнее, better-quasi order, [20]) на линейных порядках. В то же время с помощью стройных предпорядков можно доказывать термини-руемость систем переписывания термов (например, как в статье [17]).

Известны и применения стройных предпорядков в логике — например, финитная форма теоремы Крускала даёт примеры комбинаторных утверждений, не доказуемых в сильных арифметических теориях [18]. Более подробно логический анализ теоремы Крускала, вместе с её финитной формой и выводом ординального типа стройного предпорядка на деревьях, дан в статье [23]. В статье [22] обсуждается соответствие между другим независимым от арифметики Пеано комбинаторным утверждением — принципом Червя — и известным стройным предпорядком на строках из натуральных чисел и на замкнутых модальных формулах полимодальной логики доказуемости. Рассматриваемый в этой статье стройный порядок имеет природу, близкую к изучаемому в настоящей работе.

Современные результаты о стройных предпорядках собраны в книге [24], в частности, в статье [19] рассматриваются различные ординальные характеристики стройных предпорядков, включая ординальный тип.

Работа организована следующим образом. В разделе 2 формулируются необходимые понятия и известные результаты, касающиеся строго позитивного фрагмента логики К 4 и стройных предпорядков. В разделе 3 доказывается, что отношение следования на строго позитивных формулах является стройным предпорядком; далее показано, что этот предпорядок можно определить рекурсивно, и с помощью этого найдены верхняя и нижняя оценки его ординального типа.

2.    Основные понятия

Формулы пропозициональной модальной логики строятся из переменных Var = {po,pi,... } л константы Т с помощью логических связок Л.— н модальности О. Связки V, ^ и □ = —О— мы рассматриваем как стандартные сокращения. Строго позитивные формулы — это формулы, построенные из переменных и константы Т с использованием только связок Ли О. Секвенцией мы называем формулу вида А ^ В, где А и В — строго позитивные формулы.

Мы используем общепринятую семантику Крипке. Шкалой Крипке называется пара ( W, R), где W — непустое множество, a R — бинарное отношение на W. Моделью Крипке называется тройка М = (W, R, и), где (W, R) — шкала Крипке, а и, или оценка, — произвольное отображение v: Var ^ 2^W.

Отношение истинности модальной формулы р в точке ж модели Крипке М определяется индуктивно по построению формулы р:

о М, ж |= Т : М, ж = p О ж G v(p).

о М, ж |= —р О М, ж = р, о М, ж |= р1 Лр2 О М,ж |= р1 Л М,ж |= р2.

о М, ж |= Ор оЗу G W(жRу Л М,у = р).

Будем говорить, что формула истинна в модели, если она истинна в каждой точке модели, и истинна в шкале, если она истинна в модели для любой оценки на этой шкале. Логикой класса шкал С называется множество всех модальных формул, истинных в любой шкале из С.

Для модели Крипке будем использовать следующую терминологию:

о если жRy, то у — потомок жиж — предок у, о потомок у вершины ж называется блнлсайшим, если Vz G W —(жRz Л zRyУ, о корнем модели Крипке М = (W, R, в) называется такая вершина г, что Vy G W г = у V rRy :

о модель М линейна, если она антисимметрична и притом

Vж, у, z G W (жRy Л жRz) — (у = z V yRz V zRy).

о модель М является деревом (или древовидной), если она антисимметрична, транзитивна, имеет корень и для любой вершины ж G W множество {у | yRж} линейно;

о если модель М — деі>ево н ж — один из ближайших потомков её корня г. то множество {ж} U {у | жRy} называется максималъпим поддеревом модели М.

Пусть М1 = ( W i ,R i ,b i ) 11 М2 = (W2, R2,B2) — модели Крипке. Функция ф: М1 — М2 называется гомоморфизмом, если:

• 1)    Vж,y G W1 жR1 у — ф(ж^ф(у);

• 2)    Vж G W1,p G Var ж G в1(р) — ф(ж) G в₂(р).

Пусть Мі , М2 — древовидные монели Крипке. Инъективная функция ф : Мі — М2 называется гомеоморфным вложением, если:

• 1)    ф — гомоморфизм:

• 2)    если wi,W2 — два. различных б.тижайншх потомка, вершины в G Мі. то вершина, ф(в) лежит на пути между ф (wi) и ф (W2).

По определению, логика К есть логика класса всех шкал Крипке, логика К 4 есть логика класса всех шкал, в которых отношение R транзитивно.

Исчисление К + задается следующими аксиомами и правилами вывода:

1) А — Л, Л — Т,

А — В, В — С

А — С '

л л          а — В,А — С

^{А ЛВ — А}, ^{А ЛВ — В}, а — в ЛС

А — В

о) О А — О В'

Строго позитивной логикой мы называем набор секвенций, замкнутый относительно К +. Это соответствует семантике нижних полурешёток с монотонной операцией в том смысле, что теоремы К + (и только они) являются секвенциями, истинными во всех таких полурешётках. Исчисление К 4+ есть К + вместе с аксиомой ООА — ОА. Из результатов [6] следует, что исчисление К 4+ порождает в точности строго позитивный фрагмент логики К 4. II то же для К + и К. Строго позитивным фрагментом модальной логики L мы называем множество всех секвенций, входящих в L.

Следуя работе [5], каждой строго позитивной формуле А сопоставим транзитивную древовидную модель Крипке Т [А], называемую каноническим деревом формулы А.

Если А — переменная, то Т [А] — одноточечная модель с пустым отношением R. и А — единственная истинная переменная в этой точке.

Если А = Т, то Т [А] — одноточечная модель с пустым R, в которой все переменные ложны.

Если А = В Л С, то Т [И] образуется из Т [В] и Т[С ] соединением их корней в одну вершину. В новом корне истинны те и толвко те переменные, которые истинны хотя бы в одном из корней деревьев Т [В] и Т[С ].

Если А = ОВ, то Т [А] образуется из Т [В] добавлением нового корня, в котором все переменные ложны и из которого все вершины Т [В] достижимы по R.

Корень канонического дерева Т [А] будем об означать т(А).

Следующие лемма и теорема доказаны в [5, леммы 5.3-5.6].

Лемма 1. Пусть М = (W, R, v) — транзитивна я модель Крипке, А — строго позитивная формула. Тогда М,ж |= А тогда и только тогда, когда существует гомоморфизм ф: Т [А] ^ М. приз,см ф(т(А)) = ж.

Теорема 1. Пусть А, В — произвольные строго позитивные формулы. Тогда следующие утверзюдения эквивалентны:

(til К 4⁺ РА -В.

HJ Т [А]д(А) \=В:

• (т) существует гомоморфизм ф: Т[В] ^ Т[А], причем ф(г(В)) = т(А).

3. Стройный предпорядок на множестве строго позитивных формул

Пара (A, А), г де А — бинарное отношение на множестве A, называется предпорядком, если отношение А рефлексивно и транзитивно. Аналогично, частичным порядком (или частично упорядоченным множеством) называется рефлексивное, транзитивное и антисимметричное отношение; рассмотрев фактормножество по отношению эквивалентности, мы можем получить частичный порядок из любого предпорядка.

Предпорядок (A, А) называется стройным, если для любой бесконечной последовательности ai,a2,... ,а_п,... элементов из A существует пара индексов г < j такая, что Qi А Oj. Мы будем использовать эквивалентное определение, а именно — любая бесконечная последовательность содержит не только пару элементов Oi А Oj, но и бесконечную неубывающую подпоследовательность. Стройным порядком мы будем называть стройный частичный порядок; ясно, что если (A, А) — стройный предпорядок, то (A/^, А) (фактормножество по отношению эквивалентности А) — стройный порядок.

Если (X, А) — стройный порядок, мы можем рассмотреть всевозможные его расширения до линейного порядка и найти точную верхнюю грань соответствующих ординалов; будем называть эту точную верхнюю грань ординальным типом и обозначать o(X, А). В статье [4] показано, что такая точная верхняя грань является максимумом, то есть на некотором линейном расширении порядка А в точности достигается.

Ординальным типом стройного предпорядка (X, А) называется ординальный тип соответствующего стройного порядка (X/^, А).

Предложение 1. Пусть А, В — строго позитивные формулы. Гомоморфизм ф: Т [В] ^ Т [А] существует тогда, п только тогда., когда. К 4 РА ^ В V ОВ.

Доказательство. Заметим, что К 4 РА ^ В VОВ тогда и только тогда, когда К 4 РА ^ В или К 4 РА ^ ОВ. Первое, согласно теореме 1, равносильно существованию гомоморфизма ф: Т [В] ^ Т [А] такого, что ф(г(В )) = т(А); второе равносильно существованию гомоморфизма ф: Т [ОВ] ^ Т [А] такого, что ф (т(ОВ)) = т(А). В последнем случае мы можем ограничить этот гомоморфизм на Т [В] и получить гомоморфизм между Т [В] и Т [А] (причём ф (т(В)) = г(А)), что и требовалось. Обратно, если ф : Т [В] ^ Т [А] — гомоморфизм и ф (т(В)) = т(А). то ф‘ = ф U {(т(ОВ ),т(А))} — гомоморфизм между Т [ОВ] іі Т [А].

Предложение 2. Пусть А,В — строго позитивные формулы такие, что в корнях Т [А] и Т [В] истинны одни и те же переменные. Тогда из К 4 РА ^ О В следует К 4 РА ^ В.

Доказательство. Согласно теореме 1, существует гомоморфизм f : Т [ОВ] ^ Т [А], причем f (т(ОВ)) = т(А). Обозначим Т ' = Т [В] \ {т(В )}. Замет им, что f ' = f Д ‘ U {(т(В), т(А))} — гомоморфизм, поскольку для любой вершины ж € Т [В] вер но f (ж) = т(А); при этом f '(т(В)) = т(А) по построению. Следовательно, К 4 Н А ^ В, что и требовалось.

Обозначим Fm — множество строго позитивных формул на конечном множестве переменных Рі,Р*, ... ,р_п- Определим на этом множестве два отношения: А Ғ В, если К 4 Н В ^ А, и А Ғ В, если К 4 Н В ^ А V О А.

Теорема 2. Отношение Ғ является стройним предпорядком.

Доказательство. Заметим, что А Ғ В равносильно существованию гомоморфизма f : Т [А] ^ Т [В] такого, что f (т(А)) = т(В)' а А Ғ В — существованию гомоморфизма f : Т [А] ^ Т [В]. Определим ещё одно отношение: А F" В, если существует гомеоморфное вложение f : Т [А] ^ Т [В]. Ясно, что F"cF'. По теореме Крускала, Ғ" является стройным предпорядком, а значит, Ғ' — тоже стройный предпорядок. По определению стройного предпорядка, из любой бесконечной последовательности {Аг} можно выделить бесконечную подпоследовательность {А,^} такую, что А,(_г) Ғ' А,щ₊₁) (для любого натурального г), то есть К 4 Н А,щ₊₁) ^ А,(г) V ОА,^. Заметим, что мы можем также вывести К 4 Н А ₅ ( _{і +}^) ^ А ₃(і) V О Ақ і) для любого натурального к. Множество переменных {Р1,... ,Рп} имеет конечное число подмножеств, поэтому найдётся его подмножество, которое встречается в качестве Уат(т(А₅(^))) бесконечное множество раз. Удалим все остальные элементы подпоследовательности, получим новую бесконечную подпоследовательность {А,‘(г)}.Согласно предложению 1, К 4 Н А₅дг₊1) ^ А,‘(г), то есть подпоследовательность {А,‘(^)} не убывает в отношении Ғ. Таким образом, Ғ — стройный предпорядок, что и требовалось.

Будем называть модальную формулу негативной, если она построена из переменных II константы У с использованием только связок V 11 □. Множество штативных формул Т будем называть негативной теорией, если для любых негативных формул А, В из А € Т и К 4 НА ^ В следует В € Т. Аналогично, строго позитивной теорией мы называем множество строго позитивных формул Т такое, что для любых строго позитивных формул А, В из А € Т я К 4 НА ^ В следует В € Т.

Определим оператор * на строго позитивных формулах, индуктивно по их построению: Р* = Р, Т* = У, (А Л В )* = А* V В*, (ОА)* = □А*. Несложно видеть, что для любых строго позитивных формул А, В верно К 4 НА ^ В тогда и только тогда, когда К 4 НВ * мА*.

Если Т c Fm — строго позитивная теория, то двойствсппой теорией Т* будем называть множество формул {А* | А € Fm \ Т}. Несложно проверить, что Т* действительно является негативной теорией. Аксиоматизацией такой теории будем называть множество строго негативных формул М такое, что для любой формулы А € Т* найдётся конечное т подмножество формул В1, В2,..., Вт из М: К4 Н В ^і ^ А.

і=1

Следствие 1. Пусть Т — строго позитивная теория на конечном наборе переменных, замкнутая относительно аксиом и правил вывода К 4⁺. Тогда у двойственной теории Т * есть конечная аксиоматизация.

Доказательство. Рассмотрим дополнение к теории Т в языке строго позитивных формул на данном наборе переменных. Согласно свойствам стройного предпорядка, это множество имеет конечный набор минимальных элементов Аі , А* ,..., А_т', то есть для любой строго позитивной формулы В € Т найдётся формула Аг такая, что К 4 НВ ^ Аг. Тогда набор формул А*, А*, ..., Ат есть набор аксиом для Т *. Проверим это: пусть В € Т * , В = С *, где С — некоторая строго позитивная формула. Тогда по опреде.тешпо С / Т. н для одной из формул Аг имеем К 4 НС ^ Аг, а это равносильно К 4 НА* мС * = В, что и требовалось.

Отметим, что похожий результат был ранее получен Беклемишевым для логики GLP- [22. Теорема 3.4].

Лемма 2. В каэюдом классе эквивалентности по отношению Д существует формула А такая, что если К 4 Н А о В, то |Т [В] | > |Т [ А] | и ли Т [А] и Т [В ] изоморфны.

Доказательство. Предположим противное: существуют две эквивалентные в К 4 формулы А, В, при этом \Т [А]| = \Т[В]У Т [А] и Т [В] не изоморфны, и размер \Т [А]| — минимальный в своём классе эквивалентности. Мы предполагаем, что размер |Т[А]| — минимально возможный среди всех таких пар (А, В).

Обозначим А = ад Л Oa1 Л ... Л Oa_m и В = Ьд Л Obi Л ... Л Ob^, г де ад и Ьд не содержат O. Ясно, что qq = Ьд. Определим функцию ф: {1, 2,..., к} ^ {1, 2,..., т} такую, что если ф(г) = 3 ■ ^то К 4 Н Obj ^ Oat. Если более одного значения j можно выбрать в качестве ф (г), мы можем выбрать любое. Аналогично определим функцию g : {1, 2,..., т} ^ {1, 2,..., к}.

Допустим, что ф не сюръективна, то есть ф(г) = j не выполняется ни при каком г и фиксированном j. Положим В' = Ьд Л Obi Л ... Л Obj-i Л Obj+i Л ... Л ОЬ^. Тогда К 4 Н А о В', что противоречит минимальности |Т[А]| в своём классе эквивалентности. Поэтому ф (и также g) сюръективна, и т = к. Получаем, что h = g о ф является перестановкой, и для некоторого натурального I выполнено Ы = id. Это сооответствует тому, что К 4 Н Oat ^ ... ^ O q ^ ( ^ ) ^ Obj (t) ^ Oat для любого г. Поскольку Oat и Oa^(t) эквивалентны и |Т[А] | минимален, на деле выполнено равенство h = id. Так как Oat и Obj (t) эквивалентны, возможны случаи К 4 Н at ^ bj(t) ^и К 4 Н at ^ Obj (t), ^но второй случай влечёт К 4 Н at ^ Oat, противоречие. Итак, at и bj(t) эквивалентны; поскольку размеры |Т[А]| = |Т[В] | минимальны в их классе эквивалентности, то же можно сказать про |Т[at] | = |Т[bj(t)]|. Наконец, поскольку |Т[А] | >  |Т[at] |, Т [at] и Т[bj (t)] изоморфны. Объединяя эти изоморфизмы между поддеревьями с перестановкой ф, мы получаем изоморфизм между Т [А] и Т [В], что противоречит начальному предположению.

Если формула А минимальна, то формулы, соответствующие максимальным поддеревьям Т [А], также минимальны и попарио несравнимы по отношению Д'. Отметим также, что в работе Джексона [12, 2.8-2.13] была дана схожая характеристика для классов эквивалентности в логике S 4⁺.

Пусть М = (W, 6) — частично упорядоченное множество. Антицепью называется любое подмножество W, состоящее из попарно несравнимых элементов. Определим пополнение аптиирпями Mg = (Wg, Д) следующим образом:

• 1)    Wg — множество всех антицепей в W:

• 2)    х Д у О V а Е х 3 Ь Е у а 6 Ь.

Лемма 3. Пусти А, В — минимальные строго позитивные формулы, и в корнях Т [А] и Т [В] верпы одни и те .же. переменные. Обозначим А1... А_т и В1... В^ формулы, соответствующие максимальным поддеревьям Т [А] и Т [В]. Следующие утверждения эквивалентны:

• (г) А ДВ. или К 4 НВ -А.

• (и) А Д' В. или К 4 НВ - А V OА:

• (Ш) {А1 ... А_т} < {В1... В^ }. в значатси порядка (Ғт/^, Д')^ү.

Доказательство. Из (іі) следует, что существует гомоморфизм ф : Т [А] ^ Т [В]; мы можем переопределить его значение в корне ф (г(А)) = г(В), а наличие гомоморфизма с таким условием в корне влечёт (і). Тем самым первые два утверждения равносильны.

Если ф : Т [А] ^ Т [В] — гомомор<])іізм. то для каждого г = 1 ...т мы имеем ф ( г ( А і )) Е Т[Вj ] при некотором j, и ф 1_Т [^.] — гомоморфизм, отображающий А і на Вj. И обратно, если мы объединим произвольные гомоморфизмы фі : Т [ А і ] ^ Т [Вj(t)], г = 1 ...т, іі положим ф (г(А)) = г (В), мы получим гомомор<]шзм ф : Т [А] ^ Т [В]. Тем самым равносильны утверждения (і) и (ііі).

Заметим, что А У’ В влечёт наличие гомоморфизма f: Т [И] ^ Т[В], и тем самым высота дерева Т [А] не более высоты Т [В], а еели f(г(А)) = т(В ), то высота строго меньше. Поэтому А У’ В и В У’ А влечёт А У В и В У А; таким образом, в отношениях z^ и ^‘ одинаковые классы эквивалентности.

Следующие определение и лемму мы заимствуем из статьи [3].

Пусть X , У — частично упорядоченные множества. Функция f : X ^ У называется квазивложением, если f (жі) 6у f (ж₂) влечёт ж_і 6х ж₂ для любых ж_і,ж₂ € X.

Лемма 4. Пусть X, У — частично упорядоченные множества, и f: X ^ У — квазивложение. Если У является стройным порядком, то стройным порядком является также X, причём o(X ) 6 о(У ).

Доказательство. Предположим, что {ж_п} — бесконечная последовательность элементов X. Последовательность { f (ж_п)} содержит бесконечную неубывающую подпоследовательность {f (ж₅(_п))}, так как У — стройный порядок. По определению, {ж₅(_п)} также не убывает, поэтому X — стройный порядок.

Пусть У — линейный порядок, расширяющий 6 у. Если жі У ж2, то соответствующие элементы f (жі) ii f (ж₂) могут быть либо несравнимы, либо f (жі) <у f (ж₂) (иначе ж2 6х жі-противоречие), поэтому можно расширить 6у сравнением f (жі) <  f (ж₂). Если добавить все такие сравнения, мы получим линейный порядок на множестве f (X), изоморфный порядку (X, У) ii расширяют пин порядок 6у в ограничении на. f (X). поэтому o(X) 6 о(У).

2^г1

Лемма 5. Ординальный тип предпорядка (Fm, У) на п переменных не менее ш^ш

Доказательство. Заметим, что существует естественное квазивложение из строк в алфавите ({0,1}^п) на формулы в Fm/ ^, соответствующие линейным деревьям. При этом формулы, соответствующие линейным деревьям, минимальны. Поэтому мы можем применить теорему [4, Теорема 3.11] и тот факт, что о({0,1}^п) = 2^п.

Теорема 3. Ординальный тип предпорядка (Fm, У’) на п переменных не превосходит eq.

Доказательство. Пусть Fmi — множество строго позитивных формул с одними и теми же верными переменными в корне (г = 1... 2п). Согласно лемме 3, имеет место соотноше-п                  п ние (Fm/^, У’) = | | (Fmi/^, У’) = |J(Fm/^, У‘)д. Это определяет порядок (Fm/^, У’) і=і                  і=і рекурсивно. Тогда его ординальный тип не превосходит supfт(0), где f — соответствуют щая функция на ординалах; согласно [3, Теорема 2.18] и [4, Теорема 3.5], f (а) < ш“ х 2п (где х обозначает натуральное произведение ординалов), и тогда supfт(0) < Eq.

т

Следствие 2. Ординальный тип предпорядка (Fm, У) на п переменных не превосходит Eq X 2^п.

п

Доказательство. Имеется соотношение (Fm/^, У) = | | (Fm_i/~, У’), откуда и получаем і=і

o(Fm/^, У) < o(Fm_i/~, У) х 2^п<  e_q х 2^п.

Автор благодарит своего научного руководителя Л.Д. Беклемишева за обсуждения и помощь в процессе подготовки рукописи.