Строго позитивные фрагменты модальных логик тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Святловский Михаил Владимирович

• Святловский Михаил Владимирович
• кандидат наук
• 2025

Оглавление диссертации кандидат наук Святловский Михаил Владимирович

3.1 Логика $5+

3.2 Корректность аксиоматизации БТ(Я5т)

3.3 Полиномиальная разрешимость $ 5т

4 Аксиоматизация строго позитивного

фрагмента логики ^4

4.1 Линейные модели Крипке

4.2 Аксиома сотпгИп

4.3 Корректность аксиоматизации БТ(К4.3)

4.4 Характеристический класс шкал Крипке для5"Р(К4.3)

5 Полиномиальная разрешимость

ЯГ (К 4.3)

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

6.1 Определение стройного предпорядка

6.2 Отношение следования на строго позитивных формулах

6.3 Ординальный тип

7 Критерий модального напарника

8 Модальные напарники БТ(К4)

8.1 Канонические формулы шкал

8.2 Конфинальные канонические формулы

8.3 Неконфинальные канонические формулы

9 Заключение 93 Список литературы

1 Введение

Введение диссертации (часть автореферата) на тему «Строго позитивные фрагменты модальных логик»

Актуальность темы исследования и степень ее

разработанности

Данная работа посвящена исследованию строго позитивных фрагментов модальных логик. Такие фрагменты рассматривались ранее в контексте универсальной алгебры, в изучении дескрипцион-ных логик и в логике доказуемости.

Универсальная алгебра. Строго позитивные формулы строятся из переменных и константы Т с помощью связок Л и 0- Соответственно, с точки зрения универсальной алгебры, импликации между строго позитивными формулами (далее секвенции) соответствуют тождествам в языке нижних полурешеток с несколькими монотонными операторами. Строго позитивные логики при этом соответствуют многообразиям таких алгебр. В частности, в работе М. Джексона [1] рассмотрены полурешетки с операторами замыкания (closure semilattices, CSL). В этой работе описана решётка подмногообразий нормальных CSL (то есть расширения строго позитивной логики SV(S5)), а также показано, что у многообразий конечных CSL с единицей имеется конечный базис.

В работе С. Кикотя и др. [2] рассматривается вопрос о полноте по Крипке для строго позитивных логик. Известно, что строго позитивная логика полна по Крипке тогда и только тогда, когда она является строго позитивным фрагментом некоторой нормальной модальной логики. В отличие от модальных логик, не полных по Крипке, существуют простые примеры не полных по Крипке строго позитивных логик — например, логика, порождённая аксиомой §р ^ §q. В той же работе доказано, что все расширения модальной логики S5, за

исключением двух, полны по Крппке; также показано, что проблема полноты по Крипке алгоритмически неразрешима.

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

Другие вопросы общей теории строго позитивных логик рассматривались в нескольких работах М. Захарьящева, Ф. Вольтера, А. Куруш, С. Кикотя и других [3, 4, 5, 6, 8].

Дескрипционные логики используются в базах данных, снабженных некоторой способностью делать логические выводы на основе имеющихся данных (базах онтологий). Так, в базе медицинской терминологии БМОМЕБ СТ применяется строго позитивная логика ЕС, описанная в работах [9, 10, 11] вместе с эффективным разрешающим алгоритмом. Логика ЕС позволяет находить ответ на запрос за полиномиальное время от длины запроса, что показано в работе [9]. Для многих дескрипционных логик были известны алгоритмы, которые работают в худшем случае экспоненциальное время, но вполне применимы на практике благодаря оптимизациям. В работе [11] показано, что алгоритм для логики ЕС не уступает таким алгоритмам в производительности.

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

языка модальной логики. Для примера, полимодальная логика GLP не полна по Крипке [13] и PSPACE-полна [14], в то время как её строго позитивный фрагмент RC одновременно полон по Крипке и полиномиально разрешим [15]. Далее, в работах Л.Д. Беклемишева [16, 17, 18] и других авторов [19, 20, 21, 22, 23] были предложены новые арифметические интерпретации строго позитивных логик — например, для логик RC и RC& модальности соответствуют равномерным принципам рефлексии. Логика RC& при этом тоже полиномиально разрешима и полна относительно простого класса конечных моделей Крипке. В целом, можно сказать, что аппарат строго позитивной логики занял важное место в исследованиях по логике доказуемости и ее применениям к ординальному анализу логических теорий.

