Аннотация результатов, полученных в 2016 году
Найдена полная аксиоматизация бимодальной логики для операторов топологической производной и его $\alpha$-итерации на пространстве ординалов с интервальной топологией, где $\alpha$ – предельный ординал. Доказана финитная аппроксимируемость и разрешимость этой логики. Рассматривался вопрос о выразимости трансфинитных итераций операторов рефлексии в строго позитивной логике доказуемости с операторами П_n-рефлексии и П_n-консервативности. Показано, что в таком языке выразимы итерированные операторы рефлексии для каждого ординала $\alpha$, меньшего $\epsilon_0$ – характеристического ординала арифметики Пеано. Сформулировано строго позитивное исчисление, корректное относительно рассматриваемой арифметической интерпретации. Установлены эффективные теоремы о (единственной) нормальной форме для замкнутых строго позитивных формул в этом исчислении. Известная полимодальная логика доказуемости GLP была введена Г.К. Джапаридзе в 1986 году. Алгебраические модели этой логики называются GLP-алгебрами. Было доказано, что для каждого n свободная, порожденная константами 0 и 1, GLP-алгебра c n модальностями обладает разрешимой элементарной теорией. Этот результат дает ответ на открытый вопрос, поставленный Л. Д. Беклемишевым и А. Виссером в 2005 г. Индексом Кузнецова данной модальной логики L называется такой наименьший кардинал, что найдется шкала Крипке, мощность которой равна данному кардиналу и логика этой шкалы совпадает с L. Аналогично индекс Кузнецова определяется и для других логик с семантикой Крипке. Еще в 1983 году А.В. Кузнецовым был поставлен вопрос об описании возможных индексов Кузнецова для суперинтуиционистских логик и расширений S4. Нами была получена такая классификация для случая гибридных логик, в которых имеет место аксиома S4 и имеются номиналы и константы, выражающие глубину мира в шкале. В классической логике первого порядка известны два стандартных вида формул: предваренные нормальные формы и нормальные формы Хинтикки. В интуиционистской и модальной логике не всякая формула приводится к предваренной форме; однако в данном проекте впервые построены аналоги нормальных форм Хинтикки. Для этого были использованы бисимуляционные игры Эренфойхта (они также ранее не изучались). Затем выяснилось, что для некоторых классов модальных и интуиционистских теорий равенства формулы приводятся к нормальной форме ограниченной глубины. Отсюда возникают конечные модели и разрешающие алгоритмы для таких теорий. Классический результат Сегерберга - Максимовой устанавливает, что критерием локальной табличности транзитивной модальной логики является её конечная высота. Понятие конечной высоты можно распространить на случай логик с выразимым транзитивным оператором ("предтранзитивные" логики). Мы показываем, что предтранзитивность является необходимым условием локальной табличности. Далее мы описываем два семантических критерия локальной табличности. С их помощью мы расширяем критерий Сегерберга - Максимовой на случай некоторого большего семейства логик. Мы доказываем ряд новых результатов о полноте и разрешимости лексикографических сумм модальных логик на основе логик доказуемости, а также их различных расширений. Найдены гибридные логики евклидовых пространств и доказана полнота соответствующих логик. Также найдены окрестностные произведения логик, аксиоматизируемых хорновыми предтранзитивными или замкнутыми формулами, с логикой S5. Для данного класса K моделей некоторой фиксированной сигнатуры и отношения R между моделями этого класса возникает естественная задача описания свойств (K,R) в модальном языке. Для этого пропозициональные формулы интерпретируются как предложения данной сигнатуры таким образом, чтобы истинность формулы "возможно Ф" в модели M означала истинность Ф в некоторой модели N, связанной с M данным отношением. Мы описываем базовые свойства возникающих модальных логик и строим полную модальную аксиоматику отношения "быть подмоделью" для класса всех моделей сигнатуры, содержащей хотя бы один бинарный функциональный символ. Если сигнатура рассматриваемого языка содержит константы, то возникающая логика – это S4.2.1, в случае без констант – S4. Проводилось исследование борелевских и к-плотных множеств действительных чисел, наделенных естественным линейным порядком, унаследованным с вещественной прямой. В частности, установлено, что существует ровно один порядковый тип континуально плотных однородных F_\sigma-множеств и ровно два порядковых типа однородных G_\delta-множеств, не являющихся ни открытыми, ни замкнутыми ни в каком нетривиальном интервале. Установлено, что если существует ровно один порядковый тип к-плотных множеств действительных чисел, то всякое множество действительных чисел мощности к является Q-множеством. Также установлено, что множество тех кардиналов к, для которых существует ровно один порядковый тип к-плотных множеств действительных чисел, содержит пределы всех ограниченных счётных последовательностей своих элементов. Линейная логика, отличающаяся от классической и интуиционистской отсутствием структурных правил ослабления и сокращения, введена и используется для логических рассуждений, учитывающих расход некоторого ресурса. Некоммутативный вариант этой логики учитывает не только количество, но и порядок ресурсов, и применяется в теоретической информатике и математической лингвистике (в последнем случае "ресурсы" суть слова и группы слов). Версия линейной логики, используемая в лингвистике, называется исчислением Ламбека. Мы исследовали несколько алгоритмических задач, связанных с некоммутативной линейной логикой. Для проблемы выводимости из конечного множества гипотез во фрагменте с одной переменной доказана алгоритмическая неразрешимость. Также доказана алгоритмическая неразрешимость для "чистой" (без гипотез) проблемы выводимости в нескольких вариантах с (суб)экспоненциальными модальностями. В расширении с экспоненциальной модальностью и итерацией Клини доказана П_0^2-трудность проблемы выводимости. Был исследован вопрос о реализации пороговой функции от n переменных с весом 1 при каждой переменной и порогом близким к n/2 с помощью булевых схем глубины 2 и 3, состоящих из пороговых функций с весом k меньшим n. Для схем глубины 2 была установлена нижняя оценка $n^{13/19}$ с точностью до логарифмического множителя. Лучшая известная нижняя оценка – тривиальная оценка k не больше n. Для схем глубины 3 была построена схема с k не больше $n^{2/3}$ с точностью до постоянного множителя. Была построена общая схема, позволяющая моделировать машины Тьюринга, работающие на линейно ограниченной памяти, с помощью систем переписывания слов, сохраняющих длину. Было доказано, что существует конечная система подстановок слов, сохраняющих длину, для которой функция сложности выводов не эквивалентна полиномиальной или экспоненциальной функции.

