Аннотация результатов, полученных в 2020 году
Наше исследование посвящено изучению логических систем, в которых можно встретить так называемые нефундированные доказательства. Отличительной особенностью данных доказательств является то, что в них переход от заключений к посылкам может продолжаться бесконечно долго, не достигая аксиом. Такие доказательства встречаются при изучении логических систем, отражающих те или иные аспекты индуктивных рассуждений, а также при изучении логик доказуемости. В центре нашего внимания находилась важная и широко известная среди специалистов по теории доказательств полимодальная логика доказуемости GLP. Мы рассмотрели расширение данной логики, добавив к задающему данную логику аксиоматическому исчислению произвольные нефундированные выводы, и изучили семантику получившейся системы. Мы доказали, что данная система полна относительно ее окрестностной (топологической) семантики в случае глобального отношения семантического следования. В качестве интересного следствия, мы также получили новое доказательство теоремы об окрестной полноте для логики доказуемости GLP. Кроме того, изучая другую интересную модальную логику, логику Гжегорчика Grz, мы дали для неё синтаксическое доказательство интерполяционного свойство Линдона. Исчисление Ламбека – это субструктурная логическая система, в которой отсутствуют правила сокращения, ослабления и перестановки. Таким образом, формулы исчисления Ламбека выражают расходуемые ресурсы, для которых также существенно важен порядок их использования. Рассматриваются полимодальные расширения исчисления Ламбека (Нигам и Миллер, 2006; Канович и др. 2019) с субструктурными модальностями, под которыми допускаются все или некоторые структурные правила (для каждой модальности – свой набор правил). Добавление к исчислению Ламбека таких модальностей приводит к системам с существенно большими выразительными возможностями, что приводит к алгоритмической неразрешимости. В рамках проекта в 2020 г. было рассмотрено дальнейшее расширение исчисления Ламбека с субэкспоненциальными модальностями, а именно, к исчислению была добавлена операция итерации (“звёздочка Клини”). Для этого исчисления задача выводимости оказалась не только неразрешимой, но и даже неарифметической. Также был вычислен замыкающий ординал этой системы: неформально говоря, наименьший “уровень”, на котором применение правил вывода уже не даёт больше новых теорем. Также был исследован коммутативный вариант исчисления Ламбека, расширенный операцией итерации (без субэкспоненциальных модальностей), доказана его алгоритмическая неразрешимость и неперечислимость (т.е., в частности, невозможность аксиоматизации с помощью системы с конечными доказательствами). Теория BI – это фрагмент арифметики второго порядка, который позволяет формализовать широкий класс доказательств с использованием трансфинитной индукции. В данном проекте исследуется вопрос о распространении программы ординального анализа в терминах итерированных схем рефлексии на случай теории BI. Было разработано исчисление рефлексии RC_BI, которое позволяет говорить о схемах рефлексии трех естественных типов. Была формализована в теории ACA_0 теорема Эша и Найт о семействах вычислимых линейных порядков. Тем самым было показано, что существует семейство индексированных \Pi^0_{2n+1}-предложениями F вычислимых линейных порядков L_F таких, что в ACA_0 доказуемо, что порядок L_F фундирован, если и только если предложение F истинно. При этом, если L_F фундирован, то его порядковый тип равен \omega^n. Мы предполагаем, что далее это нам позволит получить точную верхнюю оценку на ординалы, требуемые для доказуемости всех истинных арифметических предложений в прогрессиях Тьюринга-Фефермана, основанных на итерации равномерной схемы рефлексии.

