ВЫВОД ЛОГИЧЕСКИЙ
– рассуждение, в ходе которого из к.-л. исходных суждений – посылок – с помощью логических правил получают заключение – новое суждение. Напр., из суждений «Все люди смертны» и «Кай – человек» мы можем вывести с помощью правил простого категорического силлогизма новое суждение: «Кай смертен».
В символической логике вывод определяется более строго – как последовательность высказываний или формул, состоящая из аксиом, посылок и ранее доказанных формул (теорем). Последняя формула данной последовательности, выведенная как непосредственное следствие предшествующих формул по одному из правил вывода, принятых в рассматриваемой аксиоматической теории, представляет собой выводимую формулу. Поскольку каждая формальная система имеет свои собственные аксиомы и правила вывода, постольку во всякой системе понятие вывода носит специфический характер.
В качестве примера приведем определение понятия вывода для следующей формальной системы. Алфавит системы включает в себя бесконечный набор символов:
р, q, r, s, ...; p1 q1, r1, s1, ...; p2q2, r2, s2, ... ,
которые называются пропозициональными переменными. К ним добавляются следующие четыре символа:
(,),->,
левая и правая скобки, знак импликации и знак отрицания. Правила построения формул:
1) всякая пропозициональная переменная есть формула;
2) если А и В суть формулы, то (А–>В) есть формула; 3) если A есть формула, то A есть формула.
В качестве аксиом можно принять следующие три формулы:
а) s-> (p->s);
б) (s->(p->q))->((s->p)->(s->q));
в) ( p-> q)->(q->p).
В качестве правил вывода принимаются следующие два
правила:
1) Правило подстановки: если формула А получается из формулы А путем замены некоторой переменной повсюду, где она встречается в Л, на некоторую формулу С, то из A следует А́.
2) Правило отделения: из формул вида (А->В) и A следует формула В.
Теперь можно определить понятие вывода. Последовательность формул A1, ..., Ат называется выводом формулы A из посылок Г1 ..., Гт, если каждая формула этой последовательности есть либо одна из аксиом системы, либо одна из посылок Г1, ..., Гт, либо получена из каких-то предыдущих формул последовательности по одному из правил вывода данной системы, а формула А есть последняя формула данной последовательности.
Формулу A, для которой существует вывод из посылок Г1, ..., Гт называют выводимой из Г1, ..., Гт. Утверждение о выводимости формулы A из посылок Г1, ..., Гт записывается так: Г1, ..., Гт -A и читается: «Формула A выводима из посылок Г1, ..., Гт». Безотносительно к специфике формальной системы отношению логической выводимости ( -) присущи следующие свойства:
1) Г – Е,.если Е входит в список посылок Г.
2) Если Г – Е, то Г, ? – Е для любого перечня формул Д.
3) Если Г – Е, то ? – Е, когда ? получено из Г путем перестановки формул Г или опускания таких формул, которые тождественны остающимся формулам.
4) Если Г – Е, то ? – Е, когда ? получено из Г за счет опускания любых формул Г, которые доказуемы или выводимы из остающихся формул Г.