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

— рассуждение, в ходе которого из к.-л. исходных суждений — посылок — с помощью логических правил получают заключение — новое суждение. Напр., из суждений «Все люди смертны» и «Кай — человек» мы можем вывести с помощью правил простого категорического силлогизма новое суждение: «Кай смертен».

В символической логике вывод определяется более строго — как последовательность высказываний или формул, состоящая из аксиом, посылок и ранее доказанных формул (теорем). Последняя формула данной последовательности, выведенная как непосредственное следствие предшествующих формул по одному из правил вывода, принятых в рассматриваемой аксиоматической теории, представляет собой выводимую формулу. Поскольку каждая формальная система имеет свои собственные аксиомы и правила вывода, постольку во всякой системе понятие вывода носит специфический характер.

В качестве примера приведем определение понятия вывода для следующей формальной системы. Алфавит системы включает в себя бесконечный набор символов:

р, q, r, s,...; p ₁ q ₁, r ₁, s ₁,...; p ₂ q ₂, r ₂, s ₂,..., которые называются пропозициональными переменными. К ним добавляются следующие четыре символа:

(,), ->, ~

левая и правая скобки, знак импликации и знак отрицания. Правила построения формул:

1) всякая пропозициональная переменная есть формула;

2) если А и В суть формулы, то (А—> В) есть формула;

3) если A есть формула, то ~ A есть формула.

В качестве аксиом можно принять следующие три формулы: а) s - > (p - > s);

б) (s - > (p - > q))- > ((s - > p)- > (s - > q));

в) (~ p - > ~ q)- > (q - > p).

В качестве правил вывода принимаются следующие два правила:

1) Правило подстановки: если формула А получается из формулы А путем замены некоторой переменной повсюду, где она встречается в Л, на некоторую формулу С, то из A следует А'.

2) Правило отделения: из формул вида (А - > В) и A следует формула В.

Теперь можно определить понятие вывода. Последовательность формул A ₁,..., А _т называется выводом формулы A из посылок Г₁ ..., Г _т, если каждая формула этой последовательности есть либо одна из аксиом системы, либо одна из посылок Г₁,..., Г _т, либо получена из каких-то предыдущих формул последовательности по одному из правил вывода данной системы, а формула А есть последняя формула данной последовательности.

Формулу A, для которой существует вывод из посылок Г₁,..., Г _т называют выводимой из Г₁,..., Г _т. Утверждение о выводимости формулы A из посылок Г₁,..., Г _т записывается так: Г₁,..., Г _т |- A и читается: «Формула A выводима из посылок Г₁,..., Г _т». Безотносительно к специфике формальной системы отношению логической выводимости (|-) присущи следующие свойства:

1) Г |- Е,.если Е входит в список посылок Г.

2) Если Г |- Е, то Г, ∆ |- Е для любого перечня формул Д.

3) Если Г |- Е, то ∆ |- Е, когда ∆ получено из Г путем перестановки формул Г или опускания таких формул, которые тождественны остающимся формулам.

4) Если Г |- Е, то ∆ |- Е, когда ∆ получено из Г за счет опускания любых формул Г, которые доказуемы или выводимы из остающихся формул Г.