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

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

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

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

11)

12) ,

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

Например, F(x) не может быть формулой вида G (x) Ú $ y H (x, y).

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

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

.

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

.

Правила вывода дополняются 4-мя правилами. Пусть Т – последовательность формул, не содержащих свободных вхождений переменной х.

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

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

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

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

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

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

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

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

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

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

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

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

Отношение эквивалентности в ИП и ИПС определяется также, как и в ИВ.

Дата добавления: 2014-01-11