Процедура доказательства - Proof procedure

В логике , и , в частности , теориях доказательств , процедура доказательства для данной логики является систематическим способом получения доказательств в некоторых доказательствах исчисления в (доказательной) отчетности.

Типы используемых исчислений доказательств

Есть несколько типов исчислений доказательств. Самыми популярными являются естественная дедукция , секвенциальные исчисления (т. Е. Системы типа Генцена ), системы Гильберта и семантические таблицы или деревья. Данная процедура доказательства будет нацелена на конкретное исчисление доказательств, но часто может быть переформулирована, чтобы получить доказательства в других стилях доказательства.

Полнота

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

Столкнувшись с недоказуемым утверждением, процедура полного доказательства может иногда успешно обнаружить и сигнализировать о его недоказуемости. В общем случае, когда доказуемость является полуразрешимым свойством, это невозможно, и вместо этого процедура будет расходиться (не завершаться).

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

Ссылки

  • В. Куайн 1982 (1950). Методы логики . Harvard Univ. Нажмите.