Теория доказательств — это основная отрасль [1] математической логики и теоретической информатики , в которой доказательства рассматриваются как формальные математические объекты , что облегчает их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определяемых структур данных , таких как списки , коробочные списки или деревья , которые строятся в соответствии с аксиомами и правилами вывода данной логической системы. Следовательно, теория доказательств имеет синтаксическую природу, в отличие от теории моделей , которая имеет семантическую природу.
Некоторые из основных областей теории доказательств включают структурную теорию доказательств , порядковый анализ , логику доказуемости , обратную математику , интеллектуальный анализ доказательств , автоматическое доказательство теорем и сложность доказательства . Многие исследования также сосредоточены на приложениях в области информатики, лингвистики и философии.
Хотя формализация логики значительно продвинулась благодаря работам таких деятелей, как Готтлоб Фреге , Джузеппе Пеано , Бертран Рассел и Ричард Дедекинд , историю современной теории доказательств часто считают заложенной Давидом Гильбертом , который инициировал то, что называется гильбертовской теорией доказательств. Программа «Основы математики» . Центральная идея этой программы заключалась в том, что если бы мы могли дать финитарные доказательства непротиворечивости для всех сложных формальных теорий, необходимых математикам, то мы могли бы обосновать эти теории посредством метаматематического аргумента, который показывает, что все их чисто универсальные утверждения (более технически их доказуемые предложения ) финитно истинны; однажды обоснованные, нас не заботит нефинитный смысл их экзистенциальных теорем, считая их псевдозначимыми условиями существования идеальных сущностей.
Неудача программы была вызвана теоремами Курта Гёделя о неполноте , которые показали, что любая ω-непротиворечивая теория , достаточно сильная для выражения некоторых простых арифметических истин, не может доказать свою собственную непротиворечивость, что по формулировке Гёделя является предложением . Однако появились модифицированные версии программы Гильберта и были проведены исследования по смежным темам. Это привело, в частности, к:
Параллельно с взлетом и падением программы Гильберта закладывались основы теории структурных доказательств . Ян Лукасевич предположил в 1926 году, что можно было бы улучшить системы Гильберта как основу аксиоматического представления логики, если бы можно было делать выводы из допущений в правилах логического вывода. В ответ на это Станислав Ясковский (1929) и Герхард Генцен (1934) независимо предоставили такие системы, называемые исчислениями естественной дедукции , с подходом Генцена, вводящим идею симметрии между основаниями для утверждения суждений, выраженными в правилах введения , и следствиями. принятия предложений в правилах исключения — идея, которая оказалась очень важной в теории доказательств. [2] Генцен (1934) далее представил идею секвенциального исчисления , исчисления, выдвинутого в том же духе, которое лучше выражает двойственность логических связок, [3] и добился фундаментальных успехов в формализации интуиционистской логики, и предоставить первое комбинаторное доказательство непротиворечивости арифметики Пеано . Вместе представление естественной дедукции и секвенциального исчисления привнесло в теорию доказательств фундаментальную идею аналитического доказательства .
Структурная теория доказательств — это раздел теории доказательств, изучающий особенности исчисления доказательств . Три наиболее известных стиля исчисления доказательств:
Каждый из них может дать полную и аксиоматическую формализацию пропозициональной логики или логики предикатов классического или интуиционистского толка , почти любой модальной логики и многих субструктурных логик , таких как логика релевантности или линейная логика . Действительно, редко можно найти логику, которая сопротивляется представлению в одном из этих исчислений.
Теоретики доказательства обычно интересуются исчислениями доказательств, поддерживающими понятие аналитического доказательства . Понятие аналитического доказательства было введено Генценом для секвенциального исчисления; там аналитические доказательства — это те, которые не содержат разрезов . Большая часть интереса к доказательствам без разрезов связана сСвойство подформулы : каждая формула в конечной секвенции доказательства без разрезов является подформулой одной из посылок. Это позволяет легко показать непротиворечивость секвенциального исчисления; если бы пустая секвенция была выводима, она должна была бы быть подформулой некоторой посылки, а это не так. Теорема Генцена о средней секвенции, интерполяционная теорема Крейга и теорема Эрбрана также являются следствиями теоремы об исключении разреза.
Исчисление естественной дедукции Генцена также поддерживает идею аналитического доказательства, как показал Даг Правиц . Определение немного сложнее: мы говорим, что аналитические доказательства — это нормальные формы , которые связаны с понятием нормальной формы в переписывании терминов. Более экзотические исчисления доказательств, такие как сети доказательств Жан-Ива Жирара, также поддерживают понятие аналитического доказательства.
Особое семейство аналитических доказательств, возникающих в редуктивной логике, представляет собой целенаправленные доказательства , которые характеризуют большое семейство целенаправленных процедур поиска доказательств. Способность преобразовать систему доказательства в целенаправленную форму является хорошим показателем ее синтаксического качества, подобно тому, как допустимость сокращения показывает, что система доказательства синтаксически непротиворечива. [4]
Теория структурных доказательств связана с теорией типов посредством соответствия Карри-Ховарда , которое наблюдает структурную аналогию между процессом нормализации в исчислении естественной дедукции и бета-редукцией в типизированном лямбда-исчислении . Это обеспечивает основу интуиционистской теории типов, разработанной Пером Мартином-Лёфом , и часто расширяется до трехстороннего соответствия, третьей частью которого являются декартовы замкнутые категории .
Другие темы исследований в области структурной теории включают аналитические таблицы, которые применяют центральную идею аналитического доказательства из теории структурных доказательств для обеспечения процедур принятия решения и процедур полурешения для широкого спектра логик, а также теорию доказательства субструктурной логики.
Порядковый анализ — мощный метод обеспечения комбинаторных доказательств непротиворечивости подсистем арифметики, анализа и теории множеств. Вторую теорему Гёделя о неполноте часто интерпретируют как демонстрацию того, что финитистские доказательства непротиворечивости невозможны для теорий достаточной силы. Порядковый анализ позволяет точно измерить бесконечное содержание непротиворечивости теорий. Для непротиворечивой рекурсивно аксиоматизированной теории T можно доказать с помощью финитистской арифметики, что обоснованность определенного трансфинитного ординала влечет за собой непротиворечивость Т. Вторая теорема Гёделя о неполноте означает, что обоснованность такого ординала не может быть доказана в теории Т.
Последствия порядкового анализа включают (1) непротиворечивость подсистем классической арифметики второго порядка и теории множеств относительно конструктивных теорий, (2) результаты комбинаторной независимости и (3) классификации доказуемо полных рекурсивных функций и доказуемо обоснованных ординалов.
Порядковый анализ был предложен Генценом, который доказал непротиворечивость арифметики Пеано с помощью трансфинитной индукции до порядкового ε 0 . Порядковый анализ был распространен на многие фрагменты арифметики первого и второго порядка и теории множеств. Одной из основных проблем был порядковый анализ импредикативных теорий. Первым прорывом в этом направлении стало доказательство Такеути непротиворечивости Π1
1-CA 0 с использованием метода порядковых диаграмм.
Логика доказуемости — это модальная логика , в которой оператор поля интерпретируется как «доказуемо, что». Цель состоит в том, чтобы уловить понятие предиката доказательства достаточно богатой формальной теории . В качестве основных аксиом логики доказуемости GL ( Gödel - Löb ), охватывающей доказуемое в арифметике Пеано , берутся модальные аналоги условий выводимости Гильберта-Бернейса и теоремы Лёба (если доказуемо, что из доказуемости A следует A, то A доказуемо).
Некоторые из основных результатов, касающихся неполноты арифметики Пеано и связанных с ней теорий, имеют аналоги в логике доказуемости. Например, в GL существует теорема о том, что если противоречие недоказуемо, то невозможно доказать, что противоречие недоказуемо (вторая теорема Гёделя о неполноте). Существуют также модальные аналоги теоремы о неподвижной точке. Роберт Соловей доказал, что модальная логика GL полна относительно арифметики Пеано. То есть пропозициональная теория доказуемости в арифметике Пеано полностью представлена модальной логикой GL. Это прямо означает, что пропозициональные рассуждения о доказуемости в арифметике Пеано полны и разрешимы.
Другие исследования в области логики доказуемости были сосредоточены на логике доказуемости первого порядка, полимодальной логике доказуемости (одна модальность представляет доказуемость в теории объекта, а другая представляет доказуемость в метатеории) и логике интерпретируемости , предназначенной для отражения взаимодействия между доказуемостью и интерпретируемостью. . Некоторые совсем недавние исследования включали применение градуированных алгебр доказуемости к порядковому анализу арифметических теорий.
Обратная математика — это программа математической логики , которая пытается определить, какие аксиомы необходимы для доказательства математических теорем. [5] Эту область основал Харви Фридман . Его метод определения можно охарактеризовать как «движение назад от теорем к аксиомам », в отличие от обычной математической практики вывода теорем из аксиом. Программа обратной математики была предвосхищена результатами в теории множеств, такими как классическая теорема о том, что аксиома выбора и лемма Цорна эквивалентны в теории множеств ZF . Однако целью обратной математики является изучение возможных аксиом обычных теорем математики, а не возможных аксиом теории множеств.
В обратной математике каждый начинает с базового языка и базовой теории — базовой системы аксиом, — которая слишком слаба, чтобы доказать большинство теорем, которые могут вас заинтересовать, но все же достаточно мощна, чтобы разработать определения, необходимые для формулировки этих теорем. Например, для изучения теоремы «Всякая ограниченная последовательность действительных чисел имеет верхнюю границу » необходимо использовать базовую систему, которая может говорить о действительных числах и последовательностях действительных чисел.
Для каждой теоремы, которая может быть сформулирована в базовой системе, но не доказуема в базовой системе, цель состоит в том, чтобы определить конкретную систему аксиом (более сильную, чем базовая система), которая необходима для доказательства этой теоремы. Чтобы показать, что для доказательства теоремы T требуется система S , требуются два доказательства. Первое доказательство показывает, что T доказуемо из S ; это обычное математическое доказательство вместе с обоснованием того , что оно может быть проведено в системе S. Второе доказательство, известное как обращение , показывает, что T само по себе влечет S ; это доказательство проводится в базовой системе. Обращение устанавливает, что никакая система аксиом S' , расширяющая базовую систему, не может быть слабее, чем S , и в то же время доказывать T .
Одним из поразительных явлений в обратной математике является надежность систем аксиом «Большой пятерки» . В порядке возрастания силы эти системы называются инициализмами RCA 0 , WKL 0 , ACA 0 , ATR 0 и Π.1
1-КА 0 . Почти каждая теорема обычной математики, подвергнутая обратному математическому анализу, оказалась эквивалентной одной из этих пяти систем. Многие недавние исследования были сосредоточены на комбинаторных принципах, которые не вписываются в эту структуру, например, RT2
2(теорема Рамсея для пар).
Исследования в области обратной математики часто включают методы и приемы теории рекурсии , а также теории доказательств.
Функциональные интерпретации – это интерпретации неконструктивных теорий в функциональных. Функциональные интерпретации обычно проходят в два этапа. Во-первых, классическую теорию C «сводят» к интуиционистской теории I. То есть обеспечивают конструктивное отображение, которое переводит теоремы C в теоремы I. Во-вторых, интуиционистскую теорию I сводят к свободной от кванторов теории теории I. функционалы F. Эти интерпретации вносят вклад в форму программы Гильберта, поскольку доказывают непротиворечивость классических теорий относительно конструктивных. Успешные функциональные интерпретации привели к сведению бесконечных теорий к финитным теориям, а непредикативных теорий к предикативным.
Функциональные интерпретации также дают возможность извлечь конструктивную информацию из доказательств сокращенной теории. Как прямое следствие интерпретации обычно получается, что любая рекурсивная функция, совокупность которой может быть доказана либо в I, либо в C, представлена термом из F. Если можно дать дополнительную интерпретацию F в I, что иногда возможно, эта характеристика на самом деле обычно оказывается точной. Часто оказывается, что члены F совпадают с естественным классом функций, например примитивно-рекурсивными или полиномиально вычислимыми функциями. Функциональные интерпретации также использовались для проведения порядкового анализа теорий и классификации их доказуемо рекурсивных функций.
Изучение функциональных интерпретаций началось с интерпретации Куртом Гёделем интуиционистской арифметики в бескванторной теории функционалов конечного типа. Эта интерпретация широко известна как интерпретация диалектики . Вместе с интерпретацией классической логики методом двойного отрицания в интуиционистской логике это обеспечивает сведение классической арифметики к интуиционистской арифметике.
Неформальные доказательства повседневной математической практики отличаются от формальных доказательств теории доказательств. Они скорее похожи на эскизы высокого уровня, которые позволили бы эксперту восстановить формальное доказательство, по крайней мере в принципе, при наличии достаточного времени и терпения. Для большинства математиков написание полностью формального доказательства слишком педантично и многословно, чтобы его можно было использовать повсеместно.
Формальные доказательства строятся с помощью компьютеров в интерактивном доказательстве теорем . Примечательно, что эти доказательства могут быть проверены автоматически, в том числе с помощью компьютера. Проверка формальных доказательств обычно проста, тогда как найти доказательства ( автоматическое доказательство теорем ) обычно сложно. Неофициальное доказательство в математической литературе, напротив, требует нескольких недель рецензирования и все равно может содержать ошибки.
В лингвистике типологическая грамматика, категориальная грамматика и грамматика Монтегю применяют формализмы, основанные на теории структурных доказательств, для придания формальной семантики естественного языка .
