ВЫВОДА ПРАВИЛО

ВЫВОДА ПРАВИЛО - способ порождения объектов, называемых заключением В. п., по множеству объектов, называемых посылками правила; формулирование В. п. играет решающую роль при описании исчислений (часто данное В. п. имеет смысл лишь в контексте данного исчисления). Для исчислений, снабженных семантикой (в частности, большинства логико-математических исчислений), В. п. сохраняет истинность, т. е. по истинным посылкам позволяет породить лишь истинное заключение; наиболее знаменитый пример такого В. п.- правило модус поненс. В большинстве изучавшихся исчислений всякое применение В. п. имеет лишь конечное число посылок (важнейшее исключение - Карнапа правило), обычно число посылок данного В. п. остается неизменным для всех его применении. Количество возможных применений данного В. п. бывает, как правило, неограниченным.

Способы формулирования В. п. весьма разнообразны, они зависят от языка исчисления и включают переменные различных типов. Подавляющее большинство используемых В. п. может быть порождено по следующей общей схеме: выбирая алфавит A, не содержащий буквы □, и натуральное число l, называют l-посылочным В. п. нек-рый алгоритм над алфавитом A ∪ {□} если применимо к слову P₀ □ P₁ □ ... □ P_l (Р₀, Р₁, ..., P_l - слова в A, а символ □ играет роль запятой), то Р₁, ..., Р_l считаются посылками, а Р₀ -заключением нек-рого применения этого В. п. Частным случаем таких В. п. являются нуль-посылочные В. п. (или аксиом схемы). В любом нечислении, содержащем лишь правила описанного типа, множество выводимых слов перечислимо. Обычно для В. п. выполнено и более жесткое требование: можно алгоритмически распознать, выводимо ли Р₀ из Р₁, ..., P_l за одно применение правила.

С. Ю. Маслов.

Источники:

1. Математическая Энциклопедия. Т. 1 (А - Г). Ред. коллегия: И. М. Виноградов (глав ред) [и др.] - М., «Советская Энциклопедия», 1977, 1152 стб. с илл.