КАРТОЧКА ПРОЕКТА ФУНДАМЕНТАЛЬНЫХ И ПОИСКОВЫХ НАУЧНЫХ ИССЛЕДОВАНИЙ,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ

Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.

ОБЩИЕ СВЕДЕНИЯ

Номер 16-11-10252

НазваниеАлгоритмические вопросы алгебры и логики

РуководительБеклемишев Лев Дмитриевич, Доктор физико-математических наук

Организация финансирования, регион Федеральное государственное бюджетное учреждение науки Математический институт им. В.А. Стеклова Российской академии наук, г Москва

Период выполнения при поддержке РНФ

2019 г. - 2020 г.

Конкурс Конкурс на продление сроков выполнения проектов, поддержанных грантами Российского научного фонда по приоритетному направлению деятельности Российского научного фонда «Проведение фундаментальных научных исследований и поисковых научных исследований отдельными научными группами».

Область знания, основной код классификатора 01 - Математика, информатика и науки о системах, 01-101 - Математическая логика и основания математики

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

Код ГРНТИ27.03.19

СтатусУспешно завершен

ИНФОРМАЦИЯ ИЗ ЗАЯВКИ

Аннотация
Настоящий проект посвящен исследованию задач математической логики и алгебры, рассматриваемых с точки зрения теории алгоритмов и теории сложности вычислений, и является продолжением одноименного проекта 2016-2018 годов (Проект 2016). На предыдущем этапе нам удалось получить ряд результатов, связанных с изучением общих вопросов теории доказательств и теории вычислимости, исследованием границ разрешимости и вычислительной сложности. В том числе был получен ряд положительных результатов, связанных с построением эффективных, практически реализуемых алгоритмов. Одновременно с этим, наши исследования в ходе Проекта-2016 позволили сформулировать ряд новых конкретных задач (возможность решения которых во многом обусловлена разработанными в Проекте 2016 методами). Как и раньше, эти задачи связаны с общими вопросами теории доказательств и теории вычислимости, исследованием границ разрешимости и построением эффективных алгоритмов. Ниже перечислены основные направления планируемых исследований. Исследование классов доказуемо тотальных вычислимых функций и спектров консервативности формальных теорий, включая расширения арифметики Пеано определениями истины. Характеризация класса доказуемо тотальных сигма-определимых функций теории множеств Крипке-Платека. Построение и исследование эффективных фрагментов модальных логик и других родственных логических языков. Изучение семантических и алгоритмических свойств пропозициональных модальных логик. Исследование проблемы выводимости для теорий первого порядка, основанных на неклассических логиках. Исследование порядковых и топологических свойств множеств на вещественной прямой и топологий на ординалах. Изучение логик (эквациональных теорий) алгебр Клини с делениями и стоящих в этой области открытых вопросов. Исследование сложности выводов для систем подстановок термов и слов. Предлагаемые исследования носят, в первую очередь, теоретический характер. Их решение имеет значение для различных областей математической логики и информатики. Одновременно с этим, предполагаемые в проекте результаты предоставляют теоретический базис для решения прикладных алгоритмических задач.

