Теория доказательств - Proof theory

Теория доказательств это основная ветвь[1] из математическая логика что представляет доказательства как формальный математические объекты, облегчая их анализ математическими методами. Доказательства обычно представлены как индуктивно определенные структуры данных такие как простые списки, прямоугольные списки или деревья, построенные по аксиомы и правила вывода логической системы. Таким образом, теория доказательств синтаксический в природе, в отличие от теория моделей, который семантический в природе.

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

История

Хотя формализация логики значительно продвинулась благодаря работе таких деятелей, как Готтлоб Фреге, Джузеппе Пеано, Бертран Рассел, и Ричард Дедекинд, история современной теории доказательств часто рассматривается как основанная Дэвид Гильберт, кто инициировал то, что называется Программа Гильберта в основы математики. Центральная идея этой программы заключалась в том, что если бы мы могли дать финишный доказательства согласованности всех сложных формальных теорий, необходимых математикам, то мы могли бы обосновать эти теории с помощью метаматематического аргумента, который показывает, что все их чисто универсальные утверждения (более технически их доказуемые фразы ) конечно истинны; будучи обоснованными, мы не заботимся о нефинитарном значении их экзистенциальных теорем, рассматривая их как псевдо-значимые условия существования идеальных сущностей.

Сбой программы был вызван Курт Гёдель с теоремы о неполноте, который показал, что любой ω-последовательная теория который достаточно силен, чтобы выразить некоторые простые арифметические истины, не может доказать свою собственную непротиворечивость, что по формулировке Гёделя является предложение. Однако появились модифицированные версии программы Гильберта, и были проведены исследования по связанным темам. Это привело, в частности, к:

Параллельно с взлетом и падением программы Гильберта основы теория структурных доказательств были основаны. Ян Лукасевич предположил в 1926 году, что можно улучшить Системы Гильберта в качестве основы для аксиоматического представления логики, если позволять делать выводы из предположений в правилах вывода логики. В ответ на это Станислав Яськовский (1929) и Герхард Гентцен (1934) независимо предоставили такие системы, названные исчислениями естественный вычет, с подходом Генцена, вводящим идею симметрии между основаниями для утверждения предложений, выраженную в правила введения, и последствия принятия предложений в правила исключения, идея, которая оказалась очень важной в теории доказательств.[2] Генцен (1934) далее представил идею последовательное исчисление, исчисление, развитое в том же духе, которое лучше выражает двойственность логических связок,[3] и продолжил кардинальные успехи в формализации интуиционистской логики и предоставил первые комбинаторное доказательство согласованности Арифметика Пеано. Вместе представление естественного вывода и исчисления секвенций представило фундаментальную идею аналитическое доказательство к теории доказательств.

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

Основная статья: Структурная теория доказательства

Теория структурных доказательств - это раздел теории доказательств, изучающий особенности исчисления доказательств. Три самых известных стиля исчислений доказательств:

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

Теоретиков доказательства обычно интересуют исчисления доказательств, поддерживающие понятие аналитическое доказательство. Понятие аналитического доказательства было введено Генценом для исчисления секвенций; там аналитические доказательства - это те, которые без обрезков. Большая часть интереса к доказательствам без срезов происходит из свойства подформулы: каждая формула в конечной секвенции доказательства без сечения является подформулой одной из посылок. Это позволяет легко продемонстрировать непротиворечивость исчисления последовательностей; если бы пустая секвенция могла быть выведена, она должна была бы быть подформулой некоторой посылки, а это не так. Теорема Гентцена о средней части, интерполяционная теорема Крейга и теорема Эрбрана также следуют как следствия теоремы об исключении сечения.

Исчисление естественной дедукции Генцена также поддерживает понятие аналитического доказательства, как показано Даг Правиц. Определение немного сложнее: мы говорим, что аналитические доказательства - это нормальные формы, которые связаны с понятием нормальной формы при переписывании терминов. Более экзотические исчисления доказательств, такие как Жан-Ив Жирар с сети доказательства также поддерживают понятие аналитического доказательства.

Особое семейство аналитических доказательств, возникающих в редуктивная логика находятся целенаправленные доказательства которые характеризуют большое семейство целенаправленных процедур поиска доказательств. Способность преобразовывать систему доказательств в сфокусированную форму является хорошим показателем ее синтаксического качества, подобно тому, как допустимость сокращения показывает, что система доказательства синтаксически непротиворечива.[4]

Теория структурных доказательств связана с теория типов с помощью Переписка Карри – Ховарда, в котором наблюдается структурная аналогия между процессом нормализации в исчислении естественной дедукции и бета-редукцией в типизированное лямбда-исчисление. Это обеспечивает основу для интуиционистская теория типов разработан Пер Мартин-Лёф, и часто расширяется до трехсторонней корреспонденции, третьей стороной которой являются декартово закрытые категории.

Другие темы исследований в теории структур включают аналитические таблицы, которые применяют центральную идею аналитического доказательства из теории структурных доказательств для обеспечения процедур принятия решений и процедур полурешения для широкого диапазона логик, а также теорию доказательства субструктурных логик.

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

Основная статья: Порядковый анализ

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

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

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

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

Основная статья: Логика доказуемости

