секвенциальное исчисление предикатов

1. Поиск контрпримера для формулы с кванторами………………………..3
2. Формулировка исчисления………………………………………………...8
3. Корректность и полнота исчисления……………………………………...9
4. Соотношение с исчислениес предикатов гильбертовского типа………10
5. О поиске вивода в секвенциальном исчислении предикатов………….11
6. Список использованной литературы…………………………………….

1. Поиск контрпримера для формулы с кванторами………………………..3
2. Формулировка исчисления………………………………………………...8
3. Корректность и полнота исчисления……………………………………...9
4. Соотношение с исчислениес предикатов гильбертовского типа………10
5. О поиске вивода в секвенциальном исчислении предикатов………….11
6. Список использованной литературы…………………………………….

2. Формулировка исчисления.
Зафиксируем произвольный язык первого порядка . Сформулируем исчисление , называемое секвенциальным исчислением предикатов генценовского типа для языка .
Секвенцией называется слово вида
,
где– формулы, . Представлением секвенции S в виде формулы (или формульным образцом секвенции S) назовем формулу
.
Назовем секвенцию общезначимой, если формула общезначима. Очевидно, секвенция общезначима тогда и только тогда, когда не существует контрпримера для этой секвенции. Контрпримером для секвенции S называется упорядоченная пара, состоящая из интепретации языка и оценки, в которых истинны все члены антецедента S и ложны все члены сукцедента S.
Будем говорить, что предметная переменная входит в секвенцию свободно (соответствено, связанно), если эта переменная входит свободно (связанно) хотя бы в один член данной секвенции.
Правила вывода исчисления подразделяются на пропозициональные и кванторные.
...

3. Корректность и полнота исчисления.

Лемма 1. В исчислении каждая аксиома общезначима; для каждого правила вывода заключение этот правила общезначимо, если и только если все посылки этого правила общезначимы.
Теорема 1 (корректность исчисления ). Любая выводимая в исчислении .
Следствие 1. Исчисление непротиворечиво, то есть не существует формулы А такой, что А выводима и выводима.
Формулу (секвенцию) назовем чистой, если никакая предметная переменная не входит в нее одновременно свободно и связанно.
Теорема 2 (полнота исчисления ). Пусть – произвольная чистая секвенция, все члены которой являются формула языка . Тогда если общезначима, то выводима в исчислении .
Замечание 2.1. Чистота формулы слабее обладания свойством чистоты переменных.
Замечание 2.2.
...