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