Элементы математической логики. Фролов И.С. - 68 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

§9. Формальные теории
Различают:
— формальные теории нулевого порядка (исчисление высказыва-
ний и исчисление секвенций);
— формальные теории первого порядка (исчисление предикатов
и их расширения, о которых речь пойдет в настоящем параграфе);
— формальные теории второго и более высоких порядков.
1. Исчисление предикатов
Алфавит и правила построения формул исчисления предикатов
(первого порядка) мы уже определили, изучая логику первого порядка.
Возможны различные подходы к заданию схем аксиом и правил
вывода (ср. § 5 и § 7). Будем придерживаться первого варианта.
Схемы аксиом исчисления предикатов включают в себя схемы ак-
сиом 1)–13) исчисления высказываний (п.1 § 5) и четыре дополнитель-
ные схемы аксиом для кванторов:
Q1) ∀xA(x) ⇒ A(t);
Q2) A(t) ⇒ ∃xA(x);
Q3) ∀x(A ⇒ B) ⇒ (A ⇒ ∀xB);
Q4) ∀x(A ⇒ B) ⇒ (∃xA ⇒ B);
причем в схемах аксиом Q1), Q2) терм t свободен для x в A(x), в схеме
Q3) переменная x не свободна в A, в схеме Q4) x не свободна в B.
Множество правил вывода состоит из двух правил: знакомого
нам правила отделения (MP) и правила обобщения, или генерализации
(Gen):
A, A ⇒ B
B
(MP),
A
∀xA
(Gen).
Очевидно, что аксиомы Q1)–Q4) суть общезначимые формулы ло-
гики предикатов. Однако правило обобщения не удовлетворяет опреде-
лению логического следования, но удовлетворяет слабому логическому
следованию: для всякой интерпретации (не расширенной), в которой
истинна формула A, истинна формула ∀xA. Поэтому, определяя поня-
тие вывода, необходимо учесть особую роль правила обобщения.
Определение 1. Выводом формулы B из списка гипотез Γ на-
зывается последовательность формул B
1
, B
2
, . . . , B
m
= B, каждая из
которых есть либо гипотеза, либо аксиома, либо получена по прави-
лу вывода из предшествующих формул последовательности; причем
67

Страницы