27. Исчисление предикатов как формальная система. Связь правил вывода в исчислении предикатов с аксиоматическими основаниями логики предикатов. Прямой и обратный вывод в исчислении предикатов.

Исчисление предикатов – это формальная система, которая включает алфавит, синтаксические правила построения формул в алфавите, аксиомы (общезначимые исходные формулы), правила вывода, позволяющие строить новые формулы.

Правила вывода ├  связаны непосредственно с формулами, а не с таблицами истинности, позволяя на основании истинности одних формул делать заключение об истинности других формул.

Аксиомами исчисления предикатов называются формулы этого языка, имеющие один из следующих видов:

A(BC); (A(BC))((AB)(AC)); A(BA&B); A&BA; A&BB;

(AC)((BC)((AB)C); A(AB); B(AB); (AB)((AB)A); AA;

К этому множеству аксиом добавляются формулы, образованные с использованием кванторов. Если free (x, t, ), то общезначимы формулы:

(x(x)(x/t)); (правило универсального обобщения); x(  (x))  (  x (x));

((x/)x(x)); (правило экзистенциальной конкретизации); x((x)  )(x (x)  ).

Общезначимые эквивалентности:

1. Замена связанной переменной :╞ xB(x)  yB(y);╞ xB(x)  yB(y).

2. Перестановка одноименных кванторов:╞ xy A(x,y)  yx A(x,y); ╞ xyA(x,y) yx A(x,y).

3. Пронесение отрицания через кванторы:╞ xC(x)  x(C(x)); ╞ xC(x)  x(C(x)).

4. Введение отрицания в формулу:╞ xC(x)  (x(C(x)));╞ xC(x)  (x(C(x))).

5. Дистрибутивность квантора общности относительно конъюнкции:

6. ╞ xB(x) & xC(x)  x(B(x)&C(x)),╞ E & xC(x)  x(E&C(x)).

7. Дистрибутивность квантора существования относительно дизъюнкции:

╞ xB(x)  xB(x)  x(B(x)  C(x)),╞ (E  xC(x))  x(E  B(x)).

8. Дистрибутивность квантора существования относительно конъюнкции:

╞ E & xC(x)  x(E & C(x)).

9. Дистрибутивность квантора общности относительно дизъюнкции:

╞ E  xC(x)  x(E  C(x)).

Общезначимые импликации логики предикатов

1. Правило пронесения квантора существования через конъюнкцию:

╞ (х (А(х) & В(х)) хА(х) & хВ(х)).

2. Правило пронесения квантора общности через дизъюнкцию

╞ (хА(х) хВ(х) х(А(х)  В(х))).

3. Смена квантора:╞ (х В(х) х В(х));

4. Перестановка разноименных кванторов: ╞ (ху А(х,у) ух А(х,у)).