Логический вывод и логическое следование
Теория. Если между высказываниями установлено отношение логического следования, т. е. А |= В, которое можно проверить с помощью таблиц истинности, то из А выводимо В. Записывается: А |– В. В большинстве исчислений логики высказываний верны следующие положения:
Выводом называется конечная последовательность формул, каждая из которых есть либо посылка, либо аксиома (при наличии аксиом), либо получена из предыдущих формул этой последовательности по одному из правил вывода. Последняя формула вывода не может быть посылкой и называется заключением. При отсутствии посылок вывод становится доказательством, а его последняя формула называется теоремой: |– А.
В соответствии с метатеоремой дедукции (если из А |– B, то |– (А → В и наоборот), любой вывод можно превратить в доказательство, а доказательство — в вывод. Основной и нетривиальной проблемой является поиск доказательства.