Аннотация результатов, полученных в 2021 году
В этом году мы изучали исчисление секвенций с нефундированными доказательствами для модальной логики транзитивного замыкания. Структурный анализ нефундированных доказательств в данном исчислении приводит к рассуждениям и определениям, содержащим индукцию с вложенной ко-индукцией с еще одной вложенной индукцией. Для нас было важно научиться аккуратно и естественно вводить математические объекты, определяемые такого рода образом. Для этого на множестве операций, действующих на нефундированных доказательств нашего исчисления, мы определили специальную структуру пространства с вполне упорядоченной системой отношений эквивалентности и доказали теорему о неподвижной точке, которая позволяет работать с вышеупомянутыми определениями. В 2021 г. мы продолжили исследование субструктурных логик, обогащённых итерацией Клини. Операция итерации аксиоматизируется с помощью омега-правила: чтобы обосновать утверждение о повторении некоторого действия неопределённое число раз, нужно доказать его для каждого конкретного количества применений. За счёт этого соответствующие логические теории оказываются не только алгоритмически неразрешимыми, но могут даже выходить за рамки гиперарифметической иерархии сложности. Таково исчисление Ламбека с субэкспоненциальными модальностями и итерацией, рассмотренное в прошлом году в рамках проекта. В этом году мы выявили и исследовали системы с промежуточным уровнем сложности. При их исследовании, наряду с омега-правилом, использовались системы, в которых доказательства могут включать бесконечные ветви, с определёнными условиями корректности. Было продолжено исследование, связанное с ординальным анализом теории бар-индукции BI на основе схем рефлексии. Был получен ряд результатов о частичной консервативности для принципов омега-модельной рефлексии и принципов синтаксической рефлексии. Были получены точные оценки на ординалы, требуемых для теоремы Фефермана об арифметической полноте трансфинитных итераций схем рефлексии. Исследована проблема изоморфизма алгебр доказуемости формальных арифметических теорий. Найдено более общее достаточное условие отсутствия эпиморфизмов между алгебрами доказуемости, усиливающее известные ранее условия Адамссона и Шаврукова. На основе полученного усиления построен целый ряд новых примеров пар формальных арифметических теорий с неизоморфными алгебрами доказуемости, в том числе, примеры пар теорий, не подпадающих под действие ранее известных условий. Изучена семантика типа Крипке совместной логики задач и высказываний. Доказано, что любая непротиворечивая теория совместной логики задач и высказываний выполнима в некотором отмеченном мире некоторой модели. Тем самым установлена теорема о сильной полноте совместной логики задач и высказываний относительно построенной семантики. Показано, что интуиционистский фрагмент совместной логики задач и высказываний обладает дизъюнктивным свойством, а если язык содержит хотя бы одну константу, то и экзистенциальным свойством.

