Исчисление предикатов.

Определение. Предикатом P(x1, x2, …, xn) называется функция, переменные которой принимают значения из некоторого множества М, а сама функция принимает два значения: И (истина) и Л (ложь), т.е.

Предикат от п аргументов называется п – местным предикатом. Высказывания считаются нуль – местными предикатами.

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

Кроме обычных логических операций к предикатам применяются также специальные операции, называемые кванторами.

Кванторы бывают двух видов:

1) Квантор общности. Обозначается ("х)Р(х). Квантором общности называется высказывание истинное, когда Р(х) истинно для каждого элемента х из множества М, и ложное – в противном случае.

2) Квантор существования. Обозначается ($х)Р(х). Квантором существования называется высказывание, истинное, когда существует элемент из множества М, для которого Р(х) истинно, и ложное в противном случае.

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

Для формул логики предикатов сохраняется справедливость всех правил равносильных преобразований логики высказываний. Кроме того, справедливы следующие свойства:

1) Перенос квантора через отрицание.

O("x)A(x) º ($x)OA(x); O($x)A(x) º ("x)OA(x);

2) Вынесение квантора за скобки.

($х)(А(х) & B) º ($x)A(x) & B; ("x)(A(x) & B) º ("x)A(x) & B;

($х)(А(х) U B) º ($x)A(x) U B; ("x)(A(x) U B) º ("x)A(x) U B;

3) Перестановка одноименных кванторов.

("y)("x)A(x,y) º ("x)("y)A(x,y); ($y)($x)A(x,y) º ($x)($y)A(x,y);

4) Переименование связанных переменных. Если заменить связанную переменную формулы А другой переменной, не входящей в эту формулу, в кванторе и всюду в области действия квантора получаем формулу, равносильную А.

Исчисление предикатов базируется на приведенных выше свойствах и правилах, называемых аксиомами.

Какими бы ни были формулы А и В для них справедливы следующие аксиомы:

1) A ? (B ? A);

2) (A ? (B ? C)) ? ((A ? B) ? (A ? C));

3) (OB ? OA) ? ((OB ? A) ? B);

4) ("xi)A(xi) ? A(xj), где формула А(хi) не содержит переменной xi.

5) A(xi) ? ($xj)A(xj), где формула А(хi) не содержит переменной xi.