Исчисления предикатов ИП (ИПС).

Определим исчисление предикатов гильбертовского типа ИП. Это исчисление является расширением исчисления высказываний ИВ.

В алфавит ИВ добавим строчные латинские буквы для обозначения предметных переменных и символы кванторов " и $. Язык исчисления составляют формулы, определяемые также, как в алгебре предикатов.

Аксиоматика исчисления дополняется двумя схемами аксиом:

11.

12. ,

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

К правилу заключения ИВ добавляются два правила, связанные с кванторами. Пусть и – формулы, которые содержат и не содержат свободные вхождения переменной x соответственно.

2. Правило обобщения (введения ")

.

3. Правило введения $

.

Правила естественного вывода дополняются 4-мя правилами. Пусть

14. Правило введения квантора ".

Если T |- U(x), то T |- "xU(x).

15. Правило удаления квантора ".

Если T |- "xU(x), то T |- U(y).

16. Правило введения квантора $.

Если T |- U(y), то T |- $xU(x).

17. Правило удаления квантора $.

Если T, U(x) |- V, то T, $xU(x) |- V.

Рассмотрим пример вывода в ИП.

Доказать, что в ИП |-

1. |-
2. |-	15 (1)
3. |-	14 (2)

Исчисление предикатов генценовского типа ИПС строится расширением исчисления ИП.