Процедура доказательства
В логике и, в частности, в теории доказательств , процедура доказательства для данной логики — это систематический метод получения доказательств в некотором исчислении доказательств (доказуемых) утверждений.
Типы используемых доказательств
[ редактировать ]Существует несколько типов исчислений доказательств. Наиболее популярными являются естественная дедукция , секвенциальные исчисления (т.е. системы типа Генцена ), системы Гильберта и семантические таблицы или деревья. Данная процедура доказательства будет нацелена на конкретное исчисление доказательств, но часто может быть переформулирована для получения доказательств в других стилях доказательства.
Полнота
[ редактировать ]Процедура доказательства логики является полной , если она дает доказательство для каждого доказуемого утверждения. Теоремы рекурсивно логических систем обычно перечислимы , что предполагает существование полной, но обычно крайне неэффективной процедуры доказательства; однако процедура доказательства представляет интерес только в том случае, если она достаточно эффективна.
Столкнувшись с недоказуемым утверждением, процедура полного доказательства иногда может успешно обнаружить и сигнализировать о его недоказуемости. В общем случае, когда доказуемость является лишь полуразрешимым свойством, это невозможно, и вместо этого процедура будет расходиться (а не завершаться).
См. также
[ редактировать ]Ссылки
[ редактировать ]- Уиллард Куайн 1982 (1950). Методы логики . Гарвардский университет. Нажимать.