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

UptoLike

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

Рубрика: 

Пример 1. Аксиомами, получаемыми из схемы 1, т.е. из
A (B A), являются: P (P P ), P ((Q R) P ),
Q (P Q), ¬P (P Q ¬P ) и т.д.
Согласно правилу отделения, из формул P Q, P Q P непо-
средственно выводима формула P .
2. Выводимость
Определение 1. (Формальным) выводом формулы B из спис-
ка формул Γ = {A
1
, A
2
, . . . , A
n
} называется последовательность
B
1
, B
2
, . . . , B
m
, в которой каждая формула B
i
(1 6 i 6 m) являет-
ся:
либо одной из формул списка Γ,
либо одной из аксиом,
либо получена по правилу MP из двух формул, расположен-
ных в этой последовательности раньше нее;
последняя формула B
m
совпадает с B.
Говорят, что формула B выводима из Γ = {A
1
, A
2
, . . . , A
n
}, если
существует вывод формулы B из списка Γ. Для выводимости использу-
ют обозначение A
1
, A
2
, . . . , A
n
` B или Γ ` B. Формулы A
i
из списка Γ
называются гипотезами, или допущениями вывода. Выражение Γ ` B
называется секвенцией. Последовательность гипотез в списке не играет
роли, поэтому мы будем обращаться с Γ как с множеством, хотя для
удобства будем ссылаться на порядковые номера гипотез и опускать
фигурные скобки при перечислении гипотез.
Пример 2. Покажем, что P (Q R), P Q ` R. Будем
строить вывод, нумеруя последовательные шаги вывода и объясняя
их.
1. P Q (гипотеза 2).
2. P Q P (аксиома 3).
3. P (MP, 1, 2).
4. P (Q R) (гипотеза 1).
5. Q R (MP, 3, 4).
6. P Q Q (аксиома 4).
7. Q (MP, 1, 6).
8. R (MP, 7, 5).
Определение 2. (Формальным) доказательством формулы B
называется вывод этой формулы из пустого списка формул, т.е. по-
следовательность формул B
1
, B
2
, . . . , B
m
, в которой каждая формула
38