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

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

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

Номер 21-11-00318

НазваниеПроблемы вычислимости, доказуемости и полноты в логике и алгебре

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

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

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

2021 г. - 2023 г.

Конкурс№55 - Конкурс 2021 года «Проведение фундаментальных научных исследований и поисковых научных исследований отдельными научными группами».

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

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

Код ГРНТИ27.03.19

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

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

Аннотация
Проект связывает воедино ряд направлений исследований, проводимых в отделе математической логики МИАН и в группе логиков из ИППИ РАН. В проекте представлены исследования по комбинаторной и геометрической теории групп, теории сложности вычислений, исследования выразительных возможностей логических языков, в том числе применяемых в базах данных. С другой стороны, алгебраические методы применяются для изучения вычислительных моделей (алгебры Клини) и формальных моделей доказуемости (алгебры рефлексии). С алгоритмической точки зрения и с точки зрения семантики исследуется ряд важных классов неклассических логик, в том числе модальные логики и вероятностные логики. Важную роль в проекте также играет исследование новых типов моделей для предикатных модальных логик, обобщающих модели Крипке. Ниже перечислены основные задачи, рассматриваемые в проекте. Исследование групп, заданных множеством периодических определяющих соотношений одного и того же достаточно большого периода. Этот класс групп является естественным обобщением свободных бернсайдовых групп, занимающих важное место в комбинаторной теории групп. Исследование сложности задачи поиска ответов на запросы к базам данных, снабженным логической теорией. Исследование логических теорий для алгебраических структур с итерацией Клини, прежде всего с точки зрения их алгоритмической сложности. Исследование определимости в разрешимых арифметических теориях, в частности в арифметике Пресбургера (полной теории натурального ряда с операцией сложения) и в её обогащении — арифметике Бюхи. Для арифметики Бюхи будет исследоваться гипотеза Виссера об интерпретациях таких теорий в себе. Также предполагается исследовать вопрос об описании линейных порядков, интерпретируемых в арифметике Пресбургера. Применение алгебраических методов при исследовании формальных теорий, важных с точки зрения оснований математики (расширений формальной арифметики первого порядка, подсистем формальной арифметики второго порядка). На основе методов, тесно связанных с использованием схем рефлексии и соответствующих полурешеток с монотонными операторами, мы ожидаем получить описание характеристических ординалов для таких теорий и описание их арифметических следствий фиксированной логической сложности (и спектров консервативности). В частности, с этой точки зрения планируется исследовать автономные прогрессии Тьюринга-Фефермана и некоторые другие теории. Исследование вероятностных логик, то есть формальных языков, в основе семантики которых лежат вероятностные пространства (конечно-аддитивные или счетно-аддитивные). В рамках проекта планируется изучить с алгоритмической точки зрения теории некоторых важных классов конечно-аддитивных вероятностных пространств. Исследование алгебраической и окрестностной семантик различных логик, допускающих нефундированные доказательства и доказательства с омега-правилом, в частности для логик с операторами взятия неподвижных точек и логик доказуемости. Построение и исследование эффективных фрагментов модальных логик и других родственных логических языков. Изучение семантических и алгоритмических свойств предикатных модальных логик. Изучение топологической семантики модальных логик.

