Аннотация результатов, полученных в 2024 году
Изучалась сложность монотонного оператора скачка, который соответствует предложенной Фиттингом модификации подхода Крипке в формальной теории истины. Доказано, что наименьшая неподвижная точка оператора Фиттинга является \Pi^1_1-полным множеством, т.е. имеет ту же сложность, что и \Pi^1_1-фрагмент арифметики второго порядка. Кроме того, замыкающий ординал этого оператора в точности равен наименьшему неконструктивному ординалу, т.е. первому ординалу, который не изоморфен никакому вычислимому вполне упорядоченному множеству. Исследовались вопросы сложности выводимости из гипотез для инфинитарной логики действий (мультипликативно-аддитивного исчисления Ламбека с итерацией Клини). Структуры с итерацией Клини обобщают регулярные выражения и играют важную роль в теоретической информатике. С помощью регулярных выражений и их обобщений описываются не только «шаблоны слов» для поиска в больших корпусах данных, но и работа вычислительных систем в целом. Логика действий обобщает алгебру Клини операциями деления. В ходе проекта установлено, что некоторые из задач выводимости из гипотез в присутствии делений имеют существенно иную сложность, чем в исходной алгебре Клини (Козен, 2002). А именно, для выводимости из гипотез без итерации установлена точная гиперарифметическая оценка сложности (на уровне \omega^\omega гиперарифметической иерархии). Задачи выводимости из гипотез естественно связаны с расширениями логики действий экспоненциальной и субэкспоненциальными модальностями. Для них также получены соответствующие результаты о сложности. Также исследовался неассоциативный вариант инфинитарной логики действий (он является алгоритмически разрешимым) и системы без итерации Клини, но с более тонким субэкспоненциалом, допускающим локальное сокращение. Помимо этого, в теоретической информатике, темпоральной логике рассматриваются обобщения регулярных выражений, называемые омега-регулярными выражениями: в них используется омега-итерация, которая позволяет порождать бесконечные строки. В рамках проекта в 2024 году было введено мультипликативно-аддитивное исчисление Ламбека с омега-итерацией и исследованы его базовые свойства. Доказана нижняя оценка на сложность алгоритмической задачи выводимости в данном исчислении. С теоретической точки зрения представляет интерес синтаксис этого исчисления: выводимые объекты в нем являются конечными либо бесконечными строками; из-за этого сложность упомянутой выше задачи очень высока, она находится не ниже второго уровня аналитической иерархии. В рамках проекта исследуются обобщения категориальных грамматик — одного из методов моделирования естественных языков и языков программирования — на графы. В 2021-2023 году Т.Г. Пшеницыным было введено и исследовано понятие гиперграфовых категориальных грамматик Ламбека. В рамках проекта в 2024 году были введены и исследованы гиперграфовые категориальные грамматики, основанные на интуиционистской линейной логике первого порядка. Данный новый подход опирается на хорошо исследованный аппарат линейной логики и обобщает понятие MILL1-грамматик, введенных в работе С.А. Славнова 2023 года. Была установлена связь данных грамматик с классическим подходом в теории графовых грамматик — гиперграфовыми порождающими грамматиками, а также связь с гиперграфовыми грамматиками Ламбека. Семантика устойчивых моделей (множеств ответов) Гельфонда и Лифшица является наиболее важной и хорошо исследованной семантикой логических программ с оператором «отрицание-как-неудача» и является основой новой парадигмы в рамках логического программирования, известной как «программирование множеств ответов» (англ. answer set programming). Немонотонные следования над множествами ответов (в разных языках) допускают представления в виде равновесных логик, дедуктивными базами которых являются конечнозначные монотонные логики. Мы определяем Белнаповские слабые временные логики BS4_{t2} и B3S4_{t2} синтаксически и семантически, доказываем теоремы полноты, и показываем, что для избыточной и паранепротиворечивой (т.е. допускающей противоречивые множества ответов) равновесных логик в языке с сильным отрицанием их немонотонные отношения следования точно вкладываются в теории определенные над логиками BS4_{t2} и B3S4_{t2}. Доказана теорема о полноте модальной логики первого порядка, расширенной отношением «свидетельство–утверждение» FOLP^{\Box} относительно моделей в стиле Крипке и Фиттинга. Изучался вопрос аксиоматизируемости «слабого» варианта односортной (точнее, без кванторов по вещественным числам) первопорядковой логики вероятности с распределением на носителе, предложенной Хальперном, где в семантике используются слабые вероятностные структуры в духе Кейслера и Хувера. Разработано подходящее инфинитарное исчисление для получающейся логики и доказана его сильная полнота относительно рассматриваемого класса структур. Также решена аналогичная задача для линейного фрагмента данной логики, который имеет дело с линейными комбинациями вероятностей.

