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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

Γ ` A; Γ ` ¬A
Γ `
Γ, ¬A `
Γ ` A
(вв. и уд. ¤).
Γ ` A
Γ, B ` A
(утончение).
Отметим, что имеется два правила удаления ∧ и два правила вве-
дения ∨.
2. Дерево доказательства
Вместо линейного вывода в исчислении секвенций по традиции
используется древовидный вывод, или дерево доказательства.
Определение. Деревом доказательства называется конструк-
ция, построенная при помощи следующих правил:
(1) аксиома является деревом доказательства, состоящим только
из корня — самой этой аксиомы;
(2) если T
1
, . . . , T
k
— деревья доказательства с корнями R
1
, . . . ,
R
k
и
R
1
, . . . , R
k
Σ
— правило вывода, где Σ — некоторая секвенция, то
T
1
, . . . , T
k
Σ
— дерево доказательства с корнем Σ.
Секвенция Σ называется доказуемой, если существует дерево до-
казательства с корнем Σ. Формула F называется доказуемой, если до-
казуема секвенция ` F .
Пример 1. Докажем секвенцию A ∧ B ` B ∧ A.
A ∧ B ` A ∧ B
A ∧ B ` B
(уд.∧
2
)
A ∧ B ` A ∧ B
A ∧ B ` A
(уд.∧
1
)
A ∧ B ` B ∧ A
(вв.∧).
Пример 2. Еще проще выводится секвенция A, B ` A ∧ B:
A ` A
A, B ` A
(ут.)
B ` B
A, B ` B
(ут.)
A, B ` A ∧ B
(вв.∧).
Справа от черты мы указываем на применяемое правило. Однако
ввиду частого использования правила утончения не будем указывать
на его применение.
51

Страницы