Ожидаемые результаты
Исследование периодических групп — важное направление теории групп. Несмотря на простоту определения, вопросы о свойствах и структуре этих групп являются весьма трудными. Одна из главных работ в этом направлении — результат Новикова-Адяна о бесконечности свободных бернсайдовых групп достаточно большого нечетного периода. Развитие этих методов позволяет решать трудные вопросы теории групп путем построения групп с необычными свойствами. Планируется рассматривать класс групп, заданных множеством периодических соотношений одного и того же достаточно большого четного периода. Для таких групп при некоторых естественных ограничениях предполагается установить бесконечность и доказать ряд других свойств (в частности, получить некоторое описание выводимых соотношений и доказать разрешимость проблем равенства и сопряженности). Тем самым будет получено существенное продвижение в изучении этого естественного класса групп, обобщающего свободные бернсайдовы. Полученные результаты могут быть использованы в последующих работах для построения примеров групп с необычными свойствами. Задача поиска ответов на запросы к базам данных, снабженным логическими теориями, стала особенно актуальной начиная с 90-х годов. В общем виде задача остается очень сложной с вычислительной точки зрения, но в ряде важных частных случаев ее сложность оказывается не слишком высокой. Эти случаи оказываются полезными для практического применения: даже довольно слабые теории помогают существенно упростить работу с базой данных. Мы планируем получить продвижения в этой задаче для некоторых принципиально важных теорий, в частности для теории, состоящей из одной аксиомы о покрытии. Алгебры Клини имеют большое значение в теоретической информатике. В частности, они используются при моделировании вычислительных процессов и для описания формальных языков. Планируется доказать алгоритмическую неразрешимость и установить место в арифметической/аналитической иерархии для хорновой теории коммутативных *-непрерывных алгебр Клини и ее фрагментов и для эквациональной теории решеток Клини с правилом сокращения; для эквациональной теории всех решеток Клини с ограничениями на использование операции пересечения планируется доказать алгоритмическую разрешимость и принадлежность классу PSPACE. Значимость результатов о неразрешимости в том, что они устанавливают границы применимости логических теорий с итерацией Клини. Исследование разрешимых фрагментов арифметики Пеано, среди которых наиболее известна арифметика Пресбургера, является классической областью математической логики. Расширяющие ее арифметики Бюхи, связанные с распознаваемостью множеств натуральных чисел конечными автоматами, являются интересным объектом исследования. В рамках проекта планируется решение двух конкретных задач. Во-первых, планируется построить полное описание линейных порядков, интерпретируемых в арифметике Пресбургера m-мерно для каждого натурального m. Во-вторых, планируется доказать, что любая интерпретация арифметики Бюхи в своей стандартной модели изоморфна тождественной интерпретации. Это даст положительное решение гипотезы Виссера для данного семейства теорий. Применение методов, связанных с алгебрами рефлексии, в области теории доказательств имеет ряд преимуществ по сравнению с традиционными методами анализа формальных систем (такими как использование методов устранения сечения в инфинитарной логике). В частности, такие методы позволяют получить результаты в большей степени общности и единообразно, а также приводят к наиболее тонким классификациям следствий рассматриваемых теорий, выражаемых формулами определенной логической сложности (вычислению спектров консервативности теорий). В данном проекте эти методы будут применены к исследованию нескольких интересных и важных классов расширений арифметики Пеано: прогрессий типа Тьюринга-Фефермана, в том числе так называемых “автономных” прогрессий, введенных для анализа предикативного доказательства Крайзелем и Феферманом. Мы планируем упростить теорию Крайзеля-Фефермана и одновременно получить ее обобщение на языке алгебр рефлексии. Также мы планируем исследовать с аналогичной точки зрения расширения арифметики Пеано определениями истинности, удовлетворяющие композициональным аксиомам. Формальные языки с вероятностной семантикой занимают важное место в современной математической логике и теоретической информатике. Планируется оценить алгоритмическую сложность теорий некоторых естественных классов конечно-аддитивных вероятностных пространств. В последнее время возрос интерес к логическим системам, включающим рекурсивно определяемые операции. К ним относятся уже упомянутые логики алгебр Клини и формальная арифметика. Еще одним классом таких логик являются модальные логики с операторами транзитивного замыкания, модальностью общего знания и другими возможными операциями. Мы определим конструкцию канонической окрестностной шкалы для модальной логики с оператором транзитивного замыкания и, как следствие, получим результат о глобальной окрестностной полноте логики транзитивного замыкания, расширенной выводами с омега-правилом. Используя конструкцию канонической окрестностной шкалы, мы получим метод семантического доказательства теорем о реализации для таких логик, как логика транзитивного замыкания, логика с модальностью общего знания и др. Модальная логика является активно развивающейся областью на стыке современной математической логики и информатики. Важной задачей современной математической логики (особенно с точки зрения ее приложений) является поиск логических исчислений, адекватно описывающих конкретные математические структуры и классы структур. Для этой цели в последние время используются модальные логики. Одной из классических семантик в модальной логике является семантика Крипке. Однако для модальных логик предикатов первого порядка вопросы полноты и неполноты относительно семантики Крипке гораздо менее изучены, чем для пропозиционального случая. В проекте, в частности, предполагается исследовать проблему полноты для минимальных предикатных расширений пропозициональных логик. Для неполных логик планируется дать, насколько возможно, эффективные описания их пополнений. Кроме семантики Крипке, проблема полноты модальных предикатных логик будет изучаться для других, более общих семантик. В математике и других областях, в которых используются математические модели, часто возникает необходимость рассматривать многомерные структуры. Многомерные полимодальные логики возникают как логики классов шкал, являющихся произведениями шкал соответствующих одномодальных логик. При этом многомерные логики, как правило, оказываются намного труднее для изучения и интереснее, чем одномерные. Планируется найти аксиоматизацию произведения модальных логик, содержащих аксиому МакКинси, в частности такие произведения как S4.1 на S4 и, в общем случае, произведения вида K4.1 на L для различных логик L. В силу теоремы Геделя о неполноте, финитные аксиоматизации достаточно богатых теорий, таких как формальная арифметика и теория множеств, не могут быть полными. В случае формальной арифметики, ее можно сделать полной посредством добавления омега-правила. В связи с этим представляется естественной задача построения аналогичных правил для теории множеств. В рамках проекта предполагается получить результаты о синтаксической и семантической полноте исчислений для теории множеств с правилами такого типа, в частности вывести полную теорию модели L, т.е. наименьшей внутренней модели теории множеств, состоящей из конструктивных по Геделю множеств. Также планируется показать, что аналогичные результаты могут быть получены для более сильных логик. Исследование периодических групп — важное направление теории групп. Несмотря на простоту определения, вопросы о свойствах и структуре этих групп являются весьма трудными. Одна из главных работ в этом направлении — результат Новикова-Адяна о бесконечности свободных бернсайдовых групп достаточно большого нечетного периода. Развитие этих методов позволяет решать трудные вопросы теории групп путем построения групп с необычными свойствами. Планируется рассматривать класс групп, заданных множеством периодических соотношений одного и того же достаточно большого четного периода. Для таких групп при некоторых естественных ограничениях предполагается установить бесконечность и доказать ряд других свойств (в частности, получить некоторое описание выводимых соотношений и доказать разрешимость проблем равенства и сопряженности). Тем самым будет получено существенное продвижение в изучении этого естественного класса групп, обобщающего свободные бернсайдовы. Полученные результаты могут быть использованы в последующих работах для построения примеров групп с необычными свойствами. Задача поиска ответов на запросы к базам данных, снабженным логическими теориями, стала особенно актуальной начиная с 90-х годов. В общем виде задача остается очень сложной с вычислительной точки зрения, но в ряде важных частных случаев ее сложность оказывается не слишком высокой. Эти случаи оказываются полезными для практического применения: даже довольно слабые теории помогают существенно упростить работу с базой данных. Мы планируем получить продвижения в этой задаче для некоторых принципиально важных теорий, в частности для теории, состоящей из одной аксиомы о покрытии. Алгебры Клини имеют большое значение в теоретической информатике. В частности, они используются при моделировании вычислительных процессов и для описания формальных языков. Планируется доказать алгоритмическую неразрешимость и установить место в арифметической/аналитической иерархии для хорновой теории коммутативных *-непрерывных алгебр Клини и ее фрагментов и для эквациональной теории решеток Клини с правилом сокращения; для эквациональной теории всех решеток Клини с ограничениями на использование операции пересечения планируется доказать алгоритмическую разрешимость и принадлежность классу PSPACE. Значимость результатов о неразрешимости в том, что они устанавливают границы применимости логических теорий с итерацией Клини. Исследование разрешимых фрагментов арифметики Пеано, среди которых наиболее известна арифметика Пресбургера, является классической областью математической логики. Расширяющие ее арифметики Бюхи, связанные с распознаваемостью множеств натуральных чисел конечными автоматами, являются интересным объектом исследования. В рамках проекта планируется решение двух конкретных задач. Во-первых, планируется построить полное описание линейных порядков, интерпретируемых в арифметике Пресбургера m-мерно для каждого натурального m. Во-вторых, планируется доказать, что любая интерпретация арифметики Бюхи в своей стандартной модели изоморфна тождественной интерпретации. Это даст положительное решение гипотезы Виссера для данного семейства теорий. Применение методов, связанных с алгебрами рефлексии, в области теории доказательств имеет ряд преимуществ по сравнению с традиционными методами анализа формальных систем (такими как использование методов устранения сечения в инфинитарной логике). В частности, такие методы позволяют получить результаты в большей степени общности и единообразно, а также приводят к наиболее тонким классификациям следствий рассматриваемых теорий, выражаемых формулами определенной логической сложности (вычислению спектров консервативности теорий). В данном проекте эти методы будут применены к исследованию нескольких интересных и важных классов расширений арифметики Пеано: прогрессий типа Тьюринга-Фефермана, в том числе так называемых “автономных” прогрессий, введенных для анализа предикативного доказательства Крайзелем и Феферманом. Мы планируем упростить теорию Крайзеля-Фефермана и одновременно получить ее обобщение на языке алгебр рефлексии. Также мы планируем исследовать с аналогичной точки зрения расширения арифметики Пеано определениями истинности, удовлетворяющие композициональным аксиомам. Формальные языки с вероятностной семантикой занимают важное место в современной математической логике и теоретической информатике. Планируется оценить алгоритмическую сложность теорий некоторых естественных классов конечно-аддитивных вероятностных пространств. В последнее время возрос интерес к логическим системам, включающим рекурсивно определяемые операции. К ним относятся уже упомянутые логики алгебр Клини и формальная арифметика. Еще одним классом таких логик являются модальные логики с операторами транзитивного замыкания, модальностью общего знания и другими возможными операциями. Мы определим конструкцию канонической окрестностной шкалы для модальной логики с оператором транзитивного замыкания и, как следствие, получим результат о глобальной окрестностной полноте логики транзитивного замыкания, расширенной выводами с омега-правилом. Используя конструкцию канонической окрестностной шкалы, мы получим метод семантического доказательства теорем о реализации для таких логик, как логика транзитивного замыкания, логика с модальностью общего знания и др. Модальная логика является активно развивающейся областью на стыке современной математической логики и информатики. Важной задачей современной математической логики (особенно с точки зрения ее приложений) является поиск логических исчислений, адекватно описывающих конкретные математические структуры и классы структур. Для этой цели в последние время используются модальные логики. Одной из классических семантик в модальной логике является семантика Крипке. Однако для модальных логик предикатов первого порядка вопросы полноты и неполноты относительно семантики Крипке гораздо менее изучены, чем для пропозиционального случая. В проекте, в частности, предполагается исследовать проблему полноты для минимальных предикатных расширений пропозициональных логик. Для неполных логик планируется дать, насколько возможно, эффективные описания их пополнений. Кроме семантики Крипке, проблема полноты модальных предикатных логик будет изучаться для других, более общих семантик. В математике и других областях, в которых используются математические модели, часто возникает необходимость рассматривать многомерные структуры. Многомерные полимодальные логики возникают как логики классов шкал, являющихся произведениями шкал соответствующих одномодальных логик. При этом многомерные логики, как правило, оказываются намного труднее для изучения и интереснее, чем одномерные. Планируется найти аксиоматизацию произведения модальных логик, содержащих аксиому МакКинси, в частности такие произведения как S4.1 на S4 и, в общем случае, произведения вида K4.1 на L для различных логик L. В силу теоремы Геделя о неполноте, финитные аксиоматизации достаточно богатых теорий, таких как формальная арифметика и теория множеств, не могут быть полными. В случае формальной арифметики, ее можно сделать полной посредством добавления омега-правила. В связи с этим представляется естественной задача построения аналогичных правил для теории множеств. В рамках проекта предполагается получить результаты о синтаксической и семантической полноте исчислений для теории множеств с правилами такого типа, в частности вывести полную теорию модели L, т.е. наименьшей внутренней модели теории множеств, состоящей из конструктивных по Геделю множеств. Также планируется показать, что аналогичные результаты могут быть получены для более сильных логик.

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

