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

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

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

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

11.

12. ,

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

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

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

.

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

.

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

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

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

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

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

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

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

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

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

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

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

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

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