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

UptoLike

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

Рубрика: 

Σ 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, Γ → ∆ âûâîäèìà.
      Äðóãèå ïðàâèëà ðàññìàòðèâàþòñÿ àíàëîãè÷íî.                 ¤

   Òàêæå, êàê è â ïðåäûäóùèõ ñëó÷àÿõ, ìîæíî óòâåðæäàòü, ÷òî èñ-
ïîëüçîâàíèå äàííûõ ïðàâèë íå óâåëè÷èâàåò âûñîòó äåðåâà âûâîäà è
êîëè÷åñòâà ñåêâåíöèé â í¼ì.