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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

S
S
→
`
H
1
A ⇒ `
S
→ A
A H
1
S H
1
`
S
→ (A
¡
¢
C)
¡
¢
((B
¡
¢
C)
¡
¢
(A ∨ B
¡
¢
C))
A
1
8
A
¡
¢
C, B
¡
¢
C → A
¡
¢
C
A
¡
¢
C, B
¡
¢
C, A → C
(→
¡
¢
)
0
A
¡
¢
C, B
¡
¢
C → B
¡
¢
C
A
¡
¢
C, B
¡
¢
C, B → C
(→
¡
¢
)
0
A
¡
¢
C, B
¡
¢
C, A ∨ B → C
(∨ →)
(→
¡
¢
)
S `
S
→ A `
S
→ A
¡
¢
B
124                    Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


Ïîíÿòíî, ÷òî òàêàÿ çàìåíà íå ïîâëèÿåò íà ñïðàâåäëèâîñòü äîêàçàííîé
òåîðåìû.
     ââåä¼ííîì Ãåíöåíîì ÈÑ ïðàâèëî Cut âõîäèëî â ñïèñîê îñíîâíûõ
è äîêàçàííàÿ èì òåîðåìà ¾îá óñòðàíåíèè ñå÷åíèÿ¿ (¾îñíîâíàÿ òåîðåìà
Ãåíöåíà¿) óòâåðæäàëà, ÷òî âûâîä ëþáîé ñåêâåíöèè ìîæåò áûòü ïîëó-
÷åí áåç ïðèìåíåíèÿ ýòîãî ïðàâèëà6 . Äîêàçàòåëüñòâà áåç èñïîëüçîâàíèÿ
ïðàâèëà ñå÷åíèÿ íàçûâàþò íîðìàëüíûìè . Ñóòü òåîðåìû îá óñòðàíåíèè
ñå÷åíèÿ â òîì, ÷òî íîðìàëüíûå âûâîäû ïîëíû: âñ¼, ÷òî äîêàçóåìî â ÈÑ
S , ìîæíî äîêàçàòü â íîðìàëüíîé ôîðìå. Ïðàêòè÷åñêè æå ïðèìåíåíèå
ïðàâèëà ñå÷åíèÿ çíà÷èòåëüíî îáëåã÷àåò âûâîä ñåêâåíöèé.
    Ñ ïîìîùüþ òåîðåìû Ãåíöåíà îá óñòðàíåíèè ñå÷åíèÿ ëåãêî äîêàçû-
âàåòñÿ íåïðîòèâîðå÷èâîñòü ÈÑ S . Äåéñòâèòåëüíî, êàê ëåãêî âèäåòü,
ïóñòàÿ ñåêâåíöèÿ → ìîæåò ïîëó÷èòüñÿ òîëüêî â ðåçóëüòàòå ïðèìåíå-
íèÿ ïðàâèëà ñå÷åíèÿ (åäèíñòâåííîå ïðàâèëî, ïîíèæàþùåå îáùåå ÷èñëî
ñèìâîëîâ ôîðìóë â ñåêâåíöèè). Â ñèëó óñòðàíèìîñòè Cut òàêîé âûâîä
íåâîçìîæåí. Îòìåòèì, ÷òî ýòî  ÷èñòî ñèíòàêñè÷åñêîå äîêàçàòåëüñòâî
íåïðîòèâîðå÷èâîñòè.
    Òåîðåìà Ãåíöåíà èãðàåò êëþ÷åâóþ ðîëü â äîêàçàòåëüñòâå ýêâèâà-
ëåíòíîñòè ÈÑ è ÈÂ. Ýòà ýêâèâàëåíòíîñòü ôîðìóëèðóåòñÿ â ñëåäóþùèõ
äâóõ ëåììàõ.

Ëåììà 3.13.        `H1 A ⇒ `S → A.

Äîêàçàòåëüñòâî. Äîêàçàòåëüñòâî ïðîâîäèòñÿ èíäóêöèåé ïî äëèíå âû-
âîäà A â H1 .
   Ñíà÷àëà óáåæäàåìñÿ, ÷òî â ÈÑ S âûâîäèìû âñå àêñèîìû È H1 .
                               ¡  ¡    ¡     ¡       ¡
Ïîêàæåì, íàïðèìåð, `S → (A ¢ C) ¢ ((B ¢ C) ¢(A ∨ B ¢ C)) (àêñè-
îìà A1 8). Äåéñòâèòåëüíî, èìååì
   ¡         ¡¢          ¡                 ¡     ¡      ¡
A ¢ C, B        C → A ¢C          ¡    A ¢ C, B ¢ C → B ¢ C                 ¡
    ¡          ¡¢             (→ ¢) 0       ¡¢    ¡¢                     (→ ¢) 0
 A ¢ C, B         C, A → C              A C, B C, B → C
                            ¡       ¡
                          A ¢ C, B ¢ C, A ∨ B → C

(ïîñëåäíèé ïåðåõîä ñäåëàí ïî ïðàâèëó (∨ →) ). Òðèæäû ïðèìåíÿÿ ê
                                      ¡
çàêëþ÷èòåëüíîé ñåêâåíöèè ïðàâèëî (→ ¢) ïîëó÷èì òðåáóåìûé âûâîä.
   Äàëåå óáåæäàåìñÿ, ÷òî ïðàâèëî âûâîäà ÌÐ ñîõðàíÿåò âûâîäèìîñòü
                                                 ¡
â ÈÑ S . Äåéñòâèòåëüíî, ïóñòü `S → A è `S → A ¢ B . Ïîêàæåì, ÷òî

   6 Îòìåòèì, ÷òî ëåììà Ï.Ñ. Íîâèêîâà îá èñêëþ÷åíèé âñòàâîê ïðàâèëüíûõ ïðîõîä-
íûõ áóêâ â âûâîäàõ ðàâåíñòâ â ãðóïïîâûõ èñ÷èñëåíèÿõ (Òðóäû Ìàòåìàòè÷. èíñòèò-
òà èì. Â.À. Ñòåêëîâà, ò. 44, 1955) ÿâëÿåòñÿ àíàëîãîì òåîðåìû Ãåíöåíà îá óñòðàíåíèè
ñå÷åíèé â ëîãè÷åñêîì âûâîäå.

Страницы