ВУЗ:
Составители:
Рубрика:
Σ A, A, Γ → ∆
Γ → A, A, ∆ Σ
0
Σ A
Σ
Σ Σ
0
Σ
r
A
r A
(→
¡
¢
)
A, A, C, Γ → ∆
1
, D
A, A, Γ → ∆
1
, C
¡
¢
D
.
A, C, Γ → ∆
1
, D
(→
¡
¢
)
Σ
0
r A
A C
¡
¢
D Σ
(
¡
¢
→)
D, C
¡
¢
D, Γ → ∆ C
¡
¢
D, Γ → ∆, C
C
¡
¢
D, C
¡
¢
D, Γ → ∆
.
(
¡
¢
→)
D, D, Γ → ∆
Γ → ∆, C, C
D, Γ → ∆ Γ → ∆, C (
¡
¢
→)
C
¡
¢
D, Γ → ∆
¤
122 Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé
Äîêàçàòåëüñòâî. Ïóñòü äàí âûâîä ñåêâåíöèè Σ âèäà A, A, Γ → ∆
èëè Γ → A, A, ∆. Ïîêàæåì, ÷òî ñóùåñòâóåò âûâîä ñåêâåíöèè Σ 0 , ïî-
ëó÷åííîé èç Σ çàìåíîé âñåõ ýêçåìïëÿðîâ ôîðìóëû A îäíèì ýêçåì-
ïëÿðîì è äàííûé âûâîä èìååò íå áîëüøóþ âûñîòó è íå áîëüøåå êîëè-
÷åñòâî ñåêâåíöèé, ÷åì âûâîä Σ. Äîêàçàòåëüñòâî ïðîâîäèòñÿ èíäóêöèåé
ïî âûñîòå äåðåâà âûâîäà.
Åñëè ñåêâåíöèÿ Σ àêñèîìà, òî è Σ 0 àêñèîìà.
Ïóñòü ñåêâåíöèÿ Σ ïîëó÷åíà ïî îäíîìó èç ïðàâèë âûâîäà. Ðàñ-
ñìîòðèì ñëåäóþùèå ïîäñëó÷àè: ýòî ïðàâèëî r (a) íå ïðèìåíÿëîñü íè
ê îäíîìó ýêçåìïëÿðó è (b) ïðèìåíÿëîñü ê õîòÿ áû îäíîìó ýêçåìïëÿðó
ñîêðàùàåìîé ôîðìóëû A.
a) Ïðàâèëî r íå ïðèìåíÿëîñü íè ê îäíîìó ýêçåìïëÿðó A. Â ýòîì
ñëó÷àå äëÿ âñåõ ïðàâèë ðàññóæäåíèÿ îäíîòèïíû.
Ïóñòü, íàïðèìåð, ðàññìàòðèâàåìàÿ ñåêâåíöèÿ ïîëó÷åíà ïî ïðà-
¡
âèëó (→ ¢):
A, A, C, Γ → ∆1 , D
¡ .
A, A, Γ → ∆1 , C ¢ D
Ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ ñåêâåíöèÿ A, C, Γ → ∆1 , D
¡
âûâîäèìà. Ïðèìåíÿÿ ê íåé ïðàâèëî (→ ¢) , ïîëó÷èì âûâîä ñå-
0
êâåíöèè Σ .
b) Ïðàâèëî r ïðèìåíÿëîñü ê õîòÿ áû îäíîìó ýêçåìïëÿðó A. Â ýòîì
ñëó÷àå ñóùåñòâåííà îáðàòèìîñòü ïðàâèë âûâîäà.
¡
Äîïóñòèì, íàïðèìåð, ÷òî A èìååò âèä C ¢ D, à ñåêâåíöèÿ Σ
¡¢
ïîëó÷åíà ïî ïðàâèëó âûâîäà ( →):
¡ ¡
D, C ¢ D, Γ → ∆ C ¢ D, Γ → ∆, C
¡ ¡ .
C ¢ D, C ¢ D, Γ → ∆
¡
Èñïîëüçóÿ îáðàòèìîñòü ïðàâèëà ( ¢ →) çàêëþ÷àåì, ÷òî èç ïåð-
âîé ñåêâåíöèè-ïîñûëêè âûâîäèìà ñåêâåíöèÿ D, D, Γ → ∆, à èç
âòîðîé Γ → ∆, C, C . Ïðè ýòîì äàííûå âûâîäû èìåþò íå áîëü-
øóþ ñëîæíîñòü, ÷åì ñîîòâåòñòâóþùèå âûâîäû ïðåäûäóùèõ ñå-
êâåíöèé.
Äàëåå ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ çàêëþ÷àåì, ÷òî âûâîäè-
¡
ìû è ñåêâåíöèè D, Γ → ∆ è Γ → ∆, C . Èç íèõ ïî ïðàâèëó ( ¢ →)
¡¢
ïîëó÷àåì òðåáóåìîå: ñåêâåíöèÿ C D, Γ → ∆ âûâîäèìà.
Äðóãèå ïðàâèëà ðàññìàòðèâàþòñÿ àíàëîãè÷íî. ¤
Òàêæå, êàê è â ïðåäûäóùèõ ñëó÷àÿõ, ìîæíî óòâåðæäàòü, ÷òî èñ-
ïîëüçîâàíèå äàííûõ ïðàâèë íå óâåëè÷èâàåò âûñîòó äåðåâà âûâîäà è
êîëè÷åñòâà ñåêâåíöèé â í¼ì.
Страницы
- « первая
- ‹ предыдущая
- …
- 120
- 121
- 122
- 123
- 124
- …
- следующая ›
- последняя »