Ожидаемые результаты
В направлении исследований, связанном с теорией доказательств и ординальным анализом, мы исследуем два типа формальных теорий: предикативные расширения элементарной арифметики определениями истинности и теорию множеств Крипке-Платека и ее фрагменты. В обоих случаях мы планируем получить анализ следствий этих теорий определённых сложностных классов, характерных для рассматриваемых языков. В случае теорий с определениями истинности мы получим характеризацию классов доказуемо тотальных вычислимых функций. В случае теории Крипке-Платека планируется получить описание класса обобщенно вычислимых (сигма-определимых) функций этой теории. Исследования классов доказуемо тотальных вычислимых функций сильных формальных теорий являются одним из центральных вопросов теории доказательств. В этой области в ходе реализации проекта мы развиваем новые методы, которые представляются перспективными для решения трудных открытых вопросов. На основе этих методов, тесно связанных с использованием схем рефлексии и строго позитивных исчислений, мы ожидаем получить наиболее тонкий анализ предикативных теорий и их характаристических ординалов из известных в настоящее время, в частности, описание их арифметических следствий кванторной сложности П_n для каждого n>0 (спектров консервативности). Также мы ожидаем получить существенно новое обобщение этих методов, позволяющее дать описание класса доказуемо тотальных в теории множеств Крипке-Платека сигма-определимых функций. (Л.Д. Беклемишев, Е.А. Колмаков, Ф.Н. Пахомов) Планируется развить общий алгебраический взгляд на теоремы Де Йонга и теоремы Соловея, их равномерные варианты, теоремы Шаврукова, а также недавние результаты Савельева и Шапировского, как на результаты о погружении модальных алгебр в алгебры классических теорий первого порядка или некоторых “метатеорий”. Ожидается, что на основе этого взгляда возникнет новое взаимодействие классической теории моделей первого порядка с теорией модальных логик, и будут построены новые разрешимые фрагменты теорий первого порядка (ср. результаты Ван Бентема о разрешимости “охраняемых фрагментов”). Одной из классических семантик для модальной логики является семантика Крипке. Для модальных логик первого порядка (модальных логик предикатов) вопросы полноты и неполноты относительно семантики Крипке сложнее, чем для пропозиционального случая: в частности, очень редко встречаются канонические логики, полные относительно своей канонической шкалы (построенной из непротиворечивых теорий со свойством Хенкина). Продолжая исследования Проекта-2016, мы ожидаем построить новые серии модальных логик предикатов, полных и неполных относительно семантики Крипке. Также ожидаются новые результаты о симплициальной семантике предикатных модальных логик. (В.Б. Шехтман) Будут изучаться конечно порождённые свободные модальные алгебры (алгебры Линденбаума в языке с конечным числом переменных). Эти алгебры были описаны В.Б. Шехтманом в конце 1970х годов для одномодального транзитивного случая. Полученный в Проекте 2016 Шапировским и Шехтманом семантический критерий локальной табличности позволяет получать такие описания для нетранзитивного одномодального и для полимодального случаев. Будет развит метод фильтраций для обобщенных и порядковых сумм шкал Крипке, что позволит получить новые результаты о разрешимости полимодальных логик. (И.Б. Шапировский) В последний год Проекта 2016 было рассмотрено расширение языка первого порядка квантором выполнимости предложения в надмоделях. Было доказано, что этот язык удовлетворяет теореме Левенгейма-Сколема о понижении мощности. Мы предполагаем выяснить, как этот достаточно неожиданный положительный результат может быть распространён на случай других естественных теоретико-модельных отношений. В целом, изучение свойств языков с кванторами такого рода – обширная и перспективная задача. (Д.И. Савельев, И.Б. Шапировский) Операция итерации (“звёздочка”), введённая Клини (1951) для представления событий в нервных сетях, играет важную роль в теоретической информатике. С точки зрения математической логики, интерес представляют эквациональные теории классов структур с итерацией Клини, т.е. множества всех общезначимых в них высказываний вида u=v, где u и v – термы (выражения). Для алгебр Клини без операций деления это известная задача о проверке тождеств регулярных выражений, она алгоритмически разрешима и является PSPACE-полной (Кроб 1990, Козен 1991). Аналогичные вопросы для алгебр и решёток Клини с делениями оставались открытыми (Козен 1994, Бушковский 2007). Мы собираемся доказать алгоритмическую неразрешимость и получить точную характеризацию классов алгоритмической сложности эквациональные теорий алгебр и решёток Клини с делениями с различными наборами операций. Также планируется получить новые результаты о полноте и неполноте этих теорий относительно интерпретаций на формальных языках (в частности, регулярных) и на алгебре бинарных отношений. (С.Л. Кузнецов) Строго позитивные модальные логики – это семейство модальных логик в ограниченном языке. Эти логики, с одной стороны, сохраняют достаточно выразительной силы (для применения как внутри математической логики, например при исследовании вопросов доказуемости, так и для внешних приложений в базах данных, медицине и т.д.), с другой – допускают эффективное решение основных связанных с ними алгоритмических задач. Для модальных логик в полном языке эти задачи в большинстве случаев обладают высокой алгоритмической сложностью, например, PSPACE-полны. Ожидается для некоторых фрагментов строго позитивных модальных логик доказать разрешимость на логарифмической памяти задачи проверки следования одной формулы из другой, а для некоторых других фрагментов – доказать L-полноту этой задачи. (В.В. Подольский) Вопросы о функции сложности вывода в системах переписывания слов, изучавшиеся в ходе Проекта 2016, тесно связаны с задачами, которые сейчас широко изучаются математиками в разных странах (Австрия, Германия, Нидерланды, Япония). Этот интерес обусловлен современными вопросами математической логики, теоретической информатики и алгебры. В проекте предполагается исследовать системы переписывания слов, сохраняющие их длину. В частности, особое внимание будет уделено системам, для которых функция сложности выводов ограничена сверху квадратичной и линейной. Ожидается установить существование сохраняющих длину систем переписывания слов с функцией сложности, асимптотически лежащей строго между n log(n) и n^2. (А.Л. Таламбуца) В части проекта, посвящённом исследованию свойств групп, заданных определяющими соотношениями, будут рассматриваться так называемые n-крученые группы, которые являются обобщениями периодических групп. А именно, n-крученой группой называется группа, заданная системой периодических соотношений степени n, в которой каждый элемент либо имеет порядок n, либо имеет бесконечный порядок. Будут изучаться вопросы об том, какие свойства периодических групп также могут быть доказаны и для n-крученых групп. В частности, предполагается описать структуру централизаторов этих групп, а также описать группы автоморфизмов этих групп. (С.И. Адян) Наши исследования по проекту 2019 носят, в первую очередь, теоретический характер. Они имеют значение для различных областей математической логики и приложений в информатике. Некоторые предполагаемые в проекте результаты, в частности связанные с теорией сложности вычислений и строго позитивными исчислениями, могут предоставлять интерес для решения прикладных алгоритмических задач. Все запланированные результаты соответствуют мировому уровню исследований.

