Исчисление доказательств - Proof calculus
В математической логике , доказательство исчисление или доказательство система построена , чтобы доказать заявления.
Обзор
Система проверки включает в себя компоненты:
- Язык: набор формул, допускаемых системой, например, логика высказываний или логика первого порядка .
- Правила вывода : список правил, которые можно использовать для доказательства теорем из аксиом и теорем.
- Аксиомы : Предполагается, что формулы в L действительны. Все теоремы выводятся из аксиом.
Обычно данное исчисление доказательств охватывает более одной конкретной формальной системы, поскольку многие исчисления доказательств недоопределены и могут использоваться для радикально различных логик. Например, парадигматическим случаем является исчисление секвенций , которое можно использовать для выражения отношений последствий как интуиционистской логики, так и логики релевантности . Таким образом, грубо говоря, исчисление доказательств - это шаблон или шаблон проектирования , характеризующийся определенным стилем формального вывода, который может быть специализирован для создания конкретных формальных систем, а именно путем определения фактических правил вывода для такой системы. Среди логиков нет единого мнения о том, как лучше всего определить этот термин.
Примеры исчислений доказательств
Наиболее широко известные исчисления доказательств - это те классические исчисления, которые все еще широко используются:
- Класс Гильберта систем , из которых наиболее известным примером является 1928 Гильберта-Аккермана система из логики первого порядка ;
- Исчисление естественной дедукции Герхарда Генцена , которое является первым формализмом структурной теории доказательства и краеугольным камнем соответствия формул как типов, связывающего логику с функциональным программированием ;
- Исчисление секвенций Генцена , которое является наиболее изученным формализмом теории структурных доказательств.
Многие другие исчисления доказательств были или могли быть основополагающими, но сегодня широко не используются.
- Аристотель «s силлогистическая исчисление, представлены в Organon , легко допускает формализацию. Существует еще некоторые современные интересы силлогистики, осуществляется под эгидой в перспективе логики .
- Двумерное обозначение Готтлобом Фреге Begriffsschrift (1879) обычно рассматривается как введение современной концепции квантора в логику.
- CS Пирс «s экзистенциальный граф легко мог бы семенным, были история работала по - разному.
Современные исследования в области логики изобилуют конкурирующими исчислениями доказательств:
- Было предложено несколько систем, которые заменяют обычный текстовый синтаксис некоторым графическим синтаксисом. К числу таких систем относятся сети доказательств и круговое исчисление .
- В последнее время многие логики, интересующиеся теорией структурных доказательств , предложили исчисления с глубоким выводом , например логику отображения , гиперсеквенты , исчисление структур и сгруппированную импликацию .
Смотрите также
- Система пропозициональных доказательств
- Доказательства сети
- Циркулярное исчисление
- Расчет конструкций
- Формальное доказательство
- Метод аналитических таблиц
- Разрешение (логика)