Аннотация результатов, полученных в 2025 году
Доказано существование континуального семейства расширений конструктивной логики Нельсона N4^{\bot}, у которых есть модальные напарники. В частности, модальные напарники есть у каждого расширения избыточной логики Нельсона N3^{\bot}, а также у каждого N4^{\bot}-расширения, которое задаётся аксиомами, в которые сильное отрицание входит только в составе подформулы вида p v ~p. Также доказано, что имеется континуальный класс расширений логики N4^{\bot}, которые не имеют модальных напарников. Доказано, что свойство табличности не переносится на наименьший модальный напарник N4^{\bot}-расширения, но переносится на напарник, содержащий аксиому Гжегорчика. Описаны предтабличные расширения логики BS4 и установлено, что свойство предтабличности не переносится на известные модальные напарники. Схема слабого Клини — одна из важнейших схем частичных означиваний, использующихся в формальной теории истины по Крипке. Однако лежащая в её основе слабая (трёхзначная) логика Клини обладает существенными недостатками, затрудняющими её применение. В рамках проекта изучались некоторые полезные модификации первопорядковой версии слабой логики Клини, которые лишены вышеупомянутых недостатков. Были построены подходящие полные секвенциальные исчисления для этих модификаций. Для исчисления Ламбека существует много различных моделей. Одна из них – сопоставление формулам бинарных отношений. Такие модели называются R-моделями или реляционными моделями. Для расширения исчисления возможностью сокращать некоторые стоящие рядом формулы (они отмечены специальной модальностью «!») тоже можно придумать свои R-модели. Модальность в таком случае естественно интерпретировать как взятие некоторого плотного подотношения. Взятие наибольшего плотного подотношения не даёт сильной полноты исчисления даже при наличии специальных правил, призванных обеспечить максимальность подотношения. Однако если разрешить варьирование интерпретации модальности, то полнота будет иметь место даже в сильном смысле. Исследовалась алгоритмическая сложность неассоциативного исчисления Ламбека с итерированными делениями, заменяющими в данном случае итерацию Клини (Седлар 2019). В отличие от ассоциативного случая, данная логика алгоритмически разрешима, в том числе в присутствии аддитивных конъюнкции и дизъюнкции, связанных законом дистрибутивности. Построено размеченное секвенциальное исчисление с циклическими выводами, доказана теорема об устранении сечения, установлена верхняя оценка EXPSPACE на сложность задачи выводимости. Описан класс языков, задаваемых грамматиками на основе инфинитарной (ассоциативной) логики действий; получены результаты, характеризующие классы языков для её фрагментов. Итерация Клини и омега-итерация – алгебраические операции, описывающие конечные и бесконечные циклы в работе программ соответственно. Алгебры действий расширяют алгебры Клини – обобщающие, в свою очередь, алгебры регулярных выражений — с помощью конъюнкции и делений. Инфинитарная логика действий аксиоматизирует *-непрерывные алгебры действий, в которых итерация Клини a* определяется не индукцией, а явно — как объединение n-кратных итераций действия a. В литературе было введено несколько видов омега-алгебр, однако во всех них омега-итерация определяется через принцип коиндукции. Нами была определена новая логическая система, расширяющая инфинитарную логику действий «инфинитарной» омега-итерацией: a^\omega — это бесконечная последовательность a⋅a⋅a... В присутствии итерации Клини были доказаны нижняя и верхняя оценки сложности задачи доказуемости в данной логике. Было продолжено изучение вопросов аксиоматизируемости для односортной первопорядковой логики вероятности с распределением на носителе. Доказана теорема о сильной полноте разработанного ранее инфинитарного исчисления относительно дискретных вероятностных структур, т.е. оригинальной семантики Хальперна (до этого была получена лишь полнота относительно «слабых» вероятностных структур, где вместо одной дискретной меры используется семейство конечно-аддитивных мер, по одной на каждой декартовой степени носителя). Аналогичные результаты получены для ряда естественных фрагментов рассматриваемой логики. Дано определение базовой свидетельской функции в модели первопорядковой логики свидетельств со связывающими модальностями. Доказано, что каждая базовая свидетельская функция может быть до-определена до свидетельской функции модели Фиттинга. При этом проверка того, что функция является базовой свидетельской, значительно проще, чем проверка того, что она является свидетельской. В частности, базовая свидетельская функция может иметь конечную область определения, что важно для построения опровергающих моделей для конкретных формул. С помощью этого результата построены модели, опровергающие ряд формул, невыводимых в логике свидетельств первого порядка FOLP, расширенной связывающими модальностями.