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