ОТЧЁТНЫЕ МАТЕРИАЛЫ

Аннотация результатов, полученных в 2019 году
Л.Д. Беклемишев, Ф.Н. Пахомов и Е.А. Колмаков исследовали расширения элементарной арифметики итерированными определениями истинности, удовлетворяющими аксиомам Тарского. Рассматривались схемы рефлексии для таких теорий и связанные с ними алгебры рефлексии с точки зрения строго позитивной модальной логики. На основе этих методов получены результаты о консервативности и результаты, характеризующие теоретико-доказательственные ординалы таких теорий, соответствующие произвольному уровню гиперарифметической иерархии. Эти теории также тесно связаны со стандартными предикативными фрагментами арифметики второго порядка, что дает альтернативный метод анализа теорий этого класса. В совместной работе А. Энаята и Ф.Н. Пахомова было доказано, что теория PA+CT+DC (PA расширенная предикатом истинности удовлетворяющим композиционным аксиомам и коммутирующим с дизъюнкциями произвольного конечного размера) доказывает аксиому индукции для ограниченных формул с предикатом истинности. Отсюда следует, что теория PA+CT+DC не является консервативным расширением PA. Ф.Н. Пахомов разработал аналог формула Шмерля для теорий в теоретико-множественном языке. Была получена характеризация Pi_2 следствий теории множеств Крипке-Платека c бесконечностью в терминах итерации схемы Pi_2 рефлексии вдоль вполне упорядоченного класса epsilon_{On+1} (первое epsilon-число после порядкового типа класса ординалов). Здесь рефлексия была итерирована над теорией KPomega_0, которая является вариантом теории множеств Крипке-Платека в котором схема индукции по принадлежности ограничена на Delta_0-формулы и явно добавлена определяющая аксиома для функции ранга rho: V -> On. В.Б. Шехтманом были получены новые результаты о полноте и неполноте для широких классов предикатных модальных логик. И.Б. Шапировским было продолжено исследование модальных логик сумм шкал Крипке. В частности, им было показано, что во многих случаях проблема модальной выполнимости на суммах сводима по Тьюрингу с использованием полиномиальной памяти к проблеме выполнимости на слагаемых. Для случая логики конечной модальной глубины, И.Б. Шапировским была получена равномерная верхняя оценка размера конечно порожденной свободной алгебры. Д.И. Савельевым вычислены устойчивые модальные теории для следующих теоретико-модельных отношений: отношения «быть подмоделью» на классах: (а) всех плотных линейно упорядоченных множеств без крайних точек, (б) всех линейно упорядоченных множеств (в предположении континуум гипотезы, этот результат был получен в рамках настоящего проекта в 2018) (в) всех частично упорядоченных множеств, (г) всех свободных групп. Для данного предложения языка первого порядка $L_{\kappa,\kappa}$, где $\kappa$ есть либо счётный, либо определённый большой кардинал, Д.И. Савельевым установлены синтаксические и семантические критерии того, что её выполнимость в некоторой подмодели выражается в этом же языке. Д.И. Савельевым также показано, что наименьший кардинал, для которого аксиома Баумгартнера нарушается, не превосходит наименьшую мощность множества действительных чисел, не являющегося Q-множеством. С.Л. Кузнецов исследовал теории алгебраических структур с операцией итерации (“звёздочка Клини”). Звёздочка Клини является одной из наиболее интересных алгебраических операций, используемых в теоретической информатике. Из-за рекурсивной природы этой операции включающие её алгебраические логики (эквациональные теории), будучи чисто пропозициональными, приобретают некоторые особенности, обычно свойственные более богатым теориям, таким как арифметика Пеано. В частности, для алгебр Клини с операциями деления (введены у Пратта в 1991 году как "action algebras") имеет место своеобразный аналог теоремы Гёделя о неполноте: полная теория, задаваемая с помощью омега-правило, оказывается сильнее любой теории, где итерация аксиоматизируется с помощью принципов индукции. Это следует из соображений алгоритмической сложности: теория с омега-правилом не является рекурсивно перечислимой (Бушковский 2007). Вопрос о сложности теорий с индуктивной аксиоматизацией оставался открытым; в рамках проекта получено его решение: эти теории алгоритмически неразрешимы. В. В. Подольский исследовал алгоритмическую задачу проверки следования одной формулы из другой в строго позитивных фрагментах некоторых полимодальных логик. Было установлено, что для некоторых логик эти задачи полны в сложностном классе L задач, разрешимых на логарифмической памяти. В. В. Подольский также исследовал алгоритмическую задачу вычисления плотных булевых линейных операторов над полугруппами. Была показана сверхлинейная нижняя оценка для случая сильно некоммутативных полугрупп.

