Тема 6. Теория доказательств в исчислении предикатов

Изучив материалы темы, Вы сможете:

- указать отличия между теорией доказательств в исчислении высказываний и теорией доказательств в исчислении предикатов;

- сформулировать теорию дедукции для исчисления предикатов;

- сформулировать правило подстановки в исчислении предикатов;

- дать определение вывода и доказательства в исчислении предикатов.

Теория доказательств в исчислении предикатов имеет много общего с теорией доказательств в исчислении высказываний, однако есть некоторые существенные отличия, которые позволяют разделять эти теории.

Исчисление предикатов имеет свои особенности. В отличие от исчисления высказываний в алфавите исчисления предикатов содержатся предикатные буквы, предметные или индивидные переменные, квантор всеобщности и существования (подробнее см. тему 9).

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

Для предикатной формулы имеют значение свободные и связанные вхождения переменных. Данные вхождения определяются правилом подстановки. Определение свободных и связанных вхождений переменных дано в теме 9. Правило подстановки в исчислении предикатов формулируется по отношению ко всем видам переменных, фигурирующих в формулах.

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

В правильных рассуждениях некорректная подстановка недопустима, так как она может привести к ложным утверждениям. Например, мы знаем, что формула выражает всегда выполнимое арифметическое условие, то есть условие, которому удовлетворяет любое численное значение переменной. Но некорректная подстановка y вместо x в данную формулу даёт высказывание , выражающее ложное суждение.

Теорема дедукции для исчисления предикатов отличается от теоремы дедукции для исчисления высказываний ограничением, которое состоит в том, что во вспомогательном выводе свободные переменные (определение свободных переменных см. в теме 9) должны оставаться фиксированными для подлежащих устранению исходных формул.

Теорема дедукции для исчисления предикатов. Если Г, А├ В,причем все свободные переменные остаются фиксированными для последней исходной формулы А, тоГ ├ (A→B).

Выводом в исчислении предикатов называется непустая конечная последовательность формул ,…, , удовлетворяющая следующим условиям:

1) каждая есть либо посылка, либо получена из предыдущих формул по одному из правил вывода;

2) если в выводе применялись правила введения импликации или правила введения отрицания, то все формулы, начиная с последней посылки и вплоть до результата применения данного правила, исключаются из дальнейших шагов построения вывода;

3) ни одна индивидная переменная в выводе не ограничивается абсолютно более одного раза (см. ограничения на применение правила «введение всеобщности» и «удаление существования»);

4) ни одна переменная не ограничивает в выводе сама себя (см. ограничения на применение правила «введение всеобщности» и «удаление существования»).

Доказательство в исчислении предикатов есть вывод из пустого множества неисключённых посылок.

Завершённым выводом в исчислении предикатов называется вывод, в котором никакая переменная, абсолютно ограничивавшаяся в выводе, не встречается свободно ни в неисключённых посылках, ни в заключении.

Завершённое доказательство в исчислении предикатов есть завершённый вывод из пустого множества неисключённых посылок.

Примеры доказательства в исчислении предикатов приведены в 10.

Контрольные вопросы:

1. Сформулируйте теорему дедукции для исчисления предикатов.

2. Как определяется вывод в исчислении предикатов?

3. Сформулируйте правило подстановки в исчислении предикатов?

4. В чём состоит отличие между доказательством в исчислении высказываний и доказательством в исчислении предикатов?

5. Какие особенности определяют различие между исчислением высказываний и исчислением предикатов?