Исчисление доказательств
В математической логике исчисление доказательств или система доказательств создается для доказательства утверждений .
Обзор [ править ]
Система доказательств включает в себя следующие компоненты: [1] [2]
- Формальный язык : множество L формул, допускаемых системой, например, логика высказываний или логика первого порядка .
- Правила вывода : список правил, которые можно использовать для доказательства теорем на основе аксиом и теорем.
- Аксиомы : формулы в L считаются действительными. Все теоремы выводятся из аксиом.
Формальное доказательство в правильно построенной формулы системе доказательств представляет собой набор аксиом и правил вывода системы доказательств, из которых следует, что правильно сформированная формула является теоремой системы доказательств. [2]
Обычно данное исчисление доказательств охватывает более чем одну конкретную формальную систему, поскольку многие исчисления доказательств недоопределены и могут использоваться для радикально разных логик. Например, парадигматическим случаем является секвенциальное исчисление , которое можно использовать для выражения отношений следствий как интуиционистской логики , так и логики релевантности . Таким образом, грубо говоря, исчисление доказательств — это шаблон или шаблон проектирования , характеризующийся определенным стилем формального вывода, который может быть специализирован для создания конкретных формальных систем, а именно путем указания фактических правил вывода для такой системы. Среди логиков нет единого мнения о том, как лучше всего определить этот термин.
доказательств Примеры
Наиболее широко известными исчислениями доказательства являются те классические исчисления, которые до сих пор широко используются:
- Класс гильбертовых систем , [2] наиболее известным примером которой является Гильберта – Аккермана система логики первого порядка 1928 года ;
- Герхарда Генцена исчисление естественной дедукции , которое является первым формализмом структурной теории доказательств и краеугольным камнем соответствия формул как типов, связывающих логику с функциональным программированием ;
- Генцена Секвенциальное исчисление — наиболее изученный формализм теории структурных доказательств.
Многие другие исчисления доказательств были или могли быть плодотворными, но сегодня они широко не используются.
- исчисление Аристотеля Силлогистическое , , представленное в «Органоне» легко допускает формализацию. В настоящее время все еще существует некоторый интерес к силлогизмам, осуществляемый под эгидой терминологической логики .
- 1879), сделанная Готтлобом Фреге, Двумерная запись Begriffsschrift ( обычно рассматривается как введение в логику современной концепции квантора .
- Пирса К.С. Экзистенциальный график легко мог бы стать плодотворным, если бы история сложилась иначе.
Современные исследования в области логики изобилуют конкурирующими исчислениями доказательств:
- Было предложено несколько систем, которые заменяют обычный текстовый синтаксис графическим синтаксисом. сети доказательств и циркуляторное исчисление относятся к числу таких систем.
- В последнее время многие логики, интересующиеся теорией структурных доказательств, предложили исчисления с глубоким выводом , например, логику отображения , гиперсеквенции , исчисление структур и групповую импликацию .
См. также [ править ]
- Пропозициональная система доказательства
- Доказательственные сети
- Цирковое исчисление
- Расчет структур
- Формальное доказательство
- Метод аналитических таблиц
- Разрешение (логика)
Ссылки [ править ]
- ^ Анита Василевская. «Общие системы доказательств» (PDF) .
- ^ Перейти обратно: а б с «Определение: Система доказательств — ProofWiki» . prowiki.org . Проверено 16 октября 2023 г.