Исчисления высказываний классической логики. Гуров С.И. - 119 стр.

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

S
`
S
Γ → ∆ Γ ∆
T Γ → ∆
Γ
0
T + Γ
0
Γ
0
T
T + Γ
0
Γ ∪ Γ
0
→ ∆
T
¤
Rl(S)
0
Rl(S)
A
¡
¢
B, Γ → ∆
Γ → ∆, A B, Γ → ∆
(
¡
¢
→)
0
.
A
¡
¢
B, Γ → ∆
Γ ∆
Γ → A, ∆ Γ, B → ∆
A
¡
¢
B, Γ → ∆
r
A
¡
¢
B
r A
¡
¢
B
(→ ¬)
C, A
¡
¢
B, Γ → ∆
1
A
¡
¢
B, Γ → ∆
1
, ¬ C
∆
1
= ∆, ¬ C
Γ → ∆
1
, A, ¬ C B, Γ → ∆
1
, ¬ C .
2. Èñ÷èñëåíèå S ñåêâåíöèàëüíîãî òèïà                            119


Ñëåäñòâèå.    `S Γ → ∆, åñëè íàáîðû Γ è ∆ ñîäåðæàò õîòÿ áû
îäíó îáùóþ ôîðìóëó. Îáðàòíîå, î÷åâèäíî, íåâåðíî.
   Ïîíÿòíî, ÷òî â äåðåâå âûâîäà ìîæíî â êà÷åñòâå ëèñòüåâ èñïîëüçî-
âàòü ñåêâåíöèè óêàçàííîãî âèäà.
Ëåììà 3.9. Ïóñòü T  äåðåâî äîêàçàòåëüñòâà ñåêâåíöèè Γ → ∆,
à Γ 0  íåêîòîðûé íàáîð ôîðìóë. Ïóñòü T + Γ 0  äåðåâî ñåêâåíöèé,
ïîëó÷åííîå äîáàâëåíèåì Γ 0 â àíòåöåäåíòû âñåõ ñåêâåíöèé èç T . Òîãäà
T + Γ 0 ÿâëÿåòñÿ äîêàçàòåëüñòâîì ñåêâåíöèè Γ ∪ Γ 0 → ∆.
Äîêàçàòåëüñòâî. Èñïîëüçóåì èíäóêöèþ ïî âûñîòå äåðåâà T . Áà-
çèñ èíäóêöèè î÷åâèäåí, à èíäóêöèîííûé ïåðåõîä îáåñïå÷èâàåòñÿ ëåì-
ìîé 3.7.                                                        ¤


   Çàìåíèì ìåñòàìè ïîñûëêè è çàêëþ÷åíèÿ â ïðàâèëàõ èç Rl(S), ïî-
ëó÷èì îáðàù¼ííûå ïðàâèëà. Èõ áóäåì îáîçíà÷àòü ñîîòâåòñòâóþùèìè
èìåíàìè ñî øòðèõîì 0 .
Ëåììà 3.10. Âñå ïðàâèëà âûâîäà èç Rl(S) îáðàòèìû, ò.å. åñëè âûâî-
äèìî çàêëþ÷åíèå êàêîãî-ëèáî ïðàâèëà, òî âûâîäèìû è âñå åãî ïîñûëêè.
Äîêàçàòåëüñòâî. Äëÿ êàæäîãî èç îáðàù¼ííûõ ïðàâèë ëåììà äîêàçû-
âàåòñÿ èíäóêöèåé ïî âûñîòå äåðåâà âûâîäà.
   Äîêàæåì, íàïðèìåð, ñïðàâåäëèâîñòü ïðàâèëà
                          ¡
                      A ¢ B, Γ → ∆          ¡
                                          ( ¢ →) 0 .
                 Γ → ∆, A       B, Γ → ∆
                        ¡
   Ïóñòü ñåêâåíöèÿ A ¢ B, Γ → ∆ åñòü àêñèîìà. Ýòî îçíà÷àåò, ÷òî
Γ è ∆ ñîäåðæàò îäíó è òó æå àòîìàðíóþ ôîðìóëó, íî òîãäà è îáå
ñåêâåíöèè Γ → A, ∆ è Γ, B → ∆ òàêæå ñîäåðæàò ýòó ôîðìóëó, ò.å.
ÿâëÿþòñÿ àêñèîìàìè è, ñëåäîâàòåëüíî, òðèâèàëüíî âûâîäèìû.
                              ¡
   Èíà÷å, ïóñòü ñåêâåíöèÿ A ¢ B, Γ → ∆ ïîëó÷åíà ïî îäíîìó èç ïðà-
âèë âûâîäà. Çäåñü èìåþò ìåñòî äâà ïîäñëó÷àÿ: ýòî ïðàâèëî r (a) íå
                                             ¡
ïðèìåíÿëîñü è (b) ïðèìåíÿëîñü ê ôîðìóëå A ¢ B .
                                               ¡
  a) Ïðàâèëî r íå ïðèìåíÿëîñü ê ôîðìóëå A ¢ B . Ïóñòü, íàïðèìåð,
     ðàññìàòðèâàåìàÿ ñåêâåíöèÿ ïîëó÷åíà ïî ïðàâèëó (→ ¬):
                                 ¡
                           C, A ¢ B, Γ → ∆1
                             ¡
                          A ¢ B, Γ → ∆1 , ¬ C
     ( ∆1 = ∆, ¬ C ). Òîãäà íàì íàäî ïîêàçàòü äîêàçóåìîñòü ñåêâåíöèé
               Γ → ∆1 , A, ¬ C     è     B, Γ → ∆1 , ¬ C .

Страницы