Цели работы. Мы рассматриваем следующую связь между модальными логиками и строго позитивными логиками. Модальной логике L сопоставляется ее строго позитивный фрагмент логики SV(L), который определяется как множество всех секвенций (импликаций между строго позитивными формулами) из L. По строго позитивной логике Р можно получить нормальную модальную логику К 0 Р — замыкание К U Р относительно правил вывода modus ponens, подстановки и усиления (обозначение М.С(Р)). Если Р = SP(L), то мы называем L модальным напарником Р. Отображения SV и вместе образуют соответствие Галуа, аналогичное соответствию между модальными и суперинтуиционистскими логиками [24].

Это соответствие было подробно изучено, начиная с работы [25]. Известно, что у каждой суперинтуиционистской логики есть наибольший модальный напарник, и что соответствующие отображе-

ния являются изоморфизмами решёток расширений ExtlPC и NExtGrz (теорема Блока-Эсакиа, см. [26]). Соответственно, вопрос о существовании наибольшего модального напарника интересен и для строго позитивных логик. Мы получаем отрицательный ответ на данный вопрос и показываем, что у строго позитивной логики SV(К4) есть как минимум два различных максимальных модальных напарника. Соответственно, вопрос о наличии удобного отображения между строго позитивными логиками и их модальными напарниками, как и вопрос о свойствах такого отображения, пока остается открытым.

Можно также начать исследование с конкретных расширений К4 и рассмотреть отображение M.Cs4..3(P) = $4.3 0 Р, которое исследуется в работе [7], или отображение M.Cs5(P) = S5 0 Р из работы [1]. При этом у любой строго позитивной логики, расширяющей SV(S4.3), максимальный модальный напарник единственен [7, Теоремы 5.2, 5.3]. То же верно и для строго позитивных логик, расширяющих SV(£5) — с одной стороны, просто потому, что 54.3 С S5, с другой стороны, этот факт можно установить отдельно, поскольку известны все строго позитивные логики, расширяющие SV(S5), и известны все нормальные расширения логики S5 [27].

В данной работе мы анализируем расширения логики К4, используя для этого введенные М. Захарьящевым [28, Section 9] канонические формулы шкал, хотя и не добиваемся полного анализа. Тем не менее, мы указываем множество всех модальных напарников SV(К4) в классе расширений К4 каноническими формулами ирре-флексивных шкал, включая наибольшую логику в этом множестве. Также мы находим критерий того, является ли некоторая модальная логика модальным напарником SV(К4)7 и показываем, что логика

GL те является максимальным модальным напарником SV(К4).

Стройные предпорядки. В работе также рассматривается отношение следования на строго позитивных формулах как отношение предпорядка. Теория стройных предпорядков (известных в англоязычной литературе как well-quasi orders) интересна с точки зрения теории множеств и комбинаторики, поскольку многие естественные структуры, такие как порядок на словах и порядок на деревьях [29, 30], оказываются стройными предпорядками. Одна из таких структур, как показано в статье [31] — стройный предпорядок по вложению на линейных порядках. Стройные предпорядки также активно используются для доказательства терминируемости систем переписывания термов (например, как в статье [32]). Помимо этого, стройные предпорядки применялись для проблемы разрешимости фрагментов логики предикатов (см. [33]).

Известны и применения стройных предпорядков в теории доказательств — например, финитная форма теоремы Крускала даёт пример естественного комбинаторного утверждения, не доказуемого в сильной арифметической теории ATR0 [34]. Более подробный логический анализ теоремы Крускала, вместе с её финитной формой и выводом ординального типа стройного предпорядка на деревьях, дан в статье [35]. В статье [36] обсуждается соответствие между другим независимым от арифметики Пеано комбинаторным утверждением — принципом Червя — и известным стройным предпоряд-ком на словах из натуральных чисел или, что то же, на замкнутых модальных формулах полимодальной логики доказуемости GLP-. Этот стройный порядок имеет природу, близкую к изучаемому в настоящей работе.

Отдельно стоит сказать про стройный порядок по отношению го-

моморфизма на размеченных деревьях, в котором метками являются натуральные числа от 0 до к; ввиду определения канонического дерева и теоремы 1, можно проследить его сходство с порядком по отношению следования. В работах [37, 38] подробно изучается структура этого порядка, в частности, вопросы определимости различных естественных операций на нём с помощью формул первого порядка.

Современные результаты о стройных предпорядках собраны в книге [39], в частности, в статье [40] рассматриваются различные ординальные характеристики стройных предпорядков, в том числе ординальный тип. Мы находим верхнюю и нижнюю оценки ординального типа для указанного стройного предпорядка на строго позитивных формулах.

