ВУЗ:
Составители:
Рубрика:
Пример 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
Страницы
- « первая
- ‹ предыдущая
- …
- 37
- 38
- 39
- 40
- 41
- …
- следующая ›
- последняя »