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

This article relies excessively on references to tertiary sources. Please improve this article by adding secondary or primary sources. Find sources: "Proof calculus" – news · newspapers · books · scholar · JSTOR (December 2024) (Learn how and when to remove this message)

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

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

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

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

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

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

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

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

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

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

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

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