Доказательство эквивалентности выводимости и логической истинности менее прямое, чем для семантических таблиц. Мы не будем стараться строить вывод всякой истинной формулы, а опровергающую модель для невыводимой формулы построим столь неэффективно, что воспользоваться данной теоретической конструкцией для практических целей практически невозможно. Это связано с “асимметричностью” естественного вывода: онхорошкаксредстводоказательства, но то, что вывод не удалось завершить, не всегда дает информацию для опровержения.

Утверждение о полноте состоит из двух частей. Нужно доказать корректность, т. е. утверждение о том, что каждая теорема является семантическим следствием теории, и собственно полноту, о том, что каждое семантическое следствие может быть выведено. Первая часть доказывается достаточно тривиальной индукцией, но с достаточно нетривиальной формулировкой инварианта индукции и входящих в него понятий.

Теорема 11.1. (Теорема корректности) Если A выводима в Th, то Aявляется семантическим следствием Th.Доказательство. Сформулируемвспомогательноепонятие незаконченного вывода. Незаконченный вывод — граф, удовлетворяющий условиям, наложенным на вывод, кроме того, что каждый подвывод должен иметь результат и использоваться в дальнейшем. Естественно, подвыводы, не имеющие результатов, использованы быть не могут. Незаконченный вывод может рассматриваться как промежуточная стадия построения вывода методом “снизу вверх”, от посылок и аксиом к результатам и теореме. Многие преобразования выводов являются общими длязавершенных и незавершенных выводов. В данном доказательстве нампотребуется переименование произвольных переменных. То, что произвольные переменные вложенных подвыводов могут совпадать, гарантирует возможность переносить куски из вывода в вывод без изменений.