Исчисление доказательств

В математической логике исчисление доказательств или система доказательств создается для доказательства утверждений .

Обзор

Система доказательств включает в себя следующие компоненты:

• Формальный язык : множество L формул, допускаемых системой, например, логика высказываний или логика первого порядка .
• Правила вывода : список правил, которые можно использовать для доказательства теорем на основе аксиом и теорем.
• Аксиомы : формулы в L считаются действительными. Все теоремы выводятся из аксиом.

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

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

Примеры доказательств

Наиболее широко известными исчислениями доказательства являются те классические исчисления, которые до сих пор широко используются:

• Класс гильбертовых систем , наиболее известным примером которой является – Аккермана Гильберта система логики первого порядка 1928 года ;
• Герхарда Генцена Исчисление естественной дедукции , которое является первым формализмом структурной теории доказательств и краеугольным камнем соответствия формул как типов, связывающих логику с функциональным программированием ;
• Генцена Секвенциальное исчисление — наиболее изученный формализм теории структурных доказательств.

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

• Аристотеля Силлогистическое исчисление , представленное в « Органоне» , легко допускает формализацию. В настоящее время все еще существует некоторый интерес к силлогизмам, осуществляемый под эгидой терминологической логики .
• 1879), сделанная Готтлобом Фреге Двумерная запись Begriffsschrift ( , обычно рассматривается как введение в логику современной концепции квантора .
• К.С. Пирса легко Экзистенциальный график мог бы стать плодотворным, если бы история сложилась иначе.

Современные исследования в области логики изобилуют конкурирующими исчислениями доказательств:

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

См. также

• Пропозициональная система доказательства
• Доказательственные сети
• Цирковое исчисление
• Расчет структур
• Формальное доказательство
• Метод аналитических таблиц
• Разрешение (логика)