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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

S
S H
1
S
Γ → ∆, A A, Γ → ∆
Γ → ∆
(Cut) .
A A
Γ → ∆, A A, Γ → ∆
Γ → ∆
A ∈ Γ A ∈ ∆ A 6∈ Γ
Γ → ∆, A B
0
B
0
∈ Γ B
0
∈ ∆ A 6∈ ∆
A
A = C
¡
¢
D
Γ → ∆, C
¡
¢
D C
¡
¢
D, Γ → ∆
Γ → ∆
.
Γ → ∆, C
¡
¢
D
C, Γ → ∆, D
(→
¡
¢
)
0
C
¡
¢
D, Γ → ∆
D, Γ → ∆ Γ → ∆, C
(
¡
¢
→)
0
.
D, Γ → ∆
D, C, Γ → ∆
(+ `) C, Γ → ∆, D
C, Γ → ∆ Γ → ∆, C
Γ → ∆
(Cut)
(Cut)
A ¤
S
Γ
1
→ ∆
1
, A A, Γ
2
→ ∆
2
Γ
1
, Γ
2
→ ∆
1
, ∆
2
.
2. Èñ÷èñëåíèå S ñåêâåíöèàëüíîãî òèïà                                  123


2.3 Äîïóñòèìîñòü ñå÷åíèÿ. Ýêâèâàëåíòíîñòü ÈÑ S è È H1

Òåîðåìà 3.10 (Î äîïóñòèìîñòè ñå÷åíèÿ).  ÈÑ S äîïóñòèìî ïðà-
âèëî ñå÷åíèÿ
                 Γ → ∆, A A, Γ → ∆
                                             (Cut) .
                        Γ→∆
Äîêàçàòåëüñòâî. Òåîðåìà äîêàçûâàåòñÿ èíäóêöèåé ïî ïîñòðîåíèþ
âûñåêàåìîé ôîðìóëû A. Ïðè ôèêñèðîâàííîé ñëîæíîñòè A óòâåðæäå-
íèå áóäåì äîêàçûâàòü èíäóêöèåé ïî ñóììå âûñîò èìåþùèõñÿ âûâîäîâ
Γ → ∆, A è A, Γ → ∆.
   Íà÷àëî äàííîé äâîéíîé èíäóêöèè ñîñòîèò â ðàññìîòðåíèè ñëó÷àÿ,
êîãäà âûñåêàåòñÿ àòîìàðíàÿ ôîðìóëà è îáå ñåêâåíöèè-ïîñûëêè â Cut
ñóòü àêñèîìû. Òîãäà ÿâëÿåòñÿ àêñèîìîé è Γ → ∆. Äåéñòâèòåëüíî, ýòî
î÷åâèäíî, åñëè A ∈ Γ è A ∈ ∆. Ïóñòü òåïåðü A 6∈ Γ. Íî òîãäà, ïîñêîëü-
êó Γ → ∆, A  àêñèîìà, íàéä¼òñÿ àòîìàðíàÿ ôîðìóëà B0 òàêàÿ, ÷òî
B0 ∈ Γ è B0 ∈ ∆. Àíàëîãè÷íî, åñëè A 6∈ ∆.
   Äàëåå íåîáõîäèìî ðàññìîòðåòü âñå âèäû ôîðìóëû A â çàâèñèìîñòè
îò ãëàâíîé ñâÿçêè.
                            ¡
   Ïóñòü, íàïðèìåð, A = C ¢ D, ò.å. äîêàçûâàåìîå ïðàâèëî èìååò âèä
                          ¡     ¡
                 Γ → ∆, C ¢ D C ¢ D, Γ → ∆
                                           .
                            Γ→∆
Ïðèìåíÿÿ îáðàù¼ííûå ïðàâèëà ê ñåêâåíöèÿì-ïîñûëêàì, ïîëó÷àåì
            ¡                          ¡
 Γ → ∆, C ¢ D        ¡              C ¢ D, Γ → ∆                 ¡
                  (→ ¢) 0   è                                  ( ¢ →) 0 .
  C, Γ → ∆, D                   D, Γ → ∆     Γ → ∆, C
Äàëåå èìååì
             D, Γ → ∆
                        (+ `)   C, Γ → ∆, D
            D, C, Γ → ∆
                                                       (Cut)
               C, Γ → ∆   Γ → ∆, C
                                    (Cut)
                      Γ→∆
Ïðèìåíåíèå (äâóêðàòíîå) ïðàâèëà Cut âîçìîæíî ïî èíäóêòèâíîìó
ïðåäïîëîæåíèþ.
   Äðóãèå âèäû ôîðìóëû A ðàññìàòðèâàþòñÿ àíàëîãè÷íî.       ¤

   Çàìåòèì, ÷òî èíîãäà ïîä ñå÷åíèåì â ÈÑ S ïîíèìàþò ïðàâèëî
                     Γ1 → ∆1 , A A, Γ2 → ∆2
                                             .
                         Γ 1 , Γ 2 → ∆1 , ∆2

Страницы