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

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

Обзор

Система проверки включает в себя компоненты:^[1]

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

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

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

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

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

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

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

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

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

Смотрите также

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

Рекомендации

1. Анита Василевская. «Общие системы доказательства» (PDF).