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

§6. Исчисления предикатов.

Рассмотрим алфавит V = V 1È V 2 È V 3 È V 4 È V 5 È V 6, где V 1 -- V 6 взяты из §4. Понятия и обозначения сигнатуры, терма, формулы, подформулы, свободной и связанной переменной, предложения определяются, как в §4.

В этом параграфе предполагается, что сигнатура s конечна или счетна.

Определим исчисление ИПС. Алфавит исчисления ИПС есть V È á ├ ñ . Понятия секвенции, правила вывода и т.п. определяются аналогично соответствующим понятиям для ИС (см. §3).

Исчисление ИПС определяется следующими схемой аксиом и правилами вывода ( Á , B , Ã -- произвольные формулы, Г, Г1, Г2 , Г3 – конечные последовательности формул, возможно пустые, t – терм, свободный для х в Á (х); Á (t) получается из Á (х) заменой всех свободных вхождений x на t; Г4 – конечная последовательность формул, не содержащих х свободно; D – формула, не содержащая х свободно).

Схема аксиом Á + Á .

Правила вывода:

1. Г
1+ Á ; Г1+ BÞГ1, Г2 + (Á & B) (введение &)

2. Г├ ( Á & B) Þ Г├ Á (удаление &)

3. Г├ ( Á & B) Þ Г├ B (удаление &)

4. Г├ B Þ Г├ (Á È B) (введение È )

5. Г├ Á Þ Г├ (Á È B) (введение È )

6. Г1 + (Á È B); Г2 , Á + Ã ;Г3 , B ├ Ã Þ Г 1 ,Г 2 , Г3 ├ Ã (удаление È )

7. Г , Á ├ B Þ Г ├ (Á É B) ( введение É )

8. Г1 ├ ( Á É B ); Г2 ├ Á Þ Г1 , Г2 ├ В (удаление É )

9. Г, Á ├ Þ Г├ ù Á (введение ù )

10. Г1 ├ Á ; Г2 ├ ┐Á Þ Г1 , Г2 ├ (сведение к противоречию)

11. Г, ┐Á ├ Þ Г ├ Á (удаление ù )

12. Г ├ Þ Г ├ Á ( утончение )

13. Г├ Á Þ Г, В ├ Á ( расширение)

14. Г1, Á , В, Г2+ Ã Þ Г1, В, Á , Г2+ Ã ( перестановка)

15. Г1, Á , Á , Г2+ Ã Þ Г1, Á , Г2+ Ã ( сокращение)

16. Г4 ├ Á (х) Þ Г4 + " х Á (х) ( введение " )

17. Г ├ " х Á (х) Þ Г ├ Á (t) ( удаление " )

18. Г ├ Á (t) Þ Г├ $ х Á (х) ( введение $ )

19. Г4, Á (х) ├ D Þ Г4, $ х Á (х)├ D (удаление $ )

Понятия вывода в ИПС и т.п. определяются аналогично соответствующим понятиям для ИС (см. §3).

Определим исчисление ИП. Схемами аксиом исчисления ИП являются следующие выражения:

1. (Á É ( B É Á ))
2. ((Á É B) É ((Á É (B É Ã )) É ( Á É Ã )))
3. ((Á & B) É B)
4. ((Á & B) É Á )
5. ((Á É B) É ((Á É Ã ) É (Á É (B & Ã ))))
6. (Á É (Á È B))
7. (B É (Á È B))
8. ((Á É Ã ) É (( B É Ã ) É ((Á È B) É Ã )))
9. ((Á É ù B) É (B É ù Á ))
10. (ù ù Á É Á )
11. (" x Á (x) É Á (t))
12. ( Á (y) É $ x Á (x)).

В схемах аксиом 1 – 10 Á , В, Ã -- любые формулы, в схемах аксиом 11, 12 Á (x) – формула, t – терм, свободный для х в Á (x). Á ( t) – формула, полученная из Á (x) заменой всех свободных вхождений хt. на

Правила вывода ИП:

I.

III.

причем в правилах II и III х не входит свободно в Ã , а у не входит свободно в Á (х) и у свободно для х в Á (x). В называется непосредственным следствием формул Á и (Á É В) по правилу I; ( Ã É " у Á (у)) и ($ у Á (у) É Ã ) представляет собой непосредственные следствия формул (Ã É Á (у)) по правилу II и (ÁÉ Ã ) по правилу III соответственно. (х)

Выводом в ИП называется конечная последовательность формул Á 1,…, Á п такая, что для каждого i ( 1 £ i £ n) Á i есть либо аксиома, либо непосредственное следствие одной или двух предыдущих формул.

Квазивывод на множестве формул Г есть последовательность Á 1,…, Á п такая, что для каждого i ( 1 £ i £Á i есть либо аксиома, либо одна из формул Г, либо непосредственное следствие одной или двух предыдущих формул. n)

Для квазивывода Á 1,…, Á п из множества Г и каждого i ( 1 £ i £ n) определим по индукции множество формул D (Á i) Í Г:

1. если Á
i есть аксиома, то D (Ái) = Æ ,
2. если
Ái Î Г, то D (Ái) = { Ái},
3. если
Ái есть непосредственное следствие Ájи Ák ( j, k < i) то D (Ái) = D (Áj) ÈD (Ák)
4. если
Ái есть непосредственное следствие Áj (1 £ j< i), то D (Ái) = D (Áj).

Выводом из Г в ИП называется квазивывод Á 1,…, Á п удовлетворяющий условию: если Á i есть непосредственное следствие формулы Á j = (Ã É Á (х)) по правилу II или формулы Á j= ( Á (x) É Ã ) по правилу III, то х не входит свободно в формулы из D (Á j).

Формула Á называется выводимой в ИП ( символически ├ Á ), если существует вывод в ИП, оканчивающийся формулой Á .

Формула Á называется выводимой из Г в ИП (символически Г├ Á ), если существует вывод из Г в ИП, оканчивающийся формулой Á .

Множество формул Г назовем непротиворечивым, если не существует такой формулы Á , что Г├ Á и Г├ ┐Á . В противном случае Г назовем противоречивым.

Множество формул Г сигнатуры s назовем полным, если для любой замкнутой формулы Á сигнатуры s Г├ Á или Г├ ┐Á . В противном случае Г назовем неполным.