Вывод заключения из множества посылок записывается так же, как в исчислении высказываний

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

Для любой F(x) формула

Например,

Это отношение может быть истинным для одних значений из области интепретации и ложным для других.

При такой интерпретации выделяют три класса формул, тождест­венно истинные, тождественно ложные и выполнимые.

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

для предиката P²(x, y):=”число x меньше числа y” формула "_x$_y(P²(x, y)):=”для любого целого числа x найдется число y, большее числа x” является тождественно истинной;

для любой F(x) формула $_x(F(x))«ù"_x(ùF(x)):=“формула ”существуют x, для которых F(x)=и”, эквивалентна формуле “не для всех x F(x)=л”” является тождественно истинной.

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

Например, для предиката P²(x, y):=”число x меньше числа y” формула $_x"_y(P²(x, y)):=”существует целое число x, которое меньше любого целого числа y” является тождественно ложной;

$_x(F(x))&"_x(ùF(x)):=”“существует x, для которой F(x)=и”, и “для всех x F(x)=л ”” является тождественно ложной.

Выполнимые формулы - это особый класс формул исчисления преди­катов, которые принимают значение “истина”в некоторой области, т.е. не для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула $_x(F(x))®ù"_x(F(x)) является истинной для одного элемента множества V и ложной для всех элементов этого множества, т.к.

$_x(F(x))®ù"_x(F(x)):=” если существует x, для которого F(x)=и, то не для всех х универсума F(x)=и” .

F₁;F₂;¼F_n|¾ B, где слева от знака “|¾” записывают множество формул посылок и необходимые аксиомы F₁;F₂;¼F_n, а справа – формулу заключения B. Тогда знак “|¾” означает “верно, что B выводима из F₁;F₂;¼F_n.