Аннотация результатов, полученных в 2022 году
Итерация Клини, задаваемая посредством омега-правила, добавленная к одной из базовых субструктурных логических систем (исчислению Ламбека), позволяет моделировать бесконечные (неостанавливающиеся) вычисления. В некотором смысле двойственной к ней операцией является субэкспоненциал, допускающий правило мультиплексирования. Система, сочетающая в себе обе операции (а в некоммутативном случае — также вспомогательную модальность для перестановки), позволяет моделировать произвольное чередование кванторов перед утверждением о неостанове вычисления на счётчиковой машине. Таким образом нами доказано, что эта система имеет сложность не ниже полной арифметики первого порядка. С другой стороны, с помощью верхней оценки на замыкающий ординал соответствующего оператора непосредственной выводимости мы получили гиперарифметическую верхнюю оценку на сложность данной системы. Неформально: итерация кванторов не может превзойти замыкающего ординала, т.е. \Sigma^0_{\omega^\omega}-уровня гиперарифметической иерархии. Результаты имеют место как в некоммутативном, так и в коммутативном случае. Структура натуральных чисел с отношением взаимной простоты — одна из наиболее важных базовых структур, возникающих при изучении «слабых арифметик». Нами было получено полное описание монадической второпорядковой определимости в этой структуре. В частности, из данного описания следует, что всякое \Pi^1_1-множество, замкнутое относительно автоморфизмов рассматриваемой структуры, определимо в ней посредством монадической \Pi^1_1-формулы с ровно одним квантором по множествам. В этом году мы продолжили изучение исчисления секвенций с нефундированными доказательствами для модальной логики транзитивного замыкания. Наша цель состояла в том, чтобы получить синтаксическое доказательство устранимости правила сечения в данной системе. Структурный анализ нефундированных доказательств в данном исчислении приводит к рассуждениям и определениям, содержащим индукцию с вложенной ко-индукцией с еще одной вложенной индукцией. Мы научились как аккуратно вводить математические объекты, определяемые такого рода образом, так и строго доказывать их свойства. Благодаря этому мы получили синтаксическое доказательство устранимости правила сечения и существенно продвинулись в понимании дедуктивных систем с нефундированными выводами с точки зрения структурной теории доказательств. Были получены новые результаты, касающиеся фрагментов формальной арифметики Пеано, основанных на дедуктивных системах с нефундированными и циклическими выводами. Циклические системы доказательств интересны с точки зрения их применений для автоматического индуктивного поиска вывода и как возможный метод анализа свойств формальных индуктивных теорий. Было найдено естественное условие на циклические выводы, приводящее к более широкому классу выводов и множеству теорем, замкнутому относительно следования в логике первого порядка. Было показано, что это исчисление содержит фрагмент арифметики Пеано, аксиоматизируемый правилом индукции для \Sigma_{n+1}-формул, что сильнее, чем ранее исследованные А. Дасом фрагменты циклической арифметики с теми же ограничениями на кванторную сложность. Мы изучали теорию бар-индукции BI, т.е. систему арифметики второго порядка, основной схемой аксиом которой является принцип индукции по всем вполне упорядоченным множествам, заданным на множестве натуральных чисел. Цель нашего исследования состояла в том, чтобы распространить методы теоретико-доказательного анализа на основе алгебр рефлексии на данную непредикативную систему. Известные применения этого метода до сих пор ограничен существенно более слабыми предикативными теориями. В 2022 году мы разработали систему ординальных обозначений для теории BI, основанную на аксиоматизации тождеств операторов рефлексии, действующих на фрагментах BI. Таким образом, мы получили новое конструктивное описание ординала Бахмана-Ховарда. В 2022 г. было продолжено исследование проблема изоморфности алгебр доказуемости формальных арифметических теорий. Получено более сильное и общее достаточное условие отсутствия эпиморфизмов между алгебрами доказуемости, основанное на сравнении субрекурсивных классов функций, связанных с теориями, а также показано, что данное условие влечёт отсутствие элементарной эквивалентности соответствующих алгебр. Доказанное усиление позволило построить новую серию примеров пар формальных арифметических теорий изоморфными алгебрами доказуемости, но неизоморфными бимодальными алгебрами доказуемости. Исследовалась совместная логика задач и высказываний HC, введенная С.А. Мелиховым. Суть этой логики состоит в попытке формализации идеи А.Н. Колмогорова о едином логическом формализме, в котором наряду с «высказываниями» (понимаемыми классическим образом) рассматриваются также «задачи», понимаемые конструктивно. А.А. Оноприенко ранее было показано, что логика этой модальности совпадает с интуиционистской эпистемической логикой IEL+, предложенной С. Артемовым и Т. Протопопеску. Таким образом IEL+ может рассматриваться как фрагмент логики Мелихова HC. В отчетном году мы рассматривали вопрос об обратном переводе логики HC в логику IEL+, естественно обобщающем негативный перевод Гёделя-Генцена классической логики в интуиционистскую. Был предложен естественный перевод совместной логики задач и высказываний HC в интуиционистскую эпистемическую логику IEL+, как в пропозициональном, так и в предикатном случае. Показано, что получившаяся интерпретация HC в IEL+ является корректной, но не точной. Также нами был рассмотрен вопрос о наличии какого-либо точного перевода из HC в IEL+ (в пропозициональном случае) и показано, что никакой перевод HC в IEL+, сохраняющий импликацию, не может быть точным.