Следствия теорем 10pd и llpd сводят понятие выводимости А1, …, Аm |- В к понятию доказуемости «|- Е» точно так же, как следование А1, …, Аm |=В сводилось к общезначимости «|=Е». Точно так же, используя » ‘, получаем редукциИ для А1, …, Аm |- x1…xq В и A1, …, Аm |=х1…xq В. Для доказательства того, что теория моделей и теория доказательств для исчисления предикатов равносильны, осталось
показать, что |=Е тогда и только тогда, когда |-Е.
Достаточность (если |- Е, то |=Е) получается легко. Ведь теорема 12 и ее следствие сохраняют силу. Использование теоремы, где утверждается общезначимость для новой редакции нет необходимости в полном исползовании теоремы. Следствие можно получить при «1- |=» вместо «|=», т. е. при D = {1}. Именно таким путем Гильберт и Аккерман в |первые доказали простую непротиворечивость исчисления преакатов.
Необходимость же (|=Е, только если |-Е), т.е. перенесение исчисление на исчисление предикатов теоремы 14, не столь элементарна, как теоремы, данные до сих пор. Она содержится в теореме Гёделя о полноте.
В классической логике (которая Интересует нас в первую очередь) мы заинтересованы в общезначимых формулах, ибо они выражают всеобщие логические законы, и в доказуемых формулах, ибо они общезначимы.
В (классическом) исчислении высказываний построение истинностных таблиц (т. е. анализ по истинности) давало безотказный метод доказательства общезначимости, исходя непосредственно из определения в теории моделей. Однако практически этот метод всегда удобен и обычно не походит на наши действительные мыслительные процессы, которые на деле гораздо более экономны. Отчасти именно, поэтому мы ввели теорию доказательств. Конечно, мы не,ограничились определениями, а перешли от них к производным правилам . Первоначальные определения теории доказательств можно рассматривать как удобную пересадочную станцию на пути от теории моделей (общезначимость и т. п.) к производным правилам вывода теории доказательств.
В (классическом) исчислении предикатов непосредственное применение определения общезначимости уже не является простым делом. Доказательства общезначимости с Помощью истинностных таблиц перестают быть механической процедурой; они нуждаются в общих рассуждениях относительно таблиц истинности для произвольных (непустых) областей D, а для бесконечной области D
таблица истинности становится бесконечным объектом.
Теорема 21.
Пусть х-произвольная переменная, А(х)-произвольная формула, r — произвольная переменная, не обязательно отличная от х, и А ( r )-результат подстановки r вместо свободных вхождений х в А(х). Пусть Г- некоторый список формул (может быть, пустой), а С — произвольная формула. Тогда, при условии что
(A) В » — удалении и $ — введении r свободно для х в A(x)
(B) В » — введении и $ — удалении х не входит свободно в Г
(C) В $ — удалении х не входит свободно в С