Аннотация результатов, полученных в 2021 году
Исследовалась задача поиска ответа на фиксированный запрос к базе данных в присутствии аксиомы покрытия. Доказано, что для ациклических ориентированных запросов вопрос о том, разрешима ли указанная задача в классе AC^0, является 2EXPTIME-трудным. Арифметика Пресбургера – элементарная теория натуральных чисел со сложением (N,+). Эта теория полна и разрешима. А. Виссер предложил исследовать интерпретации самой арифметики Пресбургера и её фрагментов в (N,+). Мы рассматриваем интерпретации линейных порядков в арифметике Пресбургера. Удалось установить, что всякий порядок, интерпретируемый в (N,+), изоморфен сужению подпорядка Z^m на некоторое определимое множество D, причём этот изоморфизм задаётся формулой арифметики Пресбургера. Более того, аналогичное свойство выполняется для однородно (общей формулой арифметики Пресбургера) заданных семейств линейных порядков (L_p, <_p). Исследованы автономные прогрессии схем рефлексии над теориями итерированных определений истинности, соответствующей идее предикативных расширений данной теории по Крайзелю-Феферману. Также сформулированы соответствующие им строго позитивные модальные исчисления. Алгебры Клини – это известный класс алгебраических систем, широко используемых в теоретической информатике для описания формальных языков и моделирования работы вычислительных систем. Наиболее важной операцией в этих алгебр, является итерация (“звёздочка”) Клини, означающая повторение некоторого слова или действия некоторое конечное, но заранее не определённое число раз. В специальном случае *-непрерывных алгебр Клини, для обоснования некоторого утверждения об итерации нужно проверить его для каждого конкретного количества повторений, что приводит к высокому уровню алгоритмической сложности соответствующих логических теорий. В рамках проекта вопросы сложности рассматривались в применении к коммутативному случаю. Важность этого случая основана на следующем наблюдении Пратта (1991): коммутативные структуры с итерацией подходят для описания параллельных процессов, в то время как некоммутативные соответствуют последовательному выполнению действий. В рамках проекта в 2021 г. установлена алгоритмическая сложность следования, во всех *-непрерывных коммутативных алгебрах Клини, некоторого равенства из множества гипотез, не содержащих операцию итерации. В области модальных логик с неподвижными точками, в центре нашего внимания находилась широко известная среди специалистов эпистемическая модальная логика общего знания S4CI. Мы рассмотрели расширение S4CI, добавив к задающему данную логику аксиоматическому исчислению омега-правило, и изучили алгебраическую и топологическую семантики получившейся системы. Мы доказали, что данная система полна относительно её топологической семантики в случае глобального отношения семантического следования. Мы также получили результат о сильной топологической полноте логики S4CI в случае локального отношения семантического следования. Найдена аксиоматизация топологического произведения модальных логик S4.1 на S4, т.е. найдена логика битопологических произведений всех топологических пространств, в которых первый компонент является слабо разреженным. Полные теории моделей, т. е. совокупности истинных в данных моделях предложений данного языка, являются классическим предметом изучения в математической логике. В частности, такова полная теория первого порядка стандартной модели арифметики, часто называемая истинной арифметикой TA. В силу классических результатов Гёделя, TA не выводима из арифметики Пеано PA (и её рекурсивных расширений) в обычном исчислении предикатов; однако, TA можно вывести из PA, усилив дедуктивный аппарат омега-правилом. В связи с этим представляется естественной задача построения класса правил такого типа, позволяющих выводить полные теории из их простых фрагментов, например, полные теории данных моделей из их диаграмм; особенный интерес представляет случай моделей теории множеств и её фрагментов (по существу, гёделевых теорий). Целью работы по данному направлению является построение класса таких правил вывода, вообще говоря, инфинитарных, которые позволяют получать полные теории различных моделей первого порядка. Фактически, описываемые в таких исчислениях модели являются поточечно определимыми в подходящем языке (подобно стандартной модели арифметики). Такого рода правила мы называем правилами ограничения ввиду того, что они специфическим образом ограничивают класс описываемых моделей. Были получены следующие результаты: теорема о синтаксической полноте исчисления с правилом S-ограничения для данного множества S термов; теорема о семантической полноте этого исчисления; а также доказательство равносильности правил ограничения, задаваемых множеством термов и множеством формул единственности.

