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

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

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

История

Хотя формализация логики значительно продвинулась благодаря работам таких деятелей, как Готтлоб Фреге , Джузеппе Пеано , Бертран Рассел и Ричард Дедекинд , история современной теории доказательств часто рассматривается как заложенная Давидом Гильбертом , который инициировал то, что называется гильбертовской теорией доказательств. Программа « Основы математики» . Центральная идея этой программы заключалась в том, что если бы мы могли дать финитарные доказательства непротиворечивости для всех сложных формальных теорий, необходимых математикам, то мы могли бы обосновать эти теории посредством метаматематического аргумента, который показывает, что все их чисто универсальные утверждения (более технически их доказуемо $\Pi _{1}^{0}$ предложения ) окончательно истинны; однажды обоснованные, нас не заботит нефинитный смысл их экзистенциальных теорем, считая их псевдозначимыми условиями существования идеальных сущностей.

Неудача программы была вызвана теоремами Курта Гёделя о неполноте , которые показали, что любая ω-непротиворечивая теория , достаточно сильная для выражения некоторых простых арифметических истин, не может доказать свою собственную непротиворечивость, что по формулировке Гёделя является $\Pi _{1}^{0}$ предложение. Однако появились модифицированные версии программы Гильберта и были проведены исследования по смежным темам. Это привело, в частности, к:

• Уточнение результата Гёделя, в частности уточнение Дж. Баркли Россера , ослабляющее указанное выше требование ω-непротиворечивости до простой непротиворечивости;
• Аксиоматизация ядра результата Гёделя в терминах модального языка, логики доказуемости ;
• Трансфинитная итерация теорий Алана Тьюринга и Соломона Фефермана ;
• Открытие самопроверяющихся теорий , систем, достаточно сильных, чтобы говорить о себе, но слишком слабых, чтобы провести диагональный аргумент , который является ключом к аргументу Гёделя о недоказуемости.

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

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

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

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

• Исчисление Гильберта
• Естественные дедуктивные исчисления
• Последующие исчисления

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

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

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

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

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

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

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

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

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

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

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

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

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

Логика доказуемости — это модальная логика , в которой оператор коробки интерпретируется как «доказуемо, что». Цель состоит в том, чтобы уловить понятие предиката доказательства достаточно богатой формальной теории . В качестве основных аксиом логики доказуемости GL ( Gödel - Löb ), охватывающей доказуемое в арифметике Пеано , берутся модальные аналоги условий выводимости Гильберта-Бернейса и теоремы Лёба (если доказуемо, что из доказуемости A следует A, то A доказуемо).

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

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

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

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

Обратная математика — это программа математической логики , которая пытается определить, какие аксиомы необходимы для доказательства математических теорем. Поле было основано Харви Фридманом . Его метод определения можно описать как «движение назад от теорем к аксиомам », в отличие от обычной математической практики вывода теорем из аксиом. Программа обратной математики была предвосхищена результатами в теории множеств, такими как классическая теорема о том, что аксиома выбора и лемма Цорна эквивалентны в теории множеств ZF . Однако целью обратной математики является изучение возможных аксиом обычных математических теорем, а не возможных аксиом теории множеств.

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

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

Одним из поразительных явлений в обратной математике является надежность систем аксиом «Большой пятерки» . В порядке возрастания силы эти системы называются инициализмами RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ и Π. ¹
₁ -СА ₀ . Почти каждая теорема обычной математики, подвергнутая обратному математическому анализу, оказалась эквивалентной одной из этих пяти систем. Многие недавние исследования были сосредоточены на комбинаторных принципах, которые не вписываются в эту структуру, например, RT ²
₂ (теорема Рамсея для пар).

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

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

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

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

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

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

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

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

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

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

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

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

См. также

• Промежуточная логика
• Теория моделей
• Доказательство (правда)
• Методы доказательства
• Секвенционное исчисление

Ссылки

• Дж. Авигад и Э. Х. Рек (2001). «'Прояснение природы бесконечного': развитие метаматематики и теории доказательств ». Технический отчет Карнеги-Меллона CMU-PHIL-120.
• Дж. Барвайз , изд. (1978). Справочник по математической логике . Северная Голландия.
• С. Басс, изд. (1998) Справочник по теории доказательств . Эльзевир.
• Г. Генцен (1935/1969). « Исследования по логической дедукции ». В М. Е. Сабо, изд. Сборник статей Герхарда Генцена . Северная Голландия. Перевод Сабо из «Исследований по логическим рассуждениям», Mathematical Journal v. 39, стр. 176–210, 405 431.
• Ж.-Ю. Жирар , П. Тейлор, Ю. Лафон (1988). «Доказательства и типы» . Издательство Кембриджского университета. ISBN   0-521-37181-3
• Д. Правиц (1965). Естественная дедукция: исследование теории доказательств , Dover Publications, ISBN   978-0-486-44655-4
• С.Г. Симпсон (2010). Подсистемы арифметики второго порядка , второе издание. Издательство Кембриджского университета, ISBN   978-0521150149 .
• А.С. Троелстра и Х. Швихтенберг (1996). Основная теория доказательств , Кембриджские трактаты по теоретической информатике, издательство Кембриджского университета, ISBN   0-521-77911-1 .
• Х. Ван (1981). Популярные лекции по математической логике , Компания Ван Ностранд Рейнхольд , ISBN   0-442-23109-1 .

Внешние ссылки

• «Теория доказательств» , Энциклопедия математики , EMS Press , 2001 [1994]
• Дж. фон Платон (2008). Развитие теории доказательств . Стэнфордская энциклопедия философии .