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

UptoLike

ВУЗ: 

СГАУ | Самара

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

Рубрика: 

Пример 3. Докажем секвенцию A ⇒ B, B ⇒ C ` A ⇒ C.
A ` A
A⇒B,A ` A
A⇒B ` A⇒B
A⇒B,A ` A⇒B
A ⇒ B, A ` B
A ⇒ B, B ⇒ C, A ` B
(уд. ⇒)
B ⇒ C ` B ⇒ C
A ⇒ B, B ⇒ C, A ` B ⇒ C
A ⇒ B, B ⇒ C, A ` C
A ⇒ B, B ⇒ C ` A ⇒ C
(вв. ⇒)
(уд. ⇒).
Мы рекомендуем строить деревья доказательств снизу вверх, на-
чиная с корней (т.е. с секвенций, которые требуется доказать) и по-
степенно наращивая дерево так, чтобы конечными секвенциями были
аксиомы. При этом следует пользоваться следующими эвристиками:
— если доказываемая секвенция имеет вид Γ ` A ∧ B, причем
Γ не содержит формулы A ∧B, то нужно применить правило введения
∧ и далее строить две ветви доказательства Γ ` A и Γ ` B;
— если доказываемая секвенция имеет вид Γ ` A ⇒ B, причем
Γ не содержит формулы A ⇒ B, то нужно применить правило введения
⇒ и далее доказывать Γ, A ` B;
— если доказываемая секвенция имеет вид Γ ` A ∨ B, причем
Γ не содержит формулы A ∨B, то можно применить правило введения
∨, но только в том случае, если можно вывести Γ ` A или Γ ` B;
— если формула A ∧B содержится в антецеденте, но не содер-
жится в консеквенте доказываемой секвенции, то можно попытаться
дойти до секвенций, в которых консеквент есть A или B, и применить
правило удаления ∧;
— если формула A ⇒ B содержится в антецеденте, но не содер-
жится в консеквенте доказываемой секвенции, то можно попытаться
дойти до секвенции, в которой консеквент есть B, и, применив прави-
ло удаления ⇒, перейти к доказательству секвенции с консеквентом
A;
— если формула A ∨ B содержится в антецеденте, но не со-
держится в консеквенте доказываемой секвенции, то можно, применив
правило удаления ∨, далее строить две ветви доказательства секвен-
ций, в которых A ∨B заменено на A и B соответственно;
— если вышеперечисленные приемы ничего не дают, надо об-
ратиться к доказательству от противного, т.е. применить правило уда-
ления противоречия, а затем (для вывода секвенции вида Γ ` ) —
правило введения противоречия.
Таким образом, при построении дерева доказательства правила
введения позволяют разбирать на части консеквент, а правила удале-
ния — антецедент секвенции.
52

Страницы