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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

4. Равносильность исчисления секвенций
и исчисления высказываний
Сравнивая две формальные теории, будем использовать их со-
кращенные названия: ИС — исчисление секвенций, ИВ — исчисление
высказываний.
Лемма 1. Доказуемость в ИС секвенции A
1
, . . . , A
n
` B равно-
сильна доказуемости в ИС формулы
A
1
⇒ (A
2
⇒ (. . . ⇒ (A
n
⇒ B) . . .)).
В одну сторону проверяется применением правила введения ⇒, в
другую — применением правила удаления ⇒.
Лемма 2. Все аксиомы ИВ являются доказуемыми формулами
ИС.
В силу леммы 1, очевидно, достаточно доказать секвенции:
1) A, B ` A; 6) A ` A ∨ B;
2) A ⇒ (B ⇒ C), A ⇒ B, A ` C; 7) B ` A ∨ B;
3) A ∧ B ` A; 8) A ⇒ C, B ⇒ C, A ∨ B ` C;
4) A ∧ B ` B; 9) A ⇒ B, A ⇒ ¬B ` ¬A;
5) A, B ` A ∧ B; 10) ¬¬A ` A.
Аксиомы 11–13 в силу соглашения о смысле эквиваленции в ИС попа-
дают под действие аксиом 3–5.
Докажем, для примера, секвенцию 8. Введем обозначение Γ =
= {A ⇒ C , B ⇒ C, A ∨ B}.
A ⇒ C , A ` C
Γ, A ` C
B ⇒ C, B ` C
Γ, B ` C
A ∨ B ` A ∨ B
Γ ` A ∨ B
A ⇒ C, B ⇒ C, A ∨ B ` C
.
Вывод секвенций A ⇒ B, A ` B (а именно такой вид имеют оставши-
еся секвенции наверху первой и второй ветви) проведен в левой ветви
доказательства в примере 3.
Теорема 2. 1) Секвенция Γ ` A тогда и только тогда доказуема
в ИС, когда A выводима из Γ в ИВ.
2) Секвенция Γ ` тогда и только тогда доказуема в ИС, когда
формула P ∧ ¬P выводима из Γ в ИВ.
55

Страницы