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

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

Обзор

Система доказательств включает в себя компоненты: ^{[1] [2]}

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Анита Василевска. «Общие системы доказательств» (PDF) .
2. «Определение: Система доказательств — ProofWiki» . prowiki.org . Проверено 16 октября 2023 г.