Тема 6. Теория доказательств в исчислении предикатов
Изучив материалы темы, Вы сможете:
- указать отличия между теорией доказательств в исчислении высказываний и теорией доказательств в исчислении предикатов;
- сформулировать теорию дедукции для исчисления предикатов;
- сформулировать правило подстановки в исчислении предикатов;
- дать определение вывода и доказательства в исчислении предикатов.
Теория доказательств в исчислении предикатов имеет много общего с теорией доказательств в исчислении высказываний, однако есть некоторые существенные отличия, которые позволяют разделять эти теории.
Исчисление предикатов имеет свои особенности. В отличие от исчисления высказываний в алфавите исчисления предикатов содержатся предикатные буквы, предметные или индивидные переменные, квантор всеобщности и существования (подробнее см. тему 9).
Эти особенности сказываются на определении формулы в исчислении предикатов и формулировке правил вывода (см. тему 9 и тему 10).
Для предикатной формулы имеют значение свободные и связанные вхождения переменных. Данные вхождения определяются правилом подстановки. Определение свободных и связанных вхождений переменных дано в теме 9. Правило подстановки в исчислении предикатов формулируется по отношению ко всем видам переменных, фигурирующих в формулах.
Подстановкой в формулу А переменной у вместо хназывается замещение в А всех свободных вхождений х вхождениями у. Результат подстановки в формулу А обозначается посредством 
. Подстановка в у вместо х называется корректной, если ни одно введённое данной подстановкой вхождение у, не оказывается связанным в .
В правильных рассуждениях некорректная подстановка недопустима, так как она может привести к ложным утверждениям. Например, мы знаем, что формула 
выражает всегда выполнимое арифметическое условие, то есть условие, которому удовлетворяет любое численное значение переменной. Но некорректная подстановка y вместо x в данную формулу даёт высказывание 
, выражающее ложное суждение.
Теорема дедукции для исчисления предикатов отличается от теоремы дедукции для исчисления высказываний ограничением, которое состоит в том, что во вспомогательном выводе свободные переменные (определение свободных переменных см. в теме 9) должны оставаться фиксированными для подлежащих устранению исходных формул.
Теорема дедукции для исчисления предикатов. Если Г, А├ В,причем все свободные переменные остаются фиксированными для последней исходной формулы А, тоГ ├ (A→B).
Выводом в исчислении предикатов называется непустая конечная последовательность формул 
,…, 
, удовлетворяющая следующим условиям:
1) каждая 
есть либо посылка, либо получена из предыдущих формул по одному из правил вывода;
2) если в выводе применялись правила введения импликации или правила введения отрицания, то все формулы, начиная с последней посылки и вплоть до результата применения данного правила, исключаются из дальнейших шагов построения вывода;
3) ни одна индивидная переменная в выводе не ограничивается абсолютно более одного раза (см. ограничения на применение правила «введение всеобщности» и «удаление существования»);
4) ни одна переменная не ограничивает в выводе сама себя (см. ограничения на применение правила «введение всеобщности» и «удаление существования»).
Доказательство в исчислении предикатов есть вывод из пустого множества неисключённых посылок.
Завершённым выводом в исчислении предикатов называется вывод, в котором никакая переменная, абсолютно ограничивавшаяся в выводе, не встречается свободно ни в неисключённых посылках, ни в заключении.
Завершённое доказательство в исчислении предикатов есть завершённый вывод из пустого множества неисключённых посылок.
Примеры доказательства в исчислении предикатов приведены в 10.
Контрольные вопросы:
1. Сформулируйте теорему дедукции для исчисления предикатов.
2. Как определяется вывод в исчислении предикатов?
3. Сформулируйте правило подстановки в исчислении предикатов?
4. В чём состоит отличие между доказательством в исчислении высказываний и доказательством в исчислении предикатов?
5. Какие особенности определяют различие между исчислением высказываний и исчислением предикатов?