Правила вывода

правило заключения (ПЗ). Здесь А и В - произвольные формулы УИП.

правило навешивания квантора общности ("-правило, или "-ПР). Здесь А и В(х) - произвольные формулы УИП, причем формула А не содержит переменной х свободно.

правило навешивания квантора существования ($-правило, или $-ПР). Здесь А(х) и В - произвольные формулы УИП, причем формула В не содержит переменной х свободно.

В случае применения "- или $-правила говорят, что переменная хв формулах А ® В(х) или А(х) ® В затрагивается (используется, ва­рьируется).

Формальные символы, формулы, система аксиом и правила вывода составляют узкое исчисление предикатов.

Определение. Доказательство в УИП есть конечная последователь­ность формул, каждая из которых есть либо аксиома, либо получена из предыдущих членов последовательности по одному из правил вывода.

Определение. Формула А доказуема в УИП, если в нем существует доказательство, последней формулой которого является А.

Всякая аксиома есть доказуемая в УИП формула, длина доказате­льства которой равна 1.

Пусть Г и D - произвольные конечные совокупности формул УИП (возможно пустые) и А,В,С - произвольные формулы в ИВ.

Определение. Конечная последовательность формул УИП есть вывод из совокупности формул Г, если всякая формула последовательности либо принадлежит Г, либо доказуема, либо получена из предыдущих формул последовательности по одному из правил вывода.

Определение. Формула А выводима в УИП из совокупности формул Г, если в УИП существует вывод из совокупности Г, последней формулой которого является А.

Заметим, что доказуемая формула выводима из любой (в том числе из пустой) совокупности формул.

Теорема. Если формула А получена подстановкой некоторых формул УИП в доказуемую формулу исчисления высказываний, то формула А доказуема в УИП лишь с помощью правила заключения.

Доказательство. Пусть формула из УИП

где В₁,В₂,....,В_n - формулы из УИП; C(p₁,p₂,...,р_n) - доказуемая в ИВ формула и p₁,р₂,...,р_n - полный список (пропозициональных) переменных формулы С. Согласно второй формулировке ИВ формула С доказуема в ИВ лишь с помощью правила заключения.

Пусть D₁,D₂,...,D_r (=C) есть доказательство формулы С в ИВ (с помощью только правила заключения); q₁,q₂,…,q_m - полный список переменных во всех формулах D_i (i = 1,2,...,r); Е₁, Е₂,...,Е_m - произвольные попарно различные формулы УИП, отличные от всех ранее упомянутых в теореме формул. Сопоставим каждому q_i формулу F_i согласно следующему равенству:

i = 1,2,...,m; j = 1,2,...,n.

В доказательстве D₁,D₂,...,D_r в ИВ заменим каждое q_i в формулах D₁,D₂,...,D_r на F_i. Полученная последовательность формул УИП будет доказательством в УИП формулы А лишь с помощью правила заключения.

Следствие. В УИП справедливы все вспомогательные правила выво­да, доказуемые в ИВ.