Введение

Систематический логический процесс, способный выводить заключение из гипотез.

В философии логики и логике, правило вывода, правило инференции или правило преобразования — это логическая форма, состоящая из функции, которая принимает посылки, анализирует их синтаксис и возвращает заключение (или заключения). Например, правило вывода modus ponens принимает две посылки, одну в форме "Если p, то q" и другую в форме "p", и возвращает заключение "q". Правило является валидным по отношению к семантике классической логики (а также к семантике многих других неклассических логик) в том смысле, что если посылки истинны (при определенной интерпретации), то истинно и заключение. Как правило, правило вывода сохраняет истинность, являющуюся семантическим свойством. Во многих многозначных логиках оно сохраняет общее значение. Однако действие правила вывода чисто синтаксическое и не требует сохранения какого-либо семантического свойства: любая функция, отображающая множества формул в формулы, считается правилом вывода. Обычно важны только рекурсивные правила, то есть правила, для которых существует эффективная процедура определения того, является ли данная формула заключением из данного набора формул в соответствии с правилом. Примером правила, не являющегося эффективным в этом смысле, является бесконечное правило ω. Популярные правила вывода в пропозициональной логике включают modus ponens, modus tollens и контрапозицию. Логика предикатов первого порядка использует правила вывода для работы с логическими кванторами.

Допустимость и выводимость

В наборе правил правило вывода может быть избыточным в том смысле, что оно допустимо или выводимо. Выводимое правило – это правило, заключение которого может быть получено из его посылок с использованием других правил. Допустимым правилом является правило, заключение которого истинно всякий раз, когда истинны посылки. Все выводимые правила допустимы. Чтобы понять разницу, рассмотрим следующий набор правил для определения натуральных чисел (суждение утверждает факт, что является натуральным числом): первое правило утверждает, что 0 является натуральным числом, а второе – что s(n) является натуральным числом, если n является натуральным числом. В этой системе доказательств следующее правило, демонстрирующее, что второй преемник натурального числа также является натуральным числом, является выводимым: его вывод представляет собой композицию двух применений вышеуказанного правила преемника. Следующее правило для утверждения существования предшественника любого ненулевого числа является лишь допустимым: Это истинный факт о натуральных числах, который может быть доказан индукцией. (Чтобы доказать допустимость этого правила, предположим вывод посылки и проведём индукцию по нему, чтобы получить вывод .) Однако оно не является выводимым, поскольку зависит от структуры вывода посылки. В силу этого, выводимость устойчива при добавлении к системе доказательств, в то время как допустимость – нет. Чтобы увидеть разницу, предположим, что к системе доказательств было добавлено следующее бессмысленное правило: В этой новой системе правило двойного преемника по-прежнему выводимо. Однако правило нахождения предшественника больше не допустимо, поскольку нет способа вывести . Хрупкость допустимости обусловлена способом её доказательства: поскольку доказательство может опираться на структуру выводов посылок, расширения системы добавляют новые случаи к этому доказательству, которые могут оказаться неверными. Допустимые правила можно рассматривать как теоремы системы доказательств. Например, в исчислении секвенций, где выполняется устранение обрезания, правило обрезания допустимо.