Аннотация результатов, полученных в 2017 году
Л.Д. Беклемишевым в рамках данного проекта начато исследование строго позитивной логики доказуемости с операторами рефлексии и консервативности. Исследование таких структур интересно с нескольких точек зрения. Во-первых, рассматриваемый язык позволяет говорить о важном для изучения арифметических теорий понятии П_n-консервативности, выражающем меру близости арифметических теорий друг к другу. Это понятие тесно связано с вычислением важных количественных характеристик формальных теорий – теоретико-доказательственных П_n-ординалов. Во-вторых, для строго позитивных исчислений подразумеваемая интерпретация не ограничивается лишь конечными расширениями базисной арифметической теории, что расширяет выразительные возможности языка. В-третьих, строго позитивные логики, как правило, проще соответствующих модальных логик как с точки зрения семантики Крипке, так и с точки зрения вычислительной сложности. Сформулировано арифметически корректное исчисление, описывающее тождества обогащенной операторами рефлексии и консервативности полурешетки расширений элементарной арифметики. Показано, что этот язык обладает значительными выразительными возможностями, в частности, в таком языке выразимы итерированные операторы рефлексии для каждого ординала $\alpha$, меньшего $\epsilon_0$, характеристического ординала арифметики Пеано. Были доказаны теоремы о нормальной форме для замкнутых формул данного исчисления, доказаны алгоритмическая разрешимость и арифметическая полнота его замкнутого фрагмента. В 2017 году была исследована алгебраическая семантика замкнутого фрагмента этого исчисления. Дано конструктивное описание соответствующей полурешетки Линденбаума-Тарского с операторами рефлексии и консервативности и установлена её точная связь с универсальной моделью Игнатьева для замкнутого фрагмента полимодальной логики доказуемости GLP. Также дано конструктивное описание универсальной модели Крипке для замкнутого фрагмента рассматриваемой логики. Доказано, что любая одномерная интерпретация арифметики Пресбургера в себе доказуемо изоморфна тождественной, тем самым получено доказательство гипотезы Виссера для одномерных интерпретаций. Установлено необходимое условие m-мерной интерпретируемости линейного порядка в арифметике Пресбургера. Полученные результаты изложены в статье A. Zapryagaev, F. Pakhomov. Interpretations of Presburger Arithmetic in Itself. Статья принята к публикации в сборнике LFCS 2018 (ISBN 978-3-319-72055-5, Lecture Notes in Computer Science 10703). Был разработан метод симуляции гибридных логик с номиналами и константами уровня, содержащих модальную логику S4, в гибридных логиках использующих лишь номиналы. Для таких логик были изучены их индексы Кузнецова - наименьшие мощности, в которых достигается полнота этих логик по Крипке. Было показано, что для всякой Π^1_1-аксиоматизируемой теории второго порядка в счетной сигнатуре найдется расширение S4 с номиналами такое, что индексы Кузнецова этого расширения и данной теории совпадут. В качестве следствия аналогичный результат также получен для расширений модальной логики GL с номиналами. Свойство Де Йонга - важная характеристика интуиционистской теории; оно показывает, что в теории не выводятся никакие логические законы, кроме базовых интуиционистских (которые задаются исчислением Гейтинга). Впервые оно было доказано Де Йонгом для интуиционистской арифметики в 1968 г. С этой точки были проанализированы еще некоторые интуиционистские теории (с равенством, порядком, функцией следования), но многие вопросы остались открытыми, и общая панорама пока не видна. После работы Бралбека (2010), где изучались 10 специальных теорий, новых результатов в этой области не было. В данном проекте получено первое новое продвижение: а именно, рассмотрены теории следования и скорректирован результат Бралбека на эту тему. Проблема полноты модальных логик предикатов решена для достаточно ограниченного класса логик. По-прежнему нет общих теорем о полноте для логик с непостоянными областями, и нет общих методов для их получения. В данной области важны любые новые результаты, но в течение последних 10 лет прогресс был незначительным. Полученный в данном проекте результат открывает исследование нетранзитивных предикатных логик, о которых почти ничего не было известно. Продолжалось исследование локальной табличности неклассических логик. Критерий локальной табличности и необходимое синтаксическое условие (найденные ранее в рамках настоящего проекта) были распространены на полимодальный случай. Это позволило получить ряд новых результатов о финитной аппроксимируемости и разрешимости. Кроме того, новые результаты о локальной табличности позволили получить существенное обобщение теоремы Гливенко. Теорема Гливенко (1929) утверждает, что выводимость пропозициональной формулы в классической логике высказываний CL равносильна выводимости её двойного отрицания в интуиционистской логике IL. В семантике Крипке интуиционистская логика является логикой частичных порядков, а классическая – логикой одной точки, или, что эквивалентно, логикой частичных порядков высоты 1. Для интуиционистской или модальной логики L пусть L[h] – расширение L аксиомой высоты h. Теорема Гливенко описывает сводимость IL[1], то есть CL, к IL. В рамках настоящего проекта рассматривался вопрос о сводимости L[h] к L для случая произвольного конечного h. Показано, что аналог теоремы Гливенко имеет место для произвольной интуиционистской логики конечной высоты, и для произвольной полимодальной локально табличной логики. Было продолжено исследование модальных логик отношения «быть подмоделью», в которых «возможность» предложения S в модели А означает его выполнимость в некоторой подмодели В модели А, на классе моделей фиксированной сигнатуры. Показано, что в случае сигнатуры с предикатом валентности не менее, чем 2, отношение «быть подмоделью» невыразимо в инфинитарной логике L_{\infty,\omega}. Далее исследовался случай сигнатур с одноместными предикатами и, возможно, константами. Показано, что если сигнатура имеет к одноместных предикатов, то возникающая логика совпадает с логикой прямого произведения ординалов с отношением обратного порядка в числе 2^к, из которого удалён наибольший элемент в случае отсутствия константных символов в сигнатуре. Показано, что такая логика является финитно аппроксимируемым расширением логики Гжегорчика Grz, если число к конечно. Более того, эти логики в пересечении дают в точности модальный компаньон логики Медведева в случае отсутствия константных символов, и логику Grz.2 иначе. Модальные логики произведений реляционных структур (шкал Крипке) активно изучаются последние годы. Окрестностные шкалы (в транзитивном и рефлексивном случае соответствующие топологическим пространствам) являются естественным обобщением шкал Крипке. Модальные логики произведений окрестностных шкал до сих пор систематически не изучались. А.В. Кудиновым были построены полные аксиоматизации для целого семейства классов произведений окрестностных шкал, а также для смешанных произведений окрестностных шкал со шкалами Крипке. Исчисление Ламбека было введено И. Ламбеком в 1958 году для математического описания синтаксиса естественных языков. Основные операции исчисления Ламбека - это операции деления: A \ B (соответственно, B / A) означает тип синтаксических объектов, которые становятся объектами типа B, если к ним слева (соответственно, справа) приписать произвольный объект типа A. Например, если N – это тип имён существительных, а S – тип правильно построенных предложений, то в N \ S попадут непереходные глаголы. Эти операции допускают естественную интерпретацию на множестве формальных языков (множеств слов над некоторым алфавитом), и оказывается естественным рассмотреть и другие подобные операции, в частности операцию итерации. Например, если S – тип "предложения", то S^+ – это тип "тексты" (текст состоит из нескольких записанных подряд предложений). Однако, как показано в ходе работы над проектом, соответствующие исчисление либо с необходимостью должно допускать бесконечные доказательства (выводы), либо неполно. Также исследовались неполные, но практически важные фрагменты бесконечного исчисления. Получен также ряд результатов о расширениях исчисления Ламбека другими операциями, имеющими значение для приложений в лингвистике. Исследовалась алгоритмическая задача о выполнимости заданной формулы полимодальной логики в заданной шкале. С этой точки зрения изучались исчисления с аксиомами транзитивности. В ряде случаев была показана полнота этой алгоритмической задачи в сложностных классах, лежащих в классе P задач, разрешимых за полиномиальное время. В области исследования функций сложности для систем подстановок термов были получены новые результаты о системах подстановок слов, сохраняющих длину. На основе результатов, полученных в ходе проекта в 2016 году, были построены широкие классы функций сложности вывода, не эквивалентные полиномиальным и экспоненциальным, в частности, было показано, что в качестве такой функции можно взять n^2 log(n)^2.