Работа организована следующим образом. В разделе 2 вводятся основные понятия, такие как строго позитивный фрагмент, семантика Крипке, свойства шкал/моделей Крипке и отображений между ними. В разделе 3 мы исследуем строго позитивный фрагмент полимодальной логики $5т. В разделе 4 мы находим аксиоматизацию строго позитивного фрагмента логики К4.3, затем в разделе 5 доказываем полиномиальную разрешимость этого фрагмента. В разделе 6 мы исследуем естественное отношение следования на строго позитивных формулах (от конечного набора переменных) как отношение предпорядка, доказываем, что это стройный предпорядок, и находим верхнюю и нижнюю оценки его ординального типа. В разделе 7 мы формулируем и доказываем критерий того, является ли модальная логика модальным напарником БТ(К4). С помощью этого критерия в разделе 8 мы исследуем множество расширений К4 и, в частности, находим, что у БТ(К4) существуют хотя бы два различных максимальных модальных напарника.

Основные положения, выносимые на защиту

1. Получены явная конечная аксиоматизация и результат о полиномиальной разрешимости строго позитивных фрагментов логик S5mn К4.3.

2. Доказано, что естественный порядок следования в К4 на строго позитивных формулах от фиксированного конечного набора переменных является стройным предпорядком (well-quasi order). Найдены нижние и верхние оценки ординального типа данного предпорядка.

3. Получен критерий того, является ли модальная логика модальным напарником SV (К4), и с его помощью доказано, что логика GL те является максимальным модальным напарником К4. Также доказано, что у SV(К4) существуют хотя бы два различных максимальных модальных напарника, и найден наибольший модальный напарник SV(К4) в классе расширений К4 каноническими формулами иррефлексивных шкал.

Цель работы и основные задачи

Основной задачей работы является исследование строго позитивных логик и их алгоритмических и семантических свойств.

Теоретическая и практическая значимость работы

Диссертация носит теоретический характер. Полученные в ней результаты имеют значение в приложениях модальной логики, таких как теория онтологических баз данных и теория доказательств.

и

Методы исследования

В диссертации используются классические методы модальной логики: метод канонической модели, метод пополнения модели вершинами, канонические формулы шкал Захарьягцева и другие. Также в диссертации предложены новые идеи, такие как линеаризации дерева и пополнение антицепями.

Апробация результатов

По теме диссертации были сделаны доклады на следующих научных конференциях и семинарах:

— Международная конференция «Workshop on Proof Theory, Modal Logic and Reflection Principles», Москва, МИАН, 2017;

— Международная конференция «Workshop on Proof Theory, Modal Logic and Reflection Principles», Барселона, 2019;

— Семинар отдела математической логики «Теория доказательств», МИАН;

— Семинар «Современные проблемы математической логики», факультет математики НИУ ВШЭ.

Публикации

Основные результаты по теме диссертации изложены в 3 работах. Две из них опубликованы в журналах, входящих в перечень ВАК; 2 из них — в журналах, индексируемых базой Scopus; 2 из них — в журналах, индексируемых базой Web of Science. Все результаты, выносимые на защиту, получены автором диссертации самостоятельно.

Объём и структура работы

Диссертация состоит из введения и 8 разделов (включая заключительный). Полный объём диссертации составляет 100 страниц. Список литературы содержит 46 наименований.

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

2.1 Строго позитивные фрагменты

Формулы модальной логики строятся из переменных Var = {Po,Pi,...} и константы Т с использованием логических связок Л, — и унарной модальности 0. Символы V, □р = —0—р и □+р = р Л □р мы используем как стандартные сокращения. Обозначим С [А/р] — результат замены каждого вхождения переменной р в формуле С на формулу А.

Нормальная модальная логика — множество модальных формул, содержащее аксиому нормальности □(Л ^ В) ^ (□Л ^ □В) и замкнутое относительно следующих правил:

А, А ^ В

- (правило modus ponens)

В

С [р] С [А/р]

А

(подстановка)

(правило усиления)

□Л

Минимальная нормальная модальная логика традиционно обозначается К.

Пусть Ь — некоторая нормальная модальная логика, р — некоторая модальная формула. Выражение Ь 0 р обозначает замыкание множества формул Ь и {р] относительно указанных выше правил. Так, например, К 0 (□р ^ □□р) — логика К4.

Строго позитивные формулы — модальные формулы, построенные из переменных и константы Т только с помощью связок Л и 0-

Строго позитивными импликациями, или секвенциям,и, мы будем называть формулы вида А ^ В, где А и В — строго позитивные формулы.

Строго позитивный фрагмент модальной логики Ь — множество всех секвенций в Ь (обозначение БТ (Ь)).

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

А ^В, В ^С 1_А ^ А,А ^Т, В_^С

А ^ В, А ^ С

2. А Л В ^ А, А Л В ^ В,

3.

А ^ В ЛС А В

О А ^ ОВ

