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

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

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

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

Ни одна предметная переменная в выводе не ограничивается абсолютно дважды;

Ни одна переменная в выводе не ограничивает сама себя.

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

Однако не любой вывод и не любое доказательство в исчислении предикатов являются завершенными. Дополнительно надо ввести еще одно требование:

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

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

Для примера рассмотрим следующее умозаключение:

Дата добавления: 2015-06-30; просмотров: 180; Нарушение авторских прав

Мы поможем в написании ваших работ!