Вывод логический (Кузнецов, 2007)
ВЫВОД ЛОГИЧЕСКИЙ - осуществляемая в рамках логических исчислений в соответствии с точными формальными правилами процедура знаковых преобразований, целью которой является обоснование правомерности, логической корректности перехода от некоторого множества формул к некоторой формуле.
Вывод логический представляет собой формальный аналог рассуждения в естественном языке.
Существование В.л. формулы А из множества формул G означает наличие между ними отношения выводимости (из G выводима А). Если исчисление строится с целью формализации логической теории, сформулированной в семантических терминах, то понятие В.л. стремятся задать таким образом, чтобы отношение выводимости являлось адекватным синтаксическим дубликатом отношения логического следования (из G логически следует А), т.е. воспроизводило формы логически правильных умозаключений.
В исчислениях различных типов определение В.л. имеет свои особенности. Так, в аксиоматических исчислениях под В.л. формулы А из множества формул G обычно понимают непустую конечную последовательность формул, завершающуюся формулой А, такую, что каждый член этой последовательности есть либо аксиома, либо элемент G, либо формула, полученная из предыдущих по одному из постулируемых в исчислении правил вывода. Причем если какое-нибудь из правил вывода не воспроизводит отношение логического следования, на его применение накладываются специальные ограничения. Специфика натуральных исчислений состоит в отсутствии аксиом и разрешении использовать при построении В.л. дополнительные допущения. В этом случае в определение В.л. обычно включают описание процедур устранения введенных допущений. В секвенциальных исчислениях обоснованию подвергаются не отдельные формулы, а секвенции — аналоги метаутверждений о выводимости. В.л. здесь представляет собой множество секвенций, упорядоченных в виде дерева согласно особым правилам.
Понятие В.л. и отношение выводимости тесно связаны с другими фундаментальными понятиями символической логики — понятиями доказательства и теоремы. Доказательство обычно определяют как В.л. формулы из пустого множества посылок, а теорему исчисления — как формулу, выводимую из пустого множества формул.
Словарь философских терминов. Научная редакция профессора В.Г. Кузнецова. М., ИНФРА-М, 2007, с. 96-97.