имеют значения «истина», формула
В также имеет значение «истина». Этот метод применим всегда,
но может оказаться слишком трудоемким.
При синтаксическом методе доказательства сначала
записывают посылки и, применяя к ним правила вывода,
стараются получить из них другие истинные формулы. Из этих
формул и исходных посылок выводят последующие формулы, и
этот процесс продолжают до тех пор, пока не будет получено
требуемое заключение (заметим, что это не всегда возможно).
Этот процесс, по сути дела, и является логическим выводом.
Исчисление предикатов (ИП) обеспечивает основу для
формализации теории логического вывода. Возможность
логически выводить новые правильные выражения из набора
истинных утверждений – это важное свойство ИП.
Говорят, что интерпретация, которая делает предложение
истинным, удовлетворяет этому предложению. Если
интерпретация удовлетворяет каждому элементу набора
выражений, то говорят, что она удовлетворяет набору.
Выражение Х логически следует из набора выражений S ИП,
если каждая интерпретация, удовлетворяющая S, удовлетворяет
и Х. Это утверждение делает основание для проверки
правильности правил вывода: функция логического вывода
должна производить новые предложения, которые логически
следуют из данного набора предложений ИП.
Важно верно понимать значения слов «логически
следует»: логическое следование выражения Х из S означает,
что оно должно быть истинным для каждой интерпретации,
которая удовлетворяет первоначальному набору выражений S.
Это означает, например, что любое новое выражение ИП,
добавленное к «миру блоков» должно быть истинным в этом
мире. Оно должно быть истинным и при любой другой
интерпретации, которую мог бы иметь этот набор выражений.
Термин «логически следует» вовсе не означает, что Х
выведено из S, или что его можно вывести из S. Это просто