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

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

 

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


Номер 20-41-05002

НазваниеНовые виды формальных доказательств и их представления

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

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

Года выполнения при поддержке РНФ2020 - 2022

КонкурсКонкурс 2019 года «Проведение фундаментальных научных исследований и поисковых научных исследований международными научными коллективами» (FWF)

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

Ключевые словаматематическая логика, теория доказательств, циклические доказательства, формальная арифметика, логика доказуемости, нефундированные доказательства, исчисление Ламбека, прогрессии Тьюринга-Фефермана, строго позитивные логики

Код ГРНТИ27.03.55


 

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


Аннотация
Аксиоматический метод Гильберта основан на пошаговом понятии доказательства: математическое доказательство есть последовательность утверждений A1, …, An, в которой каждое утверждение Ai либо является аксиомой, либо непосредственно получается из предшествующих утверждений по одному из постулированных правил вывода. При надлежащем уточнении, это понятие превращается в математически точное определение формального доказательства (вывода), в результате чего сами выводы становятся объектами математического исследования. Из этой идеи Д. Гильберта возникает предмет теории доказательств. Суть структурной теории доказательств состоит в том, чтобы извлекать разнообразную информацию из структурных свойств формальных выводов. После того как в работах Г. Генцена в 1930-х годах были созданы два важнейших метода представления и анализа формальных выводов, а именно секвенциальное исчисление и исчисление естественного вывода, структурный анализ стал одной из наиболее важных областей теории доказательств, в которой были получены существенные результаты. Достижения в этом направлении лежат в основе современного прогресса в прикладных областях, таких как автоматический поиск вывода, верификация (проверка корректности) доказательств, интерактивное доказательство теорем. В данном проекте акцент ставится на исследовании структурных свойств доказательств для систем с различными формами индукции, коиндукции и неподвижных точек, а также на исследовании новых интересных видов формальных доказательств, таких как циклические выводы или нефундированные выводы. Свойства таких выводов резко отличаются от привычных нам видов формальных выводов, таких как гильбертовский или секвенциальный. Такие системы возникли сравнительно недавно, прежде всего в прикладных областях логики и теоретической информатики, и привлекают все больший интерес специалистов. Системы, описывающие рассуждения с различными формами индукции, рекурсии или с использованием неподвижных точек (самоссылающихся утверждений), играют очень существенную роль в логике и ее приложениях в информатике. Модальное мю-исчисление, введенное Д. Скоттом и де Баккером (см. D. Kozen (1983). "Results on the Propositional μ-Calculus". Theor. Comput. Sci. 27 (3): 333–354), является расширением пропозициональной модальной логики операторами неподвижной точки. Мю-исчисление широко используется в задачах спецификации и верификации программ (state transition systems) и в смысле выразительных возможностей включает в себя стандартные временные логики, используемые для тех же целей, в том числе логику CTL*. Операция итерации Клини, называемая также “звездочкой Клини” и введенная в его важной работе 1956 года, является наиболее существенной (и интересной с математической точки зрения) операцией в языке регулярных выражений, широко применяемом инструменте сопоставления слов с образцами (например, в текстовых редакторах). Логика алгебр Клини, расширенная операциями деления и решеточными операциями, называется логикой действий (action logic). Логика действий естественным образом расширяет исчисление Ламбека, используемое в математической лингвистике для моделирования синтаксиса естественных языков. Классические теории первого порядка, например арифметика Пеано или теории индуктивных определений, также часто используют индукцию в качестве центрального принципа. Логики доказуемости для арифметических теорий, например логика Гёделя-Лёба GL и её полимодальное расширение GLP, включают так называемую аксиому Лёба, выражающую фундированность на шкалах Крипке. Структурная теория доказательств для систем с индукцией, неподвижными точками и подобными выразительными средствами, развита в недостаточной степени. В частности, вопрос о формальной системе конструктивно с устранимым правилом сечения для модального мю-исчисления, остается открытым. Также не известно ни одной системы без правила сечения (и со свойством подформульности), эквивалентной арифметике Пеано первого порядка. Для логических систем, использующих индуктивные определения и рассуждения, так называемые циклические выводы представляют собой интересную и многообещающую альтернативу традиционным древовидным доказательствам. Циклическое доказательство представляет собой ориентированный граф, помеченный формулами (секвенциями), в котором допустимы циклы, удовлетворяющие определенным условиям. Без наложения таких условий, как правило, в системе доказательств может возникнуть “порочный круг” и система окажется противоречивой. Подходящие условия зависят от конкретной рассматриваемой логики и их поиск представляет собой, в конкретных ситуациях, интересную логическую проблему. Поскольку циклические выводы допускают удобное для анализа представление доказательств с индукцией, в последние годы в математической логике и информатике усилился интерес к этому типу систем. В данном проекте мы планируем изучить различные аспекты систем с циклическими и нефундированными выводами, в том числе вопросы устранения сечения и семантики для таких систем. Другая часть проекта касается проблемы представления доказательств или преобразования доказательств из одной системы в другую. Вопросы такого рода возникают, в частности, при исследовании классических секвенциальных систем для логики предикатов первого порядка. В этом направлении будет исследоваться возможность более эффективного (элементарного) устранения сечения для определенных подклассов формул, возможность восстановления формальных выводов по их “скелетам” и устранения сечений на уровне “скелетов” доказательств. Наконец, важной частью проекта является применение методов логики доказуемости, пропозициональных модальных логик, к исследованию формальных арифметических теорий. Исследования в этом направлении активно ведутся в нескольких научных центрах, в том числе в Москве. Важной задачей здесь является распространение этих методов на непредикативные теории арифметики второго порядка. Существующие до сих пор результаты относятся к анализу предикативных, то есть более слабых, теорий. В нашем проекте мы планируем получить анализ арифметики со схемой бар-индукции и ее фрагментов, выходящей за рамки класса предикативных теорий, что является принципиальным усилением существующих результатов. Также мы планируем получить новые результаты касающиеся итерированных схем рефлексии, улучшающие оценки в известной теореме Фефермана.

Ожидаемые результаты
Структурная теория доказательств многих важных логических систем с операторами неподвижной точки, индуктивными и коиндуктивными определениями и т.п. в настоящее время развита относительно слабо. К примеру, вопросы об устранимости сечения для модального мю-исчисления, известной логической системы, применяемой для верификации вычислительных систем, до сих пор остаются открытыми. Мы планируем исследовать секвенциальные исчисления с нефундированными выводами для нескольких модальных логик с неподвижными точками, такие как модальная логика транзитивного замыкания и модальное мю-исчисление, и получить для этих систем результаты об устранимости правила сечения. Исследования некоторых более слабых по выразительным возможностям систем, таких как логика Гёделя-Лёба и логика транзитивного замыкания, могут рассматриваться как промежуточные шаги, необходимые для лучшего понимания проблематики, прежде, чем подступать к более сложной проблеме разработки циклического исчисления с конструктивно устранимым правилом сечения для модального мю-исчисления. Исследование нефундированных систем доказательств может привести к результатам о полноте нового типа для логик с неподвижными точками. Исследуя топологическую семантику логик доказуемости GLP и GLT, мы планируем получить результаты о глобальной полноте для этих систем, расширенных нефундированными выводами гильбертовского типа. Также планируется исследовать субструктурные логические системы с неподвижными точками, на примере исчисления Ламбека, расширенного итерацией Клини и субэкспоненциальными модальностями, и получить результаты о сложности (в различных смыслах) для систем с бесконечными и циклическими выводами. В отличие от многих модальных логик, в этом случае система с циклическими выводами строго слабее системы с бесконечными выводами, что сближает данную субструктурную логику с более сильными теориями, такими как формальная арифметика. Мы планируем найти формулировку удобного исчисления циклического типа в формальной арифметике, основанного на методе бесконечного спуска Ферма, с частичным устранением правила сечения. Для классической логики первого порядка в варианте Генцена будет получена элементарная процедура устранения сечения для выводов с одним правилом сечения для предваренных формул. Мы планируем построить исчисления со свойством подформульности для произвольных макросов, составленных из связок и кванторов. (Макросом называется составная логическая операция, представляющая собой комбинацию кванторов и логических связок, например “существует x такой, что для любого y …”) Также планируется построить исчисление со свойством подформульности для формальной арифметики с правилом индукции, основанное на представлении принципа наименьшего числа в эпсилон-исчислении Гильберта. Мы планируем разработать вариант исчисления рефлексий (строго позитивной модальной логики с операцией конъюнкции и модальностями “ромб”), допускающий интерпретацию принципами рефлексии арифметики второго порядка. Интерпретации формул этой системы должны соответствовать подтеориям теории BI и обладать свойствами редукции (утверждениями о консервативности, которые показывают, что исчисление рефлексий дает обозначения для “достаточно плотного” семейства подтеорий BI). Планируется использовать построенную систему для теоретико-доказательственного анализа BI средствами логики доказуемости. Предлагаемый вариант исчисления рефлексий должен будет дать альтернативную систему ординальных обозначений для ординала Бахмана-Говарда, в которой ординалы представлены формулами данного исчисления. Несмотря на то, что ординальный анализ для BI уже был ранее разработан в классических работах Г. Крайзеля, наш подход одновременно даст анализ для большого семейства подтеорий BI, и мы рассчитываем, что техника, разработанная для этого достаточно простого случая, в будущем может быть полезна для анализа более сильных подсистем арифметики второго порядка. Отметим, что что теоретико-доказательственный анализ полной арифметики второго порядка - это одна из важнейших и давно известных открытых задач теории доказательств. Мы ожидаем, что для любого n>0 и для любого истинного \Pi_{2n+1}-предложения F арифметики первого порядка существует рекурсивное вполне-упорядочение R порядкового типа \omega^n+1 такое, что итерация по R полной равномерной рефлексии влечет F. Также мы предполагаем, что для любого n>0 существует истинное \Pi_{2n}-предложение F такое, что для любого рекурсивного вполне-упорядочения R порядкового типа строго меньше \omega^n+1 предложение F не следует из итерации по R полной равномерной рефлексии. Предполагая, что эти две гипотезы удастся обосновать, мы планируем установить точную оценку длин рекурсивных вполне-упорядочений в классической теореме Фефермана о полноте.


 

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