В общем случае, нормальная строго позитивная логика — множество секвенций, замкнутое относительно аксиом и правил вывода исчисления К а также правила подстановки. Исчисление К + соответствует семантике (нижних) полурешёток с монотонными операторами (БЬО, для краткости): в К + выводятся те и только те секвенции, которые верны в любой ББО. Известно также, что все выводимые в К+ секвенции составляют строго позитивный фрагмент модальной логики К. Далее мы будем рассматривать только нормальные строго позитивные логики.

Следующую лемму мы заимствуем из статьи [24].

Лемма 1. (о позитивной замене) Пусть С — строго позитивная формула, и секвенция А ^ В выводима в К + . Тогда, в К + выводима также секвенция С[А/р] ^ С[В/р].

Доказательство. Проведем индукцию по построению формулы С.

Если р те содержится в С, то утверждение тривиально, так как С [А/р] = С [В/р] = С.

Если С = р, то секвенция С [А/р] = А ^ В = С [В/р] выводится по условию.

Если С = С\ Л С% то выводятся секвенции С\[А/р] ^ Cl[B/p],C2[A/p] ^ С2 [В/р] (по предположению индукции), С [А/р] ^ С\[В/р], С [А/р] ^ С2[В/р]и С [А/р] ^ С [В/р] (по правилам для конъюнкции).

Наконец, если С = QCi, то выводятся секвенции С\[А/р] ^ Ci[B/p] (по предположению индукции) и §С\[А/р] ^ §С\[В/р]. □

Пусть Ь — некоторая нормальная строго позитивная логика, р — некоторая секвенция. Выражение Ь + у обозначает минимальную нормальную строго позитивную логику, содержащую р и Ь. Так, например, БТ(К) + (00^ ^ §А) — логика К4+, она же строго позитивный фрагмент модальной логики К4.

2.2 Семантика

Мы используем общепринятую семантику Крипке:

о Шкала Крипке — пара Т = Д), где W — непустое множество вершин, а Я — бинарное отношение на W.

о Модель Крипке — тройка М = ( W,R,V), где (}¥,К) — шкала Крипке, а V, или оценка, — произвольное отображение V: Уаг ^

о Оценка тереме иных V (р) однозначно определяет оценку формул V(А), где А — произвольная модальная формула. Оценка определяется индукцией по построению формулы А: V(Т) = Ж, V(-А) = Ж \ V(<р), V(А Л В) = V(А) П V(В), V(ОА) = [х | Зу е V(А): хRy}.

о Обобщённая шкала Крипке — тройка С = ), где Р —

алгебра подмножеств Ж, 0 е Р и Р замкнуто относительно операций X ПУ,Ж \ X и итерации О ОА = [у | Зх е X: yRх}. Таким образом, обычную шкалу Крипке можно считать обобщённой шкалой, положив Р = 2W.

о Будем говорить, что модель (Ж, R, V) (точнее, её оценка V) допустима в обобщённой шкале ), если для любой переменной р выполнено V(р) е Р. И наоборот, по данной модели М = (Ж, R, V) мы можем определить обобщённую шкалу (Ж, R, Р), где Р состоит из всех множеств вида V(А) — это минимальная обобщённая шкала, допускающая М.

о Будем писать М,х |= А, если х е V(А) и М |= А, если V(А) = Ж. Мы также пи шем Т = А (или С = А), тел и М = А для каждой (допустимой) модели М, построенной па шкале Т (па шкале С).

о Пусть Ь — модальная логика, & С обобщённая шкала. Мы говорим, что С — шкала логики Ь, если А е Ь ^ С = А, для

А С

Ь

мы говорим, что логика Ь характеризуется С, если А е Ь ^ Т = А, для каждой формулы А и шкалы (модели) Т е С.

о

ли Криике, мы используем обозначение Уаг(х) = [р | х е V(р)}.

В части данной работы мы также говорим о полимодальной логике, в которой т модальноетей О1, О2,..., От вместо одной модальности. Соответственно, в шкале (модели) Крипке в этом случае подразумеваются отношения Rl, R2,..., Rm вместо отношения R.

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

2.2.1 Список модальных логик, упомянутых в работе

о К минимальная нормальная модальная логика, или логика класса всех шкал;

о К4 = К 0 (□р ^ □□р) — логика класса всех транзитивных шкал;

о СЬ = К0 (□(□р ^ р) ^ □р) — логика Гёделя-Лёба, или логика класса нётеровых частичных порядков;

о 34 = К4 0 (□р ^ р) логика предпорядков;

о = Б4 0 (р ^ □Ор) — логика отношений эквивалентности;

о К4.3 = К4 0 (□(□^ ^ о) V □ (□^ ^ р)) — логика линейных порядков;

о СЬ.3 = СЬ 0 (□(□^ ^ д) V □ (□^ ^ р)) — логика, которая характеризуется классом строгих линейных порядков;

