Вывода Правило

Способ порождения объектов, называемых заключением В. п., по множеству объектов, называемых посылками правила; формулирование В. п. играет решающую роль при описании исчислений (часто данное В. п. имеет смысл лишь в контексте данного исчисления). Для исчислений, снабженных семантикой (в частности, большинства логико-математических исчислений), В. п. сохраняет истинность, т. е. по истинным посылкам позволяет породить лишь истинное заключение; наиболее знаменитый пример такого В. п.- правило модус поненс. В большинстве изучавшихся исчислений всякое применение В. п. имеет лишь конечное число посылок (важнейшее исключение — Карнапа правило), обычно число посылок данного В. п. остается неизменным для всех его применений. Количество возможных применений данного В. п. бывает, как правило, неограниченным. Способы формулирования В. п. весьма разнообразны, они зависят от языка исчисления и включают переменные различных типов. Подавляющее большинство используемых В. п. может быть порождено по следующей общей схеме: выбирая алфавит А, не содержащий буквы , и натуральное число l, называют l-посылочным В. п. нек-рый алгоритм над алфавитом ; если применимо к слову ( — слова в Л, а символ играет роль запятой), то считаются посылками, а — заключением нек-рого применения этого В. п. Частным случаем таких В. п. являются нуль-посылочные В. п. (или аксиом схемы). В любом исчислении, содержащем лишь правила описанного типа, множество выводимых слов перечислимо. Обычно для В. п. выполнено и более жесткое требование: можно алгоритмически распознать, выводимо ли из за одно применение правила. С. Ю. Маслов.