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

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

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

История [ править ]

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

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

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

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

Теория структурных доказательств [ править ]

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

• Гильберт исчисления
• Естественный вычет исчисления
• Последовательные исчисления

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

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

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

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

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

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

Порядковый анализ [ править ]

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

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

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

Логика доказуемости [ править ]

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

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

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

Обратная математика [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. Также [ править ]

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

Заметки [ править ]

Ссылки [ править ]

• Дж. Авигад и Э. Х. Рек (2001). «'Разъяснение природы бесконечного': развитие метаматематики и теории доказательств ». Технический отчет Карнеги-Меллона CMU-PHIL-120.
• Дж. Барвайз , изд. (1978). Справочник по математической логике . Северная Голландия.
• С. Бусс, изд. (1998) Справочник по теории доказательств . Эльзевир.
• А.С. Трельстра и Х. Швихтенберг (1996). Основная теория доказательства , Кембриджские трактаты по теоретической информатике, издательство Кембриджского университета, ISBN 0-521-77911-1 . 
• Г. Генцен (1935/1969). « Исследования по логической дедукции ». В М.Е. Сабо, изд. Собрание статей Герхарда Гентцена . Северная Голландия. Перевод Сабо из "Untersuchungen über das logische Schliessen", Mathematisches Zeitschrift v. 39, pp. 176–210, 405 431.
• Д. Правиц (1965). Естественная дедукция: теоретико-доказательное исследование , Dover Publications, ISBN 978-0-486-44655-4 
• С.Г. Симпсон (2010). Подсистемы арифметики второго порядка , второе издание. Издательство Кембриджского университета, ISBN 978-0521150149 . 
• Х. Ван (1981). Популярные лекции по математической логике , компания Van Nostrand Reinhold , ISBN 0-442-23109-1 . 

Внешние ссылки [ править ]

Викискладе есть медиафайлы, связанные с теорией доказательств .

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