Исчисления предикатов ИП (ИПС).
Определим исчисление предикатов гильбертовского типа ИП. Это исчисление является расширением исчисления высказываний ИВ.
В алфавит ИВ добавим строчные латинские буквы для обозначения предметных переменных и символы кванторов " и $. Язык исчисления составляют формулы, определяемые также, как в алгебре предикатов.
Аксиоматика исчисления дополняется двумя схемами аксиом:
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) |
Исчисление предикатов генценовского типа ИПС строится расширением исчисления ИП.
Дата добавления: 2016-02-09; просмотров: 736;