ВЫВОД ЛОГИЧЕСКИЙ

ВЫВОД ЛОГИЧЕСКИЙ
    ВЫВОД ЛОГИЧЕСКИЙ — рассуждение, в котором
    осуществляется переход по правилам от высказывания или системы высказываний к высказыванию или системе высказываний. К логическому выводу обычно предъявляются (совместно или по отдельности) следующие требования: 1) правила перехода должны воспроизводить отношение следования логического (ту или иную его разновидность); 2) переходы в логическом выводе должны осуществляться на основе учета только синтаксических характеристик высказываний или систем высказываний.
    В современной логике понятие логического вывода определяется для формальных систем, в которых высказывания представлены формулами. Обычно выделяют три основных типа формальных систем: аксиоматические исчисления, исчисления натурального вывода, исчисления секвенций. Стандартное определение логического вывода (из множества формул Г) для аксиоматического исчисления S таково: логический вывод в S из множества формул Г есть такая последовательность Ai... A, формул языка исчисления S, что для каждой Ai (ISiSn) выполняется, по крайней мере, одно из следующих трех условий: 1) А, есть формула из Г; 2) ?? есть аксиома исчисления S; 3) А, есть формула, получающаяся из предшествующей ей в последовательности Л ?...Лд формулы или из предшествующих ей в этой последовательности формул по одному из правил вывода исчисления S. Если ? есть логический вывод в S из множества формул Г, то формулы из Г называются посылками a, a сам вывод ? называется выводом в S из посылок Г; если при этом А есть последняя формула а, то а называется логическим выводом в S формулы А из посылок Г. Запись “Г •,А* означает, что существует логический вывод в S формулы А из посылок Г. Логический вывод в S из пустого множества формул называется доказательством в S. Запись “ г,-4” означает, что существует доказательство в S формулы А. Формула А называется доказуемой в S, если -А. В качестве примера рассмотрим аксиоматическое исчисление Si со стандартным определением вывода, являющееся вариантом классической логики высказывании. Алфавит этого исчисления содержит только пропозициональные переменные pi, pi, ..., р„ ..., логические связки =>, 1 и круглые скобки. Определение формулы в этом языке обычное. Аксиомы ??—?то формулы следующих шести видов (и только эти формулы): I. (А^>А), II. ((Д55)э((Д=)С)э(^эС))), Ш. ((Л=?/”эО)эГДэ(ЛэС))), IV. ((Лэ(1Д))э(Дэ(1Д))), V. ((1(1Л)эЛ), М. (((А•зВ)=,А)зА).
    Единственное правило исчисления St модус поненс: Л, А^В^В.
    Определение логического вывода для Si является очевидной конкретизацией определения, данного выше. Следующая последовательность формул Ф1 — Ф6 является логическим выводом в Si формулы ((pi^pi)^) из посылок [pt].
    ??. ((??^??)^(??^??)), Ф2. Wpi-spi) э(р1 эра)) =>??? =>((?, э^) з^))), ФЗ. (р1Э((р1=>й)э^)), Ф4.^,, Ф5. ((pi•Dpi)^pi).
    Анализ: Ф1 есть аксиома вида 1, Ф2 есть аксиома вида III, ФЗ получена по правилу модус поненс из Ф1 и Ф2, Ф4 есть посылка, Ф5 получена по правилу модус поненс из Ф4 и ФЗ. Итак, fssilhi ((р^рг)=)рг). Рассмотрев последовательность формул Ф1, Ф2 ФЗ, убеждаемся, что гл(р13р1)зрг)).
    В ряде случаев логический вывод определяется так, что на использование некоторых правил накладываются ограничения. Напр., в аксиоматических исчислениях, являющихся вариантами классической логики предикатов первого порядка и содержащих среди правил вывода только модус поненс и правило обобщения, логический вывод часто определяется так, что на использование правила обобщения накладывается ограничение: любое применение правилам обобщения в ? таково, что переменная, по которой ироввдитея обобюение в этом применении правила обобщения, не входит ни в одну посылку, предшествующую в ? нижней формуле этого применения правила обобщения. Цель этого ограничения обеспечить ряд полезных с точки зрения логики свойств вывода (напр., выполнение для простых форм дедукции теоремы). Существуют определения логического вывода (как для аксиоматических, так и для исчислений других типов), которые (1) задают логический вывод не только из множества посылок, но допускают другие формы организации посылок (напр., списки или последовательности), (2) структурируют вывод не только линейно, но, напр., в форме дерева, (3) имеют явно выраженный индуктивный характер; при этом индуктивное определение вывода может вестись как по одной переменной (напр., по длине вывода), так и по нескольким переменньм (напр., по длине логического вывода и по числу его посылок), (4) содержат формализацию зависимости между формулами в логическом выводе, и многие другие определения логического вывода, обусловленные иными способами формализации и аксиоматизации классических и неклассических систем логики. О некоторых из них см. в ст. Аналитических таблиц метод. Семиотика, Исчисление секвенций.
    В. М. Попов

Новая философская энциклопедия: В 4 тт. М.: Мысль. Под редакцией В. С. Стёпина. 2001.