Логика доказуемости это модальная логика, в котором оператор бокса интерпретируется как «это доказуемо». Дело в том, чтобы уловить понятие предиката доказательства достаточно богатого формальная теория. В качестве основных аксиом логики доказуемости GL (Гёдель -Лёб ), который захватывает доказуемое в Арифметика Пеано, взяты модальные аналоги условий выводимости Гильберта-Бернейса и Теорема Лёба (если доказуемо, что из доказуемости A следует A, то A доказуемо).

Некоторые из основных результатов, касающихся неполноты арифметики Пеано и связанных с ней теорий, имеют аналоги в логике доказуемости. Например, в GL есть теорема о том, что если противоречие недоказуемо, то нельзя доказать, что противоречие недоказуемо (вторая теорема Гёделя о неполноте). Существуют также модальные аналоги теоремы о неподвижной точке. Роберт Соловей доказал, что модальная логика GL полна относительно арифметики Пеано. То есть пропозициональная теория доказуемости в арифметике Пеано полностью представлена ​​модальной логикой GL. Это прямо означает, что пропозициональное рассуждение о доказуемости в арифметике Пеано является полным и разрешимым.

Другое исследование логики доказуемости было сосредоточено на логике доказуемости первого порядка, полимодальная логика доказуемости (одна модальность представляет доказуемость в теории объектов, а другая - доказуемость в метатеории), и логика интерпретируемости предназначен для отражения взаимодействия между доказуемостью и интерпретируемостью. Некоторые совсем недавние исследования включали приложения градуированных алгебр доказуемости к порядковому анализу арифметических теорий.

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

Основная статья: Обратная математика

Обратная математика это программа в математическая логика который пытается определить, какие аксиомы необходимы для доказательства теорем математики.[5] Месторождение было основано Харви Фридман. Его метод определения можно описать как "движение назад от теоремы к аксиомы ", в отличие от обычной математической практики вывода теорем из аксиом. Программа обратной математики была предвосхищена результатами теории множеств, такими как классическая теорема о том, что аксиома выбора и Лемма Цорна эквивалентны по Теория множеств ZF. Однако цель обратной математики - изучить возможные аксиомы обычных теорем математики, а не возможные аксиомы теории множеств.

В обратной математике каждый начинает с каркасного языка и базовой теории - базовой системы аксиом, - которая слишком слаба для доказательства большинства интересующих вас теорем, но все же достаточно мощна, чтобы разработать определения, необходимые для формулировки этих теорем. Например, для изучения теоремы «Всякая ограниченная последовательность действительные числа имеет супремум «необходимо использовать базовую систему, которая может говорить о действительных числах и последовательностях действительных чисел.

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

Одним из поразительных явлений в обратной математике является надежность Большая Пятерка системы аксиом. В порядке возрастания силы эти системы названы инициализмами RCA.0, WKL0, ACA0, ATR0, и Π1
1-CA0. Почти каждая теорема обычной математики, которая подвергалась обратному математическому анализу, оказалась эквивалентной одной из этих пяти систем. Многие недавние исследования были сосредоточены на комбинаторных принципах, которые не вписываются в эту структуру, например RT2
2 (Теорема Рамсея для пар).

Исследования в области обратной математики часто включают методы и приемы из теория рекурсии а также теория доказательств.

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

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

Функциональные интерпретации также предоставляют способ извлекать конструктивную информацию из доказательств сокращенной теории. Как прямое следствие интерпретации обычно получается результат, что любая рекурсивная функция, совокупность которой может быть доказана либо в I, либо в C, представлена ​​членом F. Если можно дать дополнительную интерпретацию F в I, которая иногда бывает возможно, такая характеристика обычно оказывается точной. Часто оказывается, что члены F совпадают с естественным классом функций, такими как примитивно рекурсивные или вычислимые за полиномиальное время функции. Функциональные интерпретации также использовались для проведения порядкового анализа теорий и классификации их доказуемо рекурсивных функций.

Изучение функциональных интерпретаций началось с интерпретации Куртом Гёделем интуиционистской арифметики в бескванторной теории функционалов конечного типа. Эта интерпретация широко известна как Толкование диалектики. Вместе с интерпретацией двойного отрицания классической логики в интуиционистской логике она обеспечивает сведение классической арифметики к интуиционистской арифметике.

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

Основная статья: Формальное доказательство

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

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

Теоретико-доказательная семантика

Основные статьи: теоретико-доказательная семантика и логическая гармония

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

Смотрите также

Примечания

  1. ^ Согласно Вангу (1981), стр. 3–4, теория доказательств - это одна из четырех областей математической логики вместе с теория моделей, аксиоматическая теория множеств, и теория рекурсии. Barwise (1978) состоит из четырех соответствующих частей, причем часть D посвящена теории доказательств и конструктивной математике.
  2. ^ Правиц (2006), п. 98).
  3. ^ Жирар, Лафон и Тейлор (1988).
  4. ^ Чаудхури, Каустув; Марин, Соня; Straßburger, Lutz (2016), «Сфокусированные и синтетические вложенные секвенты», Конспект лекций по информатике, Берлин, Гейдельберг: Springer Berlin Heidelberg, стр. 390–407, Дои:10.1007/978-3-662-49630-5_23, ISBN  978-3-662-49629-9
  5. ^ Симпсон 2010

Рекомендации

внешняя ссылка