Теория доказательств — раздел математической логики, представляющий доказательства в виде формальных математических объектов, осуществляя их анализ с помощью математических методов. Доказательства обычно представляются в виде индуктивно определённых структур данных, таких как списки и деревья, созданных в соответствии с аксиомами и правилами вывода формальных систем. Таким образом, теория доказательств является синтаксической, в отличие от семантической теории моделей. Вместе с теорией моделей, аксиоматической теорией множеств и теорией вычислений, теория доказательств является одним из так называемых «четырёх столпов» математики[1]. Теория доказательств использует точное определение понятия доказательства при доказательстве невозможности доказательства того или иного предложения в рамках заданной математической теории.[2]
Теория доказательств важна для философской логики, где самостоятельный интерес представляет идея теоретико-доказательственной семантики, — идея, которая основана на осуществимости формально-логических методов структурной теории доказательств.
Хотя формализация логики была значительно продвинута работами таких авторов как Г. Фреге, Дж. Пеано, Б. Расселл и Р. Дедекинд, история современной теории доказательств обычно рассматривается как начатая Д. Гильбертом, который инициировал то, что названо программой Гильберта для оснований математики. Оригинальные работы Курта Гёделя по теории доказательств сначала продвинули, а затем опровергли эту программу: его теорема полноты первоначально казалась хорошим предзнаменованием для цели Гильберта представить всю математику как финитную формальную систему; однако затем его теоремы неполноты показали, что эта цель недостижима. Вся эта работа была выполнена с исчислениями доказательств, названными системами Гильберта.
Параллельно разрабатывались основания структурной теории доказательств. Ян Лукасевич предположил в 1926, что можно улучшить системы Гильберта как базис аксиоматического представления логики, если варьировать вывод заключений из предположений правилами вывода. В развитие этой идеи С.Янковский (1929) и Г. Генцен (1934) независимо создали системы, названные исчислениями натуральной дедукции (естественного вывода), сочетая их с подходом Генцена, вводящим идею симметрии между предположениями о высказываниях в правилах введения, и следствиями принятия высказываний в правилах удаления, — идею, которая оказалась очень важной в теории доказательств. Генцен (1934) в дальнейшем ввёл так называемые исчисления секвенций, которые лучше выражали дуальность логических связок, и продолжал делать фундаментальные вклады в формализацию интуиционистской логики; он также обеспечил первое комбинаторное доказательство непротиворечивости арифметики Пеано. Разработка натуральной дедукции и исчисления секвенций ввели в теорию доказательств фундаментальную идею аналитического доказательства.