Публикации

1. Куликов А.С., Михайлин И., Мохов А., Подольский В. Complexity of linear operators 30th International Symposium on Algorithms and Computation (ISAAC 2019), - (год публикации - 2019) https://doi.org/10.4230/LIPIcs.ISAAC.2019.17

2. Савельев Д.И. On first-order expressibility of satisfiability in submodels Lecture Notes in Computer Science, WoLLIC 2019: Logic, Language, Information and Computation, Lect. Notes Comput. Sci. vol. 11541, pp.610–618, Springer, 2019 (год публикации - 2019) https://doi.org/10.1007/978-3-662-59533-6_35

3. Савельев Д.И., Шапировский И.Б. On Modal Logics of Model-Theoretic Relations Studia Logica, Stud Logica (2019) doi:10.1007/s11225-019-09885-y (год публикации - 2019) https://doi.org/10.1007/s11225-019-09885-y

4. Шапировский И.Б. Modal logics of finite direct powers of ω have the finite model property Lecture Notes in Computer Science, WoLLIC 2019: Logic, Language, Information and Computation, Lect. Notes Comput. Sci. vol. 11541, pp. 610-618, Springer, 2019 (год публикации - 2019) https://doi.org/10.1007/978-3-662-59533-6_37

5. Энаят А., Пахомов Ф. Truth, disjunction, and induction. Archive for Mathematical Logic, - (год публикации - 2019) https://doi.org/10.1007/s00153-018-0657-9