Публикации

Аннотация результатов, полученных в 2022 году
Был разработан вариант так называемой итерированной теории малых сокращений, применимый к широкому классу групп, заданных с помощью порождающих и определяющих соотношений бернсайдовского типа. В частности, доказано, что такими группами являются свободные берснсайдовы группы нечетного периода, большего 2000. Исследовалась алгоритмическая сложность задачи поиска ответа на конъюнктивные запросы к базам данных, снабженным аксиомой покрытия. Установление сложности этой задачи для произвольных конъюнктивных запросов является сложной задачей. В рамках проекта показано, что эта задача нетривиальна даже для случая древовидных запросов: даже определить по запросу, разрешима ли задача ответа на запрос в классе AC^0 (что эквивалентно переписываемости запроса в виде формулы логики первого порядка), является PSPACE-трудной. Было продолжено исследование алгоритмических вопросов для коммутативных алгебр Клини – коммутативной версии класса алгебраических систем, широко используемых в теоретической информатике для описания формальных языков и моделирования вычислений. Высокую алгоритмическую сложность даёт операция итерации, соответствующая повторению некоторого действия конечное, но заранее неизвестное число раз. Интерес при этом представляет *-непрерывный случай, в котором итерация определяется как предел степеней элемента. В рамках проекта в 2022 г. установлена алгоритмическая сложность задачи семантического следования на классе *-непрерывных коммутативных алгебр Клини. Для любого линейного порядка (L, <), k-мерно интерпретируемого в стандартной модели арифметики Пресбургера (k >= 1), существует такое натуральное число m >= k и подмножество D множества Z^m, что: 1) D определимо в арифметике Пресбургера; 2) L является ограничением лексикографического порядка на Z^m на множество D; 3) биекция, связанная с данной интерпретацией, определима в арифметике Пресбургера. Из этого следует, что порядки, m-мерно интерпретируемые в PrA для некоторого m, в точности являются ограничениями лексикографического порядка на (Z^k,<) на некоторое PrA-определимое подмножество D в Z^k. Исследовались системы ординальных обозначений, основанные на строго позитивных исчислениях. Рассмотрено обобщение понятия спектра консервативности арифметической теории на язык с трансфинитно итерированными определениями истинности. Установлено естественное соответствие между спектрами консервативности и точками специальной модели Крипке, введенной Д. Фернандесом–Дуке и Й. Йоостеном. Тем самым получено конструктивное описание всевозможных последовательностей ординалов, являющихся спектрами консервативности. Для итерированных схем рефлексии над теориями определений истинности установлены результаты о консервативности, аналогичные хорошо известным формулам Шмерля. Логика Дошена N — важный представитель семейства интуиционистских модальных логик. Среди интересных расширений N стоит выделить логики N^* и Hype. Первая была введена П. Кабаларом, С.П. Одинцовым и Д. Пирсом в ходе изучения логических программ с отрицанием, которые используются в некоторых парадигмах декларативного программирования. Вторая активно изучалась в последнее время в связи с проблемой «гиперинтенциональности» в формальной семантике. С помощью подходящей модификации метода фильтрации мы доказали разрешимость некоторых естественных расширений N, таких как N^* с законом введения двойного отрицания, N^* с законом снятия двойного отрицания и Hype. (Заметим, что разрешимость N и N^* была установлена ранее С.А. Дробышевичем и С.П. Одинцовым.) Также мы показали, что происходит с некоторым важным расширениям N при добавлении схемы замены. Логики свидетельств представляют собой интересное семейство эпистемических логик, в которых имеется возможность отслеживать происхождение убеждений эпистемических агентов. Можно легко показать, что всякая логика свидетельств связана с какой-то модальной логикой. Интерес представляет обратная задача: по данной модальной логике найти, связанную с ней логику свидетельств, и получить соответствующую теорему об этой связи, так называемую теорему о реализации. В этом году мы изучали модальную логику транзитивного замыкания, нашли связанную с ней логику свидетельств и получили соответствующую теорему о реализации. Благодаря переводу кванторов в модальности, можно рассматривать логики предикатов как логики высказываний с дополнительными модальностями. Этот метод систематически применен для исследования семантических и алгоритмических свойств модальных предикатных логик. Топологические произведения модальных логик помогают моделировать и изучать многомерные непрерывные структуры и процессы. Изучение произведений модальных логик позволяет формально описать и автоматически (с помощью компьютерной программы) определять истинность или ложность формально записанных свойств. Это может помочь в изучении и моделировании работы программ, работающих со структурами, в которых одна или несколько координат имеют непрерывную природу. Нам удалось точно аксиоматизировать топологическое произведение S4.1 x S4 и D4.1 x L, где L – хорнова предтранзитивная сериальная логика. Предложен новый класс правил вывода с бесконечным числом посылок, обобщающих омега-правило, которые позволяют получать полные теории различных поточечно определимых моделей первого порядка из их простых фрагментов, которые можно понимать, как обобщённые диаграммы. Такие правила названы правилами ограничения, поскольку модели, к полным теориям которых они приводят, просты и, значит, опускают все типы, которые возможно опустить (как стандартная модель арифметики). Наиболее общая формулировка правил ограничения была предложена в отчётный период выполнения проекта; в ней заключение правила релятивизировано на выделенный одноместный предикат. Это позволяет получать полную теорию рассматриваемой модели внутри большей теории (например, теории множеств). В качестве примера показано, что полная теория универсума конструктивных по Гёделю множеств выводится из обобщённой диаграммы наименьшей транзитивную модели теории множеств посредством соответствующего правила ограничения (со счётным числом посылок). Также рассмотрены обобщения предложенных конструкций на инфинитарные языки и языков высших порядков.