о ^4.3 _ $4 0 (□(□+р ^ д) V □ (□+д ^ р)) — логика класса нестрогих линейных порядков.

2.3 Свойства и отображения шкал Крипке

Шкала Крипке Т = Я) (или соответствующая модель) называется:

о иррефлексивнощ если Ух Е W: —хЯх; о

Ух, у Е W: —(хЯу Л уЯх);

о транзитивной., если Ух,у, г Е W: (хЯу Л у Яг) ^ хЯг;

о шкалой с корнем г Е Ж, есл и У у Е W: г = у V гЯу;

о линейной, если шкала антисимметрична и Ух, у, г Е W: (хЯу Л хЯг) ^ (у = г V у Яг V гЯу);

о

любой вершины х Е Ж мпожество {у | уЯх] линейно и конечно;

о

пей (вида х0Ях\Ях2Я.. .)■

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

о Корень шкалы г е Ж, если он существует, сокращённо обозна-( Т)

о Если х,у е Ж и хRy, то у ^ потомок х и х — предок у. Если также V ^ е Ж — (хRzЛzRy), то у — непосредственный потомок.

о Если 3 С Ж, х е Ж и V« е 3: хRs, то х ^ предок 3. Если пет такой вершины у7 что у — предок 3 и х^у., будем называть х 3

единственный, и мы можем обозначить х = Iса(3)).

ох ^ обозначает х и всех его потомков (также распространено название верхний конус х. Аналогично, 3 У х

хев

ох | обозначает х и всех предков х (также распространено название нижний конус х. Аналогично, 3 У х

хев

о Если 3 — непустое подмножество Ж и Ух, у е 3: — (х^у V yRх)7 3

Предложение 1. Если, шкала (Ж^) древовидная и конечная, то любое непустое подмножество 3 С Ж или, содержит корень шка-

а( 3)

Т

шинами с1(х, у) следующим образом:

• (1(х, х) = 0;

• если хЯу7 то (1(х, у) — длина пут и от х до у7 где на каждом шаге от вершины мы переходим к её непосредственному потомку;

• в прочих случаях (1(х,у) = — 1.

Высота Н(х) — это расстояние от х до наиболее удалённой вершины в ж Для краткости мы обозначим Н(Т) = Н(г(Т)). Если у вершины ж не менее двух непосредственных потомков и Н(х) = к, мы называем это ветвлением высоты к. Говоря о транзитивных и антисимметричных шкалах, мы будем иногда использовать обозначение х < у вместо хЯу и соответствующую терминологию частичных порядков (несравнимые элементы, минимальный/максимальный элемент и т.п.).

Пусть М = Я, у) — некоторая модель Крипке. Размером этой модели (обозначение 1М\) мы будем называть величину ^I + 1Щ + X} |"Уаг(ж)|. С учётом того, как организован доступ к

ХЕШ

памяти в большинстве языков программирования, описание каждого единичного фактам Е Уаг(х) на практике имеет не единичный размер, как в нашем определении, а размер порядка 1од(1); аналогично для описания факта (х, у) Е ^ в случае полимодальной логики. Мы опустим эти логарифмические множители, поскольку на истинность интересующих нас утверждений вида "величина / полиномиально зависит от величины д]] они не влияют.

Шкала Крипке 5 = Я0) называется подшкалой Т = (Ш, Я), если Wo С W ж Я0 = Я^о - Если при этом выполнено Wo ^ Wo то 5 называется конфинальнои подшкалои. Аналогично, (^0,Я0,У0) —

подмодель (Ж^, V), если (Ж0, Ro) — подписал а (\¥,К) к Уо(р) = V(р) П Обобщённая шкала Крипке С0 = (Ж0, R0, Р0) называется подшкалой С = (Ж, R, Р), если Я® = R|w0 и Р0 С Р.

Пусть С1 = (Ж1, R1,Р1) и С2 = (Ж2, R2, Р2) — обобщённые шкалы Крипке. Отображение /: ^ Ж2 называется р-морфизмом с С1 на С2) если:

(Р2) Ух,у еЖ1: х^1у ^ /(х)Еа/(у);

(РЗ) Ух еЖ1,у еЖ2: (f(х)R2y ^ Зг е : х^г Л ¡(г) = у);

(Р4) УХ еР2: Г\х) еРъ

Если / — р-морфизм Т2, и 81 — (конфинальная) подшка-

