Т. А. Сливина математическая логика и теория алгоритмов

Определение 1 (доказательства). Доказательством называют конечную последовательность s₁, s₂, ..., s_k высказываний рассматриваемой теории, каждое из которых либо является аксиомой, либо выводится из одного или более предыдущих высказываний этой последовательности по логическим правилам вывода.
Определение 2 (теоремы). Теоремой или доказуемым высказыванием называется высказывание, являющееся последним высказыванием некоторого доказательства.
Ясно, что любая аксиома является теоремой, причем ее доказательство состоит из одного шага.
Вывод высказывания С из пустого множества посылок есть, очевидно, доказательство высказывания С.
Теорема. Если формула А теории первого порядка Т есть частный случай тавтологии, то А есть теорема в Т и может быть выведена с употреблением схем логических аксиом (1), (2) и (3) и правила заключения.
Доказательство. Пусть формула А получена из некоторой тавтологии В с помощью подстановок, и x₁, x₂, ..., х_n – набор переменных, входящих в В. Как известно, в этом случае существует вывод В из совокупности . Сделаем в этом выводе всюду подстановки по следующим правилам:

1. 
   если какая-нибудь переменная x_i входит в В, то на места всех ее вхождений в каждую формулу вывода подставляем ту формулу теории Т, которая подставлялась в В на места вхождения той же буквы при построении А.
   
2. 
   если некоторая переменная x_k не входит в В, то на места всех ее вхождений в формулы вывода подставляет произвольную (одну и ту же для данной буквы) формулу теории Т.
   

Полученная таким образом последовательность формул и будет выводом формулы А в теории Т. При этих рассуждениях использовались только аксиомы (1), (2), (3) и правило заключения.
Как известно, в исчислении высказываний справедлива Теорема дедукции:
Если Н, С ├ А, то Н ├ СА.
Эта теорема без соответствующих изменений не справедлива для произвольных теорий первого порядка Т. Например, в любой теории первого порядка всегда
А ├ , но не всегда доказуема формула А . Действительно, рассмотрим область, содержащую по крайней мере два элемента М = а, в, ...}.
Пусть Т – исчисление предикатов, и пусть формула А есть . Проинтерпретируем каким-нибудь свойством, которым обладает только элемент а. Тогда выполнима на множестве, которое содержит а, при этом формула не выполнима на множестве М.