Публикации

1. Беклемишев Л.Д. Спектры консервативности и модель Йоостена-Фернандеса Доклады Российской академии наук. Математика, информатика, процессы управления, T. 505, № 1, стр. 5-10 (год публикации - 2022) https://doi.org/10.1134/S1064562422040032

2. Кузнецов С.Л. Reasoning in commutative Kleene algebras from *-free hypotheses The Logica Yearbook 2021, The Logica Yearbook 2021, College Publications, London, 2022, pp. 99-113 (год публикации - 2022)

3. Сперанский С.О. Some remarks on Došen's logic N and its extensions Сибирские электронные математические известия, Том 19, № 2, стр. 562-577 (год публикации - 2022) https://doi.org/10.33048/semi.2022.19.047

4. Чистопольская А.И., Подольский В.В. On the decision tree complexity of threshold functions Theory of Computing Systems, Vol. 66, N 6, P. 1074-1098 (год публикации - 2022) https://doi.org/10.1007/s00224-022-10084-x

5. Шамканов Д.С. On algebraic and topological semantics of the modal logic of common knowledge S4CI Logic Journal of the IGPL, Published online, jzac075 (год публикации - 2022) https://doi.org/10.1093/jigpal/jzac075

Аннотация результатов, полученных в 2023 году
Был разработан вариант так называемой итерированной теории малого сокращения, применимый к широкому классу групп, заданных с помощью порождающих и определяющих соотношений "бернсайдовского типа". В частности, доказано, что такими группами являются свободные берснсайдовы группы периода, большего или равного 16000, делящегося на 16. В отличие от известных ранее подходов теория позволяет исследовать периодические группы с гораздо меньшей оценкой на значения периода. Было продолжено исследование вопросов алгоритмической сложности для алгебр Клини. Алгебры Клини представляют собой класс алгебраических систем, широко используемых в теоретической информатике для описания формальных языков и моделирования вычислений. Интерес при этом представляет *-непрерывный случай, в котором итерация определяется как предел степеней элемента. В 2023 году в рамках проекта получены уточнённые результаты о сложности следования из конечных множеств гипотез. Данные результаты усиливают более ранние результаты Д. Козена и С.Л. Кузнецова. А именно, установлено, что существуют фиксированные множества гипотез, для которых достигаются те же нижние оценки сложности, что и в общем случае. Результаты имеют место как в коммутативном, так и в некоммутативном случае. Исследовались логики доказуемости для негёделевых теорий, в которых формализуемо и доказуемо утверждение о собственной непротиворечивости. Самым простым примером такой теории, обнаруженном сравнительно недавно К. Нибергаллем, является пересечение теорий S и T, где S – расширение арифметики Пеано PA всеми истинными П_1-предложениями, а T = PA+Con(S) – расширение PA утверждением о непротиворечивости теории S. Для логики доказуемости арифметики Нибергалля относительно арифметики Пеано описан класс конечных шкал Крипке и установлена теорема о полноте. Для консервативного расширения данной логики в языке с дополнительной пропозициональной константой также получена явная конечная аксиоматизация. Исследованы истинностная логика доказуемости арифметики Нибергалля и логика доказуемости относительно ее самой. Описаны классы моделей Крипке, относительно которых данные логики полны. Установлена PSpace-полнота проблемы выводимости в перечисленных логиках. Для логики доказуемости NA относительно арифметики Пеано установлено отсутствие интерполяционного свойства Крейга. Дана аксиоматизация замкнутого фрагмента логики доказуемости NA относительно арифметики Пеано, конструктивно описана универсальная модель Крипке для этого фрагмента и получено эффективное доказательство теоремы о нормальной форме для замкнутых формул. Были получены точные верхние оценки на сложность элементарных теорий некоторых естественных классов вероятностных пространств. Здесь под «элементарными теориями» подразумеваются теории в языке с кванторами по событиями и кванторами по вещественным числам. В частности, используя полученные ранее нижние оценки, было доказано, что элементарные теории класса всех вероятностных пространств и класса всех пространств с бесконечным числом атомов вычислимо эквивалентны полной арифметике второго порядка. Кроме того, эти сложностные результаты остаются верны, если оставить лишь кванторы по событиям. В этом году мы изучали инфинитарный вариант модальной логики транзитивного замыкания K+, получаемый из исходной системы с помощью добавления омега-правила. Работая с данной системой методами теории доказательств, мы ввели эквивалентное секвенициальное исчисление, допускающее нефундированные доказательства. Опираясь на теорему об устранении сечения в исчислении секвенций для логики K+, мы смогли получить результат об устранении сечения также для рассматриваемой нами системы. Исследовались границы применимости стандартной семантики Крипке для модальных логик предикатов. Новые результаты дополняют сложившуюся картину: имеются обширные семейства неполных логик, а доказательства полноты во многих случаях весьма нетривиальны. Также нетривиальны фрагменты модальных предикатных логик с одной переменной. В проекте изучались битопологические произведения топологических пространств и их модальные логики. Битопологические произведения отличаются от обычных тем, что в результате получаются пространства с двумя топологиями: горизонтальной и вертикальной. Модальные логики таких пространств интересны, т.к. являются естественным обобщением топологических модальных логик на двумерный случай. В частности в этом проекте мы нашли бимодальную логику произведений топологических пространств, в которых одно пространство является экстремально несвязным. Ранее полученные результаты распространены на инфинитарные языки L_{\kappa, \lambda}. Для определённых \kappa и \lambda имеются дедуктивные системы, удовлетворяющие слабой теореме о полноте; например, это верно для недостижимого кардинала \kappa (Карп). Отсюда следует, что если \kappa – сильно компактный, то L_{\kappa, \lambda} удовлетворяет теореме о полноте для любого числа формул. Напротив, языки вида L_{\kappa^+, \kappa^+} обладают высокой степенью неполноты (Скотт). Определены правила ограничения для L_{\kappa, \lambda} и показано, что их добавление к базовой дедуктивной системе даёт аналогичные теоремы о синтаксической и о семантической полноте. Это позволяет выводить полные теории в языке L_{\kappa, \lambda} любых поточечно определимых моделей, вне зависимости от их полноты или неполноты без правил ограничения. Для случая сверхкомпактного \kappa установлен усиленный аналог теоремы Барвайза – для сигнатур любой мощности. Рассмотрены обобщения предложенных конструкций на языки второго порядка и соответствующие теоремы о полноте (например, для истинной арифметики второго порядка).

Публикации

1. Дворкин Л.В. О логиках доказуемости арифметики Нибергалля Известия РАН. Серия математическая, - (год публикации - 2024)

2. Кудинов А.В. Топологическое произведение модальных логик с аксиомой Маккинси Доклады Российской академии наук. Математика, информатика, процессы управления, - (год публикации - 2024)

3. Кузнецов С.Л. Алгоритмическая сложность теорий коммутативных алгебр Клини Известия РАН. Серия математическая, - (год публикации - 2024)

4. Сперанский С.О. Элементарные инварианты для кванторной вероятностной логики Доклады Российской академии наук. Математика, информатика, процессы управления, Том 510, сс. 8–12. (год публикации - 2023) https://doi.org/10.1134/S1064562423700667

5. Шехтман В.Б., Шкатов Д.П. Полупроизведения, произведения и предикатные логики: некоторые примеры Доклады Российской академии наук. Математика, информатика, процессы управления, том 513, с. 98-106 (год публикации - 2023) https://doi.org/10.31857/S2686954323600325

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