ла Т1 = (Ж1, R1), то / можно также назвать частичным (конфи-

Т1 Т2

3 С мы обозначаем /(3) = [/(х) | х е 3 П йот /}.

Пусть М1 = (Ж1, R1,V1) и М2 = (Ж2^^¿,¥'2) — транзитивные модели Крипке. Отображение /: ^ Ж2 — гомоморфизм, если:

1. Ух,у е : х^1У ^ (у);

2. Ух еЖ1: Уаг1 (х) С Уаг2(/(х)).

Если обе модели с корнем и /(г(М1)) = г(М2), мы называем / корневым гомоморфизмом. Если /: ^ Ж2 — гомоморфизм, и /-1: Ж2 ^ ^ — также гомоморфизм, то мы называем / изоморфизмом, а модели Ж1, Ж2 — изоморфными.

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

\.f гомоморфизм;

2. если w1, w2 — два различных непосредственных потомкам в модели Mi, то f (v) = lca(f (w1),f (w2)).

2.4 Канонические деревья

Следуя работе [15], для каждой строго позитивной формулы Л мы определяем её каноническое дерево Т[А] — древовидную и транзитивную модель Крипке с корнем. Аналогичные понятия использовались и ранее — например, в работе М. Джексона [1] похожий объект называется term, tree.

Мы используем индукцию по строению формулы А. Если А — переменная пли константа Т, то Т[А] — модель из единственной вершины, в которой истинна А.

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

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

Нетрудно видеть, что размер модели \Г[А]1 полиномиально зависит от длины формулы IAI.

Следующие лемма и теорема о связи канонических деревьев со строго позитивным фрагментом К4 доказаны в [15, Леммы 5.3-5.6]:

Лемма 2. Пусть M — транзитивная модель Крипке, А — строго позитивная формула. Тогда, M.,x = А, если и только если существует гомоморфизм f: Т[А] ^ M такой, что f (г(Т[А])) = х.

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

(г) (А ^ В) е К4;

(И)Т [А], г(Т [А]) =В;

(Ш) существует корневой гомоморфизм /: Т[В] ^ Т[А].

3 Аксиоматизация и полиномиальная разрешимость строго позитивного фрагмента логики 55т

Аксиоматизация строго позитивных фрагментов может быть нетривиальна для модальных логик, которые не заданы строго позитивными (или эквивалентными им) аксиомами. Здесь мы рассмотрим первый пример такого рода — логику отношений эквивалентности $5т. Мы воспользуемся тем, что отношение эквивалентности можно определить как рефлексивное, транзитивное и евклидово отношение — поскольку выразить тот факт, что отношение симметрично, с помощью только строго позитивных аксиом не удается.

ЗЛ Логика 55+

Логика $5т, т.е. логика т отношений эквивалентности — одна из наиболее важных эпистемических логик. Она полна относительно класса шкал Я\,... , Ят)7 где в се Щ — отношения эквивалентности ([28, Предложение 3.76]).

Определим исчисление логики Б5т (для каждого г = 1, 2,..., т):

1. аксиомы и правила К4 для 0«;

2. □¡А ^ А (рефлексивность);

3. 0¡А ^ □¿О«^ (симметричность).

В работе [2, Теорема 23] доказана полнота некоторого исчисления для строго позитивного фрагмента одномодальной логики $5.

Мы рассмотрим сразу полимодальный случай; хотя различие между ними и несущественно, это позволит продемонстрировать методы, используемые в данной работе.

Перечислим аксиомы и правила вывода с.п. логики 35+(для каждого г = 1, 2,... ,т):

1'. аксиомы и правила К4+для 0«;

2'. А ^ ^¡А (рефлексивность);

3'. ^¡А Л ^¡В ^ 0г(А Л 0гВ) (евклидовость).

Лемма 3. Для любого натурального п и любых строго позитивных формул А,В1,В2,... ,Вп в 35^ выводима секвенция 0«А Л

п I п \

Д 0гВ3 ^ 0Л А Л Л 0гВ3 .

з=1 V /

п

Если п = 1, то данная секвенция совпадает с аксиомой 3'. Если п > 1, то в 35^ выводимы следующие секвенции:

п п—1

0гА Л Д 0гВ3 ^ 0.А Л Д 0гВ3 Л 0гВп з=1 3=1

п—1 / п—1 \

0гА Л Д 0гВ3 Л 0гВп ^ оЛ а Л Д 0.ВЛ Л 0А (пр. пнд.

3=1 \ 3=1 )

/ п—1\ / п—1 \

0^А Л Д 0гВ^ Л 0гВп ^ 0^А Л Д 0гВ3 Л 0гВ„1 (акс. 3')

'3 I ' х чг^п ^ V« I ^± ' ^ / \ Vг^]

3=1 ) V 3=1

/ п—1\ / п \

0^А Л Д 0гВ3 Л 0гВ„1 ^ 0^А Л Д

п

Соединяя начало и конец цепочки, заключаем 0iA А Д 0iBj ^

3=1

^ А Д 0^ .

0< ( А А /\ 0гВ3 I. □

3=1

3.2 Корректность аксиоматизации БТ(55т)

Теорема 2. В 35^ выводимы те и только те секвенции, которые выводимы в Б5т.

Доказательство теоремы будет похоже на стандартный для модальной логики метод канонической модели — с той разницей, что, во-первых, вместо всех максимальных непротиворечивых теорий (как в [16]) мы рассмотрим вообще все теории. Во-вторых, мы модифицируем отношения Щ на канонической модели $5^, поскольку в последней отношения не будут отношениями эквивалентности.

Рассмотрим модель Крипке М = ..., Ятгде:

I ^ ...................... множество всех непустых $5+-теорий, то есть множеств

строго позитивных формул, замкнутых относительно вывода в 5 5+:

т1

2. для любых х,у £ W и % = 1.. .т хЩу тогда и только тогда, когда для любой строго позитивной формулы А 0iА £ х ^ 0гА £ у;

Список литературы диссертационного исследования кандидат наук Святловский Михаил Владимирович, 2025 год

Список литературы

[1] М. jackson 'Semilattices with closure', Algebra Universalis 52:1-37, 2004.

[2] S. Kikot, A. Kurucz, Y. Tanaka, F. Wolter, and M. zakharyaschev, 'Kripke completeness of strictly positive modal logics over meet-semilattices with operators', Journal of Symbolic Logic, vol.84(2019), pp.533-588.

[3] Kurucz A., Wolter F., Zakharyaschev M. Islands of Tractability for Relational Constraints: Towards Dichotomy Results for the Description of Logic EL. // Advances in Modal Logic. — 1998. — P. 271-291.

[4] Gabbay D., Kurucz A., Wolter F., Zakharyaschev M. Many-Dimensional Modal Logics: Theory and Applications. // Studies in Logic and the Foundations of Mathematics. — 2003. 2003.

[5] Kurucz A., Wolter F., Zakharyaschev M. Islands of tractability for relational constraints: towards dichotomy results for the description logic EL. // London, UK: College Publications. - 2010. - P. 271291.

[6] Kikot S., Kurucz A., Tanaka Y., Wolter F., Zakharyaschev M. On the completeness of EL-equations: First results. // 11th International Conference on Advances in Modal Logic, Short Papers (Budapest, 30 August-2 September, 2016). - P. 82-87.

[7] Kikot S., Kurucz A., Wolter F., Zakharyaschev M. On strictly positive modal logics with S4.3 frames. // Advances in Modal

Logic, Vol.12 (eds.: G.Bezhanishvili, G.D'Agostino, G.Metcalfe and T.Studer), College Publications (2018), pp.399-418.

[8] Kikot S., Kudinov A. On Strictly Positive Fragments of Modal Logics with Confluence. // Mathematics 2022, 10, 3701.

[9] Baader F., Brandt S., Lutz C. Pushing the EL envelope. // Proc. of the 19th Joint International Conference of Artificial Intelligence. — 2005.

[10] Baader F., Brandt S., Lutz C. Pushing the EL envelope. // LTCS-Report 05-01, Institute for Theoretical Computer Science, Dresden University of Technology. — 2005.

[11] Baader F., Brandt S., Suntisrivaraporn Is tractable reasoning in extensions of the description logic EL useful in practice?. // Proc. of the Methods for Modalities Workshop, Berlin, Germany. — 2005.

[12] Л. Д. Беклемишев, Схемы рефлексии и алгебры доказуемости в формальной арифметике, УМН, 60:2(362) (2005), 3-78; Russian Math. Surveys, 60:2 (2005), 197-268.

[13] Boolos G. The Logic of Provability. // Cambridge University Press.

_ 1993.

[14] Shapirovskiy I. PSPACE-decidability of Japaridze's polymodal logic. // Advances in Modal Logic. — 2008. — V. 7 (College Publications, London). - P. 289-304.

[15] E. V. Dashkov, 'On the positive fragment of the polymodal provability logic GLP', Matematicheskie Zametki, 91(3):331—346, 2012. English translation: Mathematical Notes, 91(3):318—333, 2012.

[16] L. D. Beklemishev, 'Positive provability logic for uniform reflection principles', Annals of Pure and Applied Logic, 165:82-105, 2014.

[17] Beklemishev L. D. On the reflection calculus with partial conservativity operators. // Lecture Notes in Computer Science. — 2017. - V. 10388. - P. 48-67.

[18] Beklemishev L. D. A universal algebra for the variable-free fragment of RCV. // Symposium on Logical Foundations of Computer Science, S. Artemov and A. Nerode, editors, Lecture Notes in Computer Science. — 2018.

[19] Pakhomov F., Walsh J. Reducing w-model reflection to iterated syntactic reflection. // Journal of Mathematical Logic. — 2023. — V. 23.

[20] Joosten J. J. Turing-Taylor expansions of arithmetical theories. // Stud. Logica 104, 1225-1243 (2015). https://doi.org/10.1007/sll225-016-9674-z

[21] Fernandez-Duque, Joosten J. J. Models of transfinite provability logic. // J. Symbol. Logic 78 (2), 543- 561 (2013).

[22] Hermo Reyes E., Joosten J. J. The logic of Turing progressions. // ArXiv: 1604.08705v2 [math.LO], 2017

[23] Borges A., Joosten J. J. Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic. / / https://doi.org/10.48550/arXiv.2312.14727

[24] L. D. Beklemishev, 'A note on strictly positive logics and word rewriting systems', In: s. odintsov, Larisa Maksimova,

editors, on Implication, Interpolation, and Definability. Outstanding Contributions to Logic series, v. 15, Springer, 2017, pp. 61-70. Preprint ArXiv: 1509.00666, 2015.

[25] L. L. Maksimova, V. V. Rybakov, 'Lattices of modal logics', Algebra i Logika, 13:105-122, 1974.

[26] W. J. Blok, 'Varieties of interior algebras'. Doctoral thesis, 1976.

[27] Scroggs, S. 'Extensions of the Lewis system S5', The Journal of Symbolic Logic, v. 16(2), 1951, pp. 112-120.

[28] A. chagrov, M. zakharyaschev, Modal Logic, Oxford University Press, 1997.

[29] Kruskal J. B. The theory of well quasi-ordering: a frequently discovered concept //J. Combin. Theory. — 1972. — Ser. A 13.

- P. 297-305.

[30] Nash-Williams C.St.J.A. On well-quasi-ordering finite trees. // Proceedings of Cambridge Phil.Soc 59. — 1963. — P. 833-835.

[31] Laver R. On Fraisse's order type conjecture. // Annals of Mathematics. - 1971. - V. 93. - P. 89-111.

[32] Dershowitz N., Manna Z. Proving termination with multiset orderings. // Lecture Notes in Computer Science. — 1979. — V. 71.

- P. 188-202.

[33] Egon Borger, Erich Graded, Yuri Gurevich. The Classical Decision Problem. - 1997.

[34] Simpson S. G. Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Baume. // Arch. Math. Logik Grundlag. — 1985. — V. 25 (1). P. 45 05.

[35] Gallier J. What's so special about Kruskal's theorem and the ordinal Го? A survey of some results in proof theory. // Annals of Pure and Applied Logic. - 1991. - V. 53. - P. 199-260.

[36] Carlucci L. Worms, gaps, and hydras. // Mathematical Logic Quarterly. - 2005. - V. 51 (4). - P. 342-350.

[37] Селиванов В. Л. Фактор-алгебра размеченных лесов по отношению h-эквивалентности // Алгебра и логика, 46:2 (2007), 217-243.

[38] Жуков А. В., Кудинов О. В., Селиванов В. Л. Определимость операций замыкания в h-предпорядке размеченных лесов // Алгебра и логика, 49:2 (2010), 181-194.

[39] Schuster P., Seisenherger М.. Weiermann A. (editors) Well-Quasi Orders in Computation, Logic, Language and Reasoning. // Trends in Logic_ _ 2020. - V. 53.

[40] Dzamonja M.. Schmitz S., Schnoebelen P. On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders. // Well-Quasi Orders in Computation, Logic, Language and Reasoning. — 2020. — Trends in Logic, V. 53 (Schuster P., Seisenberger M., Weiermann A. editors), Springer, Cham. — P. 29-54.

[41] D. H. J. de Jongh, Parikh R. Well-partial orderings and hierarchies. // Nederl. Akad. Wetensch. — 1977. — Proc. Ser. A 80 = Indag. Math. 39, N. 3. - P. 195-207.

[42] С. Каниськин. О позитивных фрагментах модальных логик. Дипломная работа, МГУ, 2013 http://lpcs.math.msu.su/ zolin/msc/

[43] Rathjen Л/.. J. Van der Meeren, Weiermann A. Well-partial-orderings and the big Vehlen number. // Archive for Mathematical Logic. - 2015. - V. 54. - P. 193-230.

Публикации автора по теме диссертации

[44] М. В. Святловский. Аксиоматизация и полиномиальная разрешимость строго позитивных фрагментов некоторых модальных логик // Матем. Заметки, 103:6 (2018), с. 884-901

[45] Svyatlovskiy, М. Modal Companions of К4+. Studia Lógica 110 (2022), с. 1327-1347

[46] М. В. Святловский. Стройный порядок на строго позитивных формулах // Труды МФТИ. Т.14, №3 (55), 129-138. 2022