Аннотация результатов, полученных в 2020 году
Для алгебр рефлексии теорий итерированных определений истинности была сформулирована новая конструкция «автономного замыкания» данной алгебры рефлексии. Было установлено, что с помощью операции автономного замыкания порождается система конструктивных ординальных обозначений для ординала Фефермана-Шютте (обычно обозначаемого Г_0), представляющего собой границу ординалов предикативных теорий. (Л.Д. Беклемишев, Е.А. Колмаков) Разработан аналог иерархии Леба - Вейнера быстро-растущих вычислимых функций для случая сигма-определимых функций из ординалов в ординалы. Получена классификация Pi_1-следствий теории множеств Крипке-Платека в терминах итерированных схем рефлексии. (Ф. Н. Пахомов) Получены результаты о свойствах фрагментов предикатных модальных логик с одной переменной. Для ряда таких фрагментов построена аксиоматика, доказана финитная аппроксимируемость и алгоритмическая разрешимость. (В.Б. Шехтман) Были усилены полученные ранее результаты об алгоритмической разрешимости и сложности пропозициональных модальных логик. Были получены новые результаты о локальной табличности, финитной аппроксимируемости и фильтруемости модальных логик. (И.Б. Шапировский) Найдены логики смешанных произведений логик для произвольных хорновых направленных логик. Смешанное произведение модальных логик является логикой структур специального вида, а именно произведений окрестностных шкал логики L1 и шкал Крипке логики L2. Шкалы Крипке представляют собой дискретные структуры, а именно направленные графы с петлями, тогда как окрестностные шкалы – непрерывные структуры, частным случаем которых являются топологические пространства. (А.В. Кудинов) Продолжены исследования алгебраических логик с итерацией Клини. Получены результаты о неразрешимости и алгоримтической сложности, уточняющие результат 2019 г. о сложности эквациональной теории алгебр Клини с делениями. Исследовались и семантические вопросы, связанные с данными логиками. Одна из естественных интерпретаций теорий с делениями и итерацией – это интерпретация на алгебрах бинарных отношений, или реляционная семантика. Интуитивно она соответствует пониманию формул данной логики как классов действий (переходов) в некоторой недетерминированной вычислительной системе. В общем случае, однако, имеет место неполнота теорий с делениями и итерацией Клини относительно реляционной семантики, из-за невыводимости законов дистрибутивности и их следствий. В рамках проекта была доказана полнота для фрагмента без дизъюнкции (объединения) и с ограничением на использование итерации – её можно использовать только в знаменателях делений. При этом сложность и выразительные возможности данного фрагмента не уступают таковым для всего исчисления. (С.Л. Кузнецов) Исследовалась алгоритмическая сложность некоторых вариантов задач достижимости в специальных классах графов и задач проверки наличия гомоморфизма между деревьями. Для ряда рассмотренных задач была установлена полнота в сложностном классе L относительно AC^0 и NC^1 сведений. Полученные результаты применены для исследования сложности задач проверки следования одной формулы из другой в строго позитивных фрагментах полимодальных логик. (В.В. Подольский) Получен ответ на вопрос о существовании односторонних систем подстановок слов, функция сложности выводов в которых находится асимптотически строго между линейной функцией и функцией n log (n). Было доказано, что существует бесконечная серия таких систем, сложность каждой из которых асимптотически отличается от каждой другой. (А.Л. Таламбуца)

Публикации

1. Кикоть С. П., Шапировский И. Б., Золин Е. Е. Modal Logics with Transitive Closure: Completeness, Decidability, Filtration Advances in Modal Logic, College publications, 2020, т. 13, стр. 369–388 (год публикации - 2020)

2. Кузнецов С.Л. Complexity of the infinitary Lambek calculus with Kleene star The Review of Symbolic Logic, FirstView (год публикации - 2020) https://doi.org/10.1017/S1755020320000209

3. Кузнецов С.Л., Рыжкова Н.С. Ограниченный фрагмент исчисления Ламбека с операциями итерации и пересечения Алгебра и логика, 59:2 (2020), 190-214 (год публикации - 2020) https://doi.org/10.1007/s10469-020-09586-9

4. Савельев, Д. И. Hindman's finite sums theorem and its application to topologizations of algebras Записки научных семинаров ПОМИ РАН, - (год публикации - 2020)

5. Таламбуца А. Л. On Subquadratic Derivational Complexity of Semi-Thue Systems CSR 2020: Computer Science – Theory and Applications, 15th International Computer Science Symposium in Russia, Yekaterinburg, Russian Federation, 29 June 2020 - 3 July 2020, Lecture Notes in Comput. Sci., 12159, Springer, 2020, стр. 379–392 (год публикации - 2020) https://doi.org/10.1007/978-3-030-50026-9_28

Возможность практического использования результатов
не указано