Аннотация результатов, полученных в 2018 году
В 2018 году Л.Д. Беклемишевым была продолжена работа по изучению строго позитивной логики доказуемости с операторами рефлексии и консервативности и опубликована работа, суммирующая полученные в этом направлении результаты (Успехи математических наук 73:4(442), 2018, с. 3-52). Была подробно изучена связь между рассматриваемой логикой и так называемыми спектрами консервативности для арифметических теорий. Для данной арифметической теории Т и выбранной элементарной системы ординальных обозначений П_n-ординалом теории Т называется наибольший такой ординал alpha, что в Т доказуема alpha-кратная итерация схемы П_n-рефлексии над элементарной арифметикой. Для наиболее естественных арифметических теорий (называемых регулярными) теория Т будет П_n-консервативным расширением такой alpha-кратно итерированной схемы рефлексии. Спектром консервативности теории Т называется последовательность П_n-ординалов теории Т для всех n>0. Таким образом, спектр консервативности содержит информацию о том, насколько теория сильна в смысле доказуемости предложений для каждого из классов П_n при n>0. Показано, что совокупность всех возможных спектров консервативности для ограниченных расширений элементарной арифметики образует полурешетку с монотонными операторами, изоморфную полурешетке Линденбаума-Тарского для замкнутого фрагмента строго позитивной логики доказуемости с операторами рефлексии и консервативности. Показана применимость рассматриваемой логики к задаче вычисления ординалов и спектров для конкретных арифметических теорий. Ф. Н. Пахомовым изучались формальные теории семейств определений истины, индексированных элементами линейно упорядоченного множества. В таких теориях каждое следующее определение истины покрывает первопорядковый язык, где разрешается использовать только определения истины со строго меньшими индексом. Мы рассматриваем две версии этих теорий, где аксиомы для уровней определения истины – это 1) однородные эквивалентности Тарского (каждая формула эквивалентна утверждению о своей истинности) и 2) композиционные аксиомы (определение истины коммутирует со всеми связками); в обоих случаях аксиомы сформулированы с кванторами по уровням определений истины. Используя формализацию парадокса Виссера-Ябло оказывается возможным показать, что обе эти теории всегда доказывают определенную форму индукции по множеству индексов определений истины. Из этого следует, что добавление бесконечного семейства определений истины к PA не является консервативным расширением. Более того, этот результат дает нам возможность сравнить теории итерированных определний истины и фрагментов арифметики второго порядка. Мы показываем, что теория с omega уровнями определений истины и эквивалентностями Тарского является взаимноинтерпретируемой с теорией ACA_0', которая расширяет ACA_0 аксиомой, утверждающей, что для каждого натурального числа n и множества X существует n-ый тьюринговский скачок от X. Теория с omega уровнями определения истины и композиционными аксиомами оказалась взаимоинтерпретируемой с теорией ACA_0^+, расширяющей ACA_0 посредством аксиомы постулирующей наличие кодированной omega-модели ACA_0 над каждым множеством X (эквивалентно, существование omega-вого тьюрингова скачка от каждого множества X). В. Б. Шехтманом разработан теоретико-игровой метод доказательства полноты для предикатных модальных логик. С его помощью доказана полнота по Крипке предикатных модальных логик с аксиомами типа плотности и Черча — Россера. Построено новое семейство неполных предикатных логик с аксиомой ослабленной рефлексивности. И. Б. Шапировским исследовались модальные логики сумм шкал Крипке. Получены новые результаты о финитной аппроксимируемости, алгоритмической разрешимости и локальной табличности логик сумм шкал. Д. И. Савельевым и И. Б. Шапировским было продолжено изучение модальных логик теоретико-модельных отношений. Для произвольных класса моделей C, отношения R на C и теоретико-модельного языка L было введено понятие модальной алгебры (и, соответственно, модальной логики) теории класса C в языке L. Полученные ранее результаты о модальной аксиоматизации отношения подмодели для случая языка второго порядка были обобщены на случай произвольных теоретико-модельных языков. Были исследованы модальные логики отношений гомоморфного образа. Для расширения языка первого порядка квантором выполнимости предложения в надмодели доказана теорема Левенгейма-Сколема о понижении мощности. Д. И. Савельевым также получены результаты о топологизации модальных и других универсальных алгебр и по смежным темам. Доказано, что n-я степень такой алгебры с топологией Зариского, задаваемой многочленами от n переменных, замкнута и нигде не плотна в её (n+1)-й степени (и подавно эти пространства не дискретны). А. В. Кудиновым доказана полнота первопорядковых расширений направленных вверх хорновых модальных логик относительно окрестностных шкал с постоянной предметной области. Исчисление Ламбека, введённое в 1958 г. для описания синтаксиса естественных языков, допускает расширение с помощью различных дополнительных операций. Одно из таких естественных расширений даёт операция итерации (“звёздочка Клини”): A* есть A, повторенное произвольное конечное число раз. Имеются два определения итерации: как предела n-х степеней A и как неподвижной точки – наименьшего элемента, содержащего единицу и замкнутого относительно умножения на A. В рамках проекта в 2018 г. С. Л. Кузнецовым построены явные примеры, различающие эти два определения; получены новые результаты о полноте и неполноте соответствующих логических исчислений относительно моделей на алгебрах бинарных отношений. В. В. Подольским исследовалась алгоритмическая задача проверки следования одной формулы из другой в строго позитивных фрагментах некоторых полимодальных логик. С этой точки зрения изучались исчисления с аксиомами транзитивности и аксиомами монотонности. В ряде случаев была показана полнота этой алгоритмической задачи в сложностных классах, лежащих в классе P задач, разрешимых за полиномиальное время. С. И. Адяном доказано, что любая счетная абелева группа D может быть вербально вложена в качестве центра в некоторую m-порожденную группу A так, что фактор группа A / D будет изоморфна свободной бернсайдовой группе B(m,n), где m>1, а n >= 665 — нечетное число. А. Л. Таламбуцe удалось найти систему переписывания слов, сохраняющую длину, для которой функция сложности находится в классе ϴ(n log(n)). С помощью указанной системы удалось построить более сложные системы переписывания слов, для которых функции сложности вывода асимптотически находятся между ϴ(n) и ϴ(n^2). В частности, удалось ответить на поставленный Ю. Кобаяши в 2011 году вопрос о том, существуют ли системы переписывания слов, для которых функции длин вывода лежат в классе ϴ(n^a), где 1<a<2; было доказано, что для любых пар натуральных чисел (a,b), где a>b существует конечная система переписывания слов, для которой функция сложности вывода принадлежит асимптотическому классу ϴ(n^(a/b)). Ссылки на информационные ресурсы в сети Интернет: https://arxiv.org/abs/1804.02641 Beklemishev, L. D. A universal Kripke frame for the variable-free fragment of RC∇. https://arxiv.org/abs/1810.01947 Saveliev D.I. Hindman’s finite sums theorem and its application to topologizations of algebras https://arxiv.org/abs/1804.09810 D. Saveliev, I. Shapirovsky On modal logics of model-theoretic relations. https://arxiv.org/abs/1804.09810 I.Shapirovsky, Glivenko's theorem, finite height, and local finiteness