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