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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

S
B A
¡
¢
B A
A B
Rl(S)
S
S
S
Γ → ∆, A A, Γ → ∆
Γ → ∆
S
A
S
Γ → ∆
A, Γ → ∆
(+ →)
Γ → ∆
Γ → ∆, A
(→ +) .
Γ → ∆
A, Γ → ∆ Γ → ∆, A
Γ → ∆
(→
¡
¢
)
A, Γ → ∆, B
Γ → ∆, A
¡
¢
B
.
2. Èñ÷èñëåíèå S ñåêâåíöèàëüíîãî òèïà                           117


÷àñòè. Ïîýòîìó è â âûâîäàõ ñåêâåíöèè, ðàñïîëîæåííûå âûøå âñÿêî-
ãî ïðàâèëà âûâîäà ñîñòîÿò èñêëþ÷èòåëüíî èç ïîäôîðìóë ôîðìóë â
ñåêâåíöèÿõ, âñòðå÷àþùèõñÿ â çàêëþ÷åíèè äàííîãî ïðàâèëà âûâîäà.
 ýòîì çàêëþ÷àåòñÿ ñâîéñòâî ïîäôîðìóëüíîñòè èñ÷èñëåíèÿ ñåêâåí-
öèé.
    Ïðè ðàññìîòðåíèè ïðàâèë âûâîäà ñíèçó ââåðõ ñâîéñòâî ïîäôîð-
ìóëüíîñòè îáåñïå÷èâàåò íà êàæäîì øàãå äðîáëåíèå ôîðìóë â ñåêâåí-
öèÿõ, ò.ê. íèêàêèõ íîâûõ ôîðìóë, êðîìå ïîäôîðìóë çàêëþ÷åíèÿ íå
ïîÿâëÿåòñÿ.  èñ÷èñëåíèÿõ ãèëüáåðòîâñêîãî òèïà ýòî íå òàê: ìû çíà-
                                                          ¡
åì, ÷òî ôîðìóëà B áûëà ïîëó÷åíà ïî MP èç ôîðìóë A ¢ B è A,
îäíàêî âîññòàíîâèòü ôîðìóëó A, çíàÿ ëèøü B , íåâîçìîæî. Êðîìå òî-
ãî, êàæäàÿ ïàðà ïðàâèë èç Rl(S) åäèíñòâåííûì îáðàçîì îïðåäåëÿåò
âîçìîæíîñòè ïîÿâëåíèÿ ñîîòâåòñòâóþùåé ñâÿçêè. Ýòî îñòàâëÿåò î÷åíü
ìàëî ñâîáîäû âûáîðà ïîñûëîê, èç êîòîðûõ ìîæíî âûâåñòè äàííóþ ñå-
êâåíöèþ, â çíà÷èòåëüíîé ìåðå ïðåäîïðåäåëÿÿ ñïîñîá âûâîäà äàííîé
òåîðåìû. Îòìå÷åííûå ñâîéñòâà ÈÑ S ÷ðåçâû÷àéíî îáëåã÷àåò ïîèñê
âûâîäà äàííîé ñåêâåíöèè.
    Äëÿ óäîáíîãî îñóùåñòâëåíèÿ ïîèñêà âûâîäà â S íåîáõîäèìî äî-
êàçàòü íåêîòîðûå ñâîéñòâà ýòîãî èñ÷èñëåíèÿ, ÷òî è áóäåò ñäåëàíî äà-
ëåå. Îñíîâíûì ôàêòîì çäåñü ÿâëÿåòñÿ òåîðåìà îá óñòðàíåíèè ñå÷åíèÿ
(Cut).  ÈÑ S ïîä ñå÷åíèåì ïîíèìàþò ïðàâèëî âûâîäà
                       Γ → ∆, A A, Γ → ∆
                             Γ→∆
Òåîðåìà óòâåðæäàåò, ÷òî ýòî ïðàâèëî äîïóñòèìî â ÈÑ S , ò.å. åãî èñ-
ïîëüçîâàíèå íå ðàñøèðÿåò ìíîæåñòâà âûâîäèìûõ ñåêâåíöèé. Çàìåòèì,
÷òî ïðàâèëî Cut íå îáëàäàåò ñâîéñòâîì ïîäôîðìóëüíîñòè, ò.ê. ôîðìó-
ëà A â í¼ì íèêàê íå ñâÿçàíà ñ íèæíåé ñåêâåíöèåé.
Ëåììà 3.7. Â ÈÑ S äîïóñòèìû ñëåäóþùèå ïðàâèëà äîáàâëåíèÿ â
àíòåöåäåíò è ñóêöåäåíò (ïðàâèëà îñëàáëåíèÿ):
           Γ→∆                          Γ→∆
                     (+ →)      è                 (→ +) .
          A, Γ → ∆                     Γ → ∆, A
Äîêàçàòåëüñòâî. Èñïîëüçóåì èíäóêöèþ ïî âûñîòå äåðåâà âûâîäà ñå-
êâåíöèé.
   Åñëè Γ → ∆  àêñèîìà, òî àêñèîìàìè ÿâëÿþòñÿ îáå ñåêâåíöèè
A, Γ → ∆ è Γ → ∆, A.
   Äàëåå ñëåäóåò ðàçîáðàòü âñå ñëó÷àè, êîãäà ñåêâåíöèÿ Γ → ∆ ïîëó-
÷åíà ïî îäíîìó èç ïðàâèë âûâîäà. Ïóñòü, íàïðèìåð, îíà ïîëó÷åíà ïî
             ¡
ïðàâèëó (→ ¢):
                           A, Γ → ∆, B
                                      ¡ .
                          Γ → ∆, A ¢ B

Страницы