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

Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики^[1]. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории^[2].

Теория доказательств важна для философской логики, где самостоятельный интерес представляет идея теоретико-доказательственной семантики, — идея, которая основана на осуществимости формально-логических методов структурной теории доказательств.

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

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

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

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

Три самых известных видов исчислений доказательства:

• Исчисления Гильберта
• Исчисления натуральной дедукции
• Исчисления секвенций

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

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

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

Структурная теория доказательства — раздел теории доказательства, в котором изучают те исчисления доказательств, которые поддерживают понятие аналитического доказательства. Понятие аналитического доказательства было введено Генценом для исчисления секвенций. Его исчисление натуральной дедукции также поддерживает понятие аналитического доказательства. Мы говорим, что аналитические доказательства суть нормальные формы, связанные с понятием нормальной формы в системах переписывании термов. Более экзотические исчисления доказательств, типа сетей доказательств И.Джиро, также поддерживают понятие аналитического доказательства.

Структурная теория доказательства связана с теорией типов посредством соответствия Карри-Говарда, которое основано на структурной аналогии между процессом нормализации в исчислении натуральной дедукции и бета-редукцией типизированного лямбда-исчисления. Это соответствие обеспечивает основу для интуиционистской теории типа, развитой М.-Лефом, и часто расширяется на тройственное соответствие, третья опора которого — декартово замкнутые категории.

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

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

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

Г. Генценом был вычислен ординал первопорядковой арифметики Пеано ${\displaystyle PA}$ — он установил, что непротиворечивость ${\displaystyle PA}$ может быть доказана трансфинитной индукцией до ординала ${\displaystyle \varepsilon _{0}}$. Дальнейшие исследования показали, что ${\displaystyle PA}$ доказывает принцип трансфинитной индукции для ординалов меньших ${\displaystyle \varepsilon _{0}}$, но не для самого ординала ${\displaystyle \varepsilon _{0}}$ и, что вычислимые функции, всюду — определённость которых может быть доказана в ${\displaystyle PA}$, совпадают с ${\displaystyle \varepsilon _{0}}$-рекурсивными функциями. Хотя, общем случае, для других теорий аналоги этих результатов не обязаны иметь место одновременно для одного и того же ординала, для естественных достаточно сильных теорий, как правило, аналоги этих результатов не дают разных ординалов для одной и той же теории (как впрочем и другие подходы к определению теоретико-доказательственного ординала).

Теоретико-доказательственные ординалы были вычислены для ряда фрагментов арифметики второго порядка и расширений теории множеств Крипке-Платека. До сих пор остаётся открытым вопрос о вычислении теоретико-доказательственного ординала полной арифметики второго порядка и более сильных теорий, в частности, теории множеств Цермело-Френкеля ${\displaystyle ZFC}$

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

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

• Такеути Г. Теория доказательств. — М.: Мир, 1978. — 412 с.
• Хао Ван (1981) Популярные лекции по математической логике. ISBN 0-442-23109-1.
• Д. Барвайз (редактор, 1978). Справочник по математической логике, тт. 1 — 4.
• Г. Такеути. Теория доказательств. М., Мир, 1978
• A. Трулстра (1996). Базовая теория доказательств. В серии: Трактаты Кембриджа по Теоретической Информатике, Университет Кембриджа, ISBN 0-521-77911-1.
• Д. фон Плато (2008). Развитие теории доказательств. Стэнфордская Энциклопедия Философии.