Введение

Теория доказательств — это важная отрасль математической логики и теоретической информатики, в которой доказательства рассматриваются как формальные математические объекты, что позволяет анализировать их математическими методами. Доказательства обычно представляются в виде индуктивно определенных структур данных, таких как списки, списки в скобках или деревья, которые строятся в соответствии с аксиомами и правилами вывода заданной логической системы. Следовательно, теория доказательств носит синтаксический характер, в отличие от теории моделей, которая носит семантический характер. К основным областям теории доказательств относятся структурная теория доказательств, ординальный анализ, логика доказуемости, обратная математика, извлечение доказательств, автоматическое доказательство теорем и сложность доказательств. Значительная часть исследований также посвящена применению в информатике, лингвистике и философии.

Порядковый анализ

Ординальный анализ — мощный метод для предоставления комбинаторных доказательств согласованности подсистем арифметики, анализа и теории множеств. Вторая теорема о неполноте Гёделя часто интерпретируется как демонстрация невозможности финитистских доказательств согласованности для теорий достаточной силы. Ординальный анализ позволяет точно измерить инфинитарное содержание согласованности теорий. Для последовательной рекурсивно аксиоматизированной теории T можно доказать в финитистской арифметике, что обоснованность определенного трансфинитного ординала влечет согласованность T. Вторая теорема о неполноте Гёделя подразумевает, что обоснованность такого ординала не может быть доказана в теории T.

Следствия ординального анализа включают (1) согласованность подсистем классической арифметики второго порядка и теории множеств относительно конструктивных теорий, (2) результаты комбинаторной независимости и (3) классификацию доказуемо тотальных рекурсивных функций и доказуемо обоснованных ординалов. Ординальный анализ был разработан Гентценом, который доказал согласованность арифметики Пеано, используя трансфинитную индукцию до ординала ε0. Ординальный анализ был расширен на многие фрагменты арифметики первого и второго порядка и теории множеств. Одной из основных задач был ординальный анализ импредикативных теорий. Первым прорывом в этом направлении стало доказательство Такеути согласованности Π CA0 с использованием метода ординальных диаграмм.

Логика доказуемости

Логика доказуемости — это модальная логика, в которой оператор коробки интерпретируется как «это доказуемо». Цель состоит в том, чтобы отразить понятие предиката доказуемости для достаточно богатой формальной теории. В качестве основных аксиом логики доказуемости GL (Гёдель — Лёб), которая отражает доказуемость в арифметике Пеано, принимаются модальные аналоги условий выводимости Гильберта — Бернайса и теоремы Лёба (если доказуемо, что доказуемость A влечет A, то A доказуемо). Некоторые из основных результатов, касающихся неполноты арифметики Пеано и связанных с ней теорий, имеют аналоги в логике доказуемости. Например, в GL доказывается, что если противоречие не доказуемо, то не доказуемо, что противоречие не доказуемо (вторая теорема о неполноте Гёделя). Существуют также модальные аналоги теоремы о неподвижной точке. Роберт Соловэй доказал, что модальная логика GL полна относительно арифметики Пеано. То есть, пропозициональная теория доказуемости в арифметике Пеано полностью представлена модальной логикой GL. Это непосредственно подразумевает, что пропозициональное рассуждение о доказуемости в арифметике Пеано является полным и разрешимым. Другие исследования в логике доказуемости были сосредоточены на логике доказуемости первого порядка, полимодальной логике доказуемости (с одной модальностью, представляющей доказуемость в объектной теории, и другой, представляющей доказуемость в метатеории), и логиках интерпретируемости, предназначенных для отражения взаимодействия между доказуемостью и интерпретируемостью. Некоторые совсем недавние исследования включали применение алгебр градуированной доказуемости к ординальному анализу арифметических теорий.

Обратная математика

Обратная математика — это программа в математической логике, которая стремится определить, какие аксиомы необходимы для доказательства теорем математики. Эта область была основана Харви Фридманом. Её определяющий метод можно описать как «движение от теорем к аксиомам», в отличие от обычной математической практики вывода теорем из аксиом. Программа обратной математики была предвосхищена результатами в теории множеств, такими как классическая теорема о том, что аксиома выбора и лемма Зорна эквивалентны в теории множеств ZF. Однако целью обратной математики является изучение возможных аксиом для обычных теорем математики, а не возможных аксиом для теории множеств. В обратной математике начинают с языка фрейма и базовой теории — основной аксиоматической системы, которая слишком слаба для доказательства большинства интересующих теорем, но всё же достаточно мощна для разработки необходимых определений, чтобы сформулировать эти теоремы. Например, для изучения теоремы «Каждая ограниченная последовательность вещественных чисел имеет супремум» необходимо использовать базовую систему, которая оперирует вещественными числами и последовательностями вещественных чисел. Для каждой теоремы, которую можно сформулировать в базовой системе, но которая не доказуема в этой системе, цель состоит в том, чтобы определить конкретную систему аксиом (более сильную, чем базовая система), необходимую для её доказательства. Чтобы показать, что система S необходима для доказательства теоремы T, требуются два доказательства. Первое доказательство показывает, что T доказуема из S; это обычное математическое доказательство с обоснованием возможности его проведения в системе S. Второе доказательство, известное как обращение, показывает, что сама T влечёт S; это доказательство проводится в базовой системе. Обращение устанавливает, что никакая аксиоматическая система S′, расширяющая базовую систему, не может быть слабее S, при этом доказывая T.

Одним из поразительных явлений в обратной математике является устойчивость аксиомных систем «Большой пятёрки». В порядке возрастания силы эти системы обозначаются аббревиатурами RCA0, WKL0, ACA0, ATR0 и Π CA0. Почти каждая теорема обычной математики, подвергнутая анализу с помощью обратной математики, оказалась эквивалентной одной из этих пяти систем. Многие недавние исследования сосредоточены на комбинаторных принципах, которые не укладываются в эту структуру, например, RT (теорема Рамсея для пар). Исследования в области обратной математики часто включают методы и приёмы из теории рекурсии, а также теории доказательств.

Функциональные интерпретации

Функциональные интерпретации — это интерпретации неконструктивных теорий в функциональные. Обычно функциональные интерпретации осуществляются в два этапа. Сначала классическая теория C "приводится" к интуиционистской теории I. То есть, строится конструктивное отображение, переводящее теоремы C в теоремы I. Затем интуиционистская теория I приводится к кванторно-свободной теории функционалов F. Эти интерпретации вносят вклад в программу Гильберта, поскольку доказывают непротиворечивость классических теорий относительно конструктивных. Успешные функциональные интерпретации привели к приведению бесконечно-теоретических теорий к конечно-теоретическим и непредсказуемых теорий к предикативным. Функциональные интерпретации также предоставляют способ извлечения конструктивной информации из доказательств в приведённой теории. Как прямое следствие интерпретации, обычно получается результат о том, что любая рекурсивная функция, полнота которой может быть доказана либо в I, либо в C, представляется термом F. Если удаётся построить дополнительную интерпретацию F в I, что иногда возможно, эта характеристика обычно оказывается точной. Часто оказывается, что термы F совпадают с естественным классом функций, таким как примитивно рекурсивные или функции, вычислимые за полиномиальное время. Функциональные интерпретации также использовались для проведения ординального анализа теорий и классификации их доказуемо рекурсивных функций. Изучение функциональных интерпретаций началось с интерпретации Куртом Гёделем интуиционистской арифметики в кванторно-свободной теории функционалов конечного типа. Эта интерпретация обычно известна как диалектическая интерпретация. Вместе с интерпретацией двойного отрицания классической логики в интуиционистской логике она обеспечивает приведение классической арифметики к интуиционистской арифметике.

Формальные и неформальные доказательства

Неформальные доказательства, используемые в повседневной математической практике, отличаются от формальных доказательств в теории доказательств. Они скорее напоминают высокоуровневые наброски, которые позволили бы специалисту, при наличии достаточного времени и терпения, в принципе восстановить формальное доказательство. Для большинства математиков написание полностью формального доказательства слишком скрупулезно и громоздко, чтобы быть распространенной практикой. Формальные доказательства строятся с помощью компьютеров в рамках интерактивного доказательства теорем. Важно, что такие доказательства могут быть проверены автоматически, также с помощью компьютера. Проверка формальных доказательств обычно проста, в то время как нахождение доказательств (автоматическое доказательство теорем) как правило, является сложной задачей. В отличие от этого, неформальное доказательство, представленное в математической литературе, требует нескольких недель экспертной оценки для проверки и все равно может содержать ошибки.

Семантика теории доказательств

В лингвистике логическая грамматика типов, категориальная грамматика и грамматика Монтегю используют формализмы, основанные на теории структурных доказательств, для построения формальной семантики естественного языка.