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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

Σ N
N Σ A
N N
Σ = ` A
` A
¡
¢
A
Σ : A ` A
Σ : ` A
¡
¢
A +
¡
¢
N
Σ
Σ
1
, . . . , Σ
l
= Σ, l > 1
Rl(N)
(+ `) Rl(N)
(+ N) (−
¡
¢
) RA (−∨)
(+ N )
Γ ` A ∆ ` B
Γ, ∆ ` A N B
,
− ∨
Γ
1
` A ∨ B Γ
2
, A ` C Γ
3
, B ` C
Γ
1
, Γ
2
, Γ
3
` C
.
Σ : Γ ` A
Σ : Γ, ∆ ` A (+ `)
Σ : ∆ ` B
Σ : Γ, ∆ ` B (+ `)
92                   Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


   Ñåêâåíöèÿ Σ íàçûâàåòñÿ âûâîäèìîé (äîêàçóåìîé , òåîðåìîé ) â N ,
åñëè ñóùåñòâóåò âûâîä â N , îêàí÷èâàþùèéñÿ Σ. Ôîðìóëà A èñ÷èñ-
ëåíèÿ N íàçûâàåòñÿ âûâîäèìîé (äîêàçóåìîé , òåîðåìîé ) â N , åñëè
âûâîäèìà ñåêâåíöèÿ Σ = ` A.
Ïðèìåð 3.1.
           ¡
  1. ` A ¢ A
      Σ1 : A ` A   àêñèîìà
               ¡                   ¡
      Σ2 : ` A ¢ A  ïî ïðàâèëó (+ ¢)
    Ñòàíäàðòíî, ïðàâèëî íàçûâàåòñÿ äîïóñòèìûì â ÈÑ N , åñëè
åãî èñïîëüçîâàíèå íå ðàñøèðÿåò ìíîæåñòâî âûâîäèìûõ ñåêâåíöèé.
Äîñòàòî÷íûì óñëîâèåì äîïóñòèìîñòè ïðàâèëà áóäåò âûâîäèìîñòü
ñåêâåíöèè-çàêëþ÷åíèÿ Σ ïðè óñëîâèè âûâîäèìîñòè ñåêâåíöèé-
ïîñûëîê. Òàêèì âûâîäîì íàçûâàåòñÿ êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü
Σ1 , . . . , Σl = Σ, l > 1 ñåêâåíöèé òàêàÿ, ÷òî êàæäûé ýëåìåíò ýòîé ïî-
ñëåäîâàòåëüíîñòè åñòü ëèáî àêñèîìà, ëèáî îäíà èç ñåêâåíöèé-ïîñûëîê,
ëèáî ïðÿìî ñëåäóåò èç êàêèõ ëèáî ïðåäûäóùèõ ñåêâåíöèé ïî îäíîìó
èç ïðàâèë Rl(N ).
    Ñ ó÷¼òîì ñòðóêòóðíîãî ïðàâèëà (+ `) , ëîãè÷åñêèå ïðàâèëà Rl(N )
                                                         ¡
èìåþùèå äâå è òðè ñåêâåíöèè-ïîñûëêè, ò.å. (+ N), (− ¢), RA è (−∨),
ìîãóò áûòü çàìåíåíû íà ñîîòâåòñòâóþùèå äîïóñòèìûå îáîáù¼ííûå.
 íèõ ñëåâà îò çíàêà âûâîäèìîñòè ñåêâåíöèè-ïîñûëêè èìåþò, âîîáùå
ãîâîðÿ, ðàçíûå íàáîðû ãèïîòåç, à ñåêâåíöèÿ-çàêëþ÷åíèå  îáúåäèíå-
íèå ýòèõ íàáîðîâ. Òîãäà, íàïðèìåð, ïðàâèëî (+ N ) áóäåò âûãëÿäåòü
êàê
                              Γ ` A     ∆ ` B
                                               ,
                                Γ, ∆ ` A N B
à (− ∨)  êàê

                Γ1 ` A ∨ B       Γ2 , A ` C     Γ3 , B ` C
                                                             .
                             Γ1 , Γ2 , Γ3 ` C
Äîêàçàòåëüñòâî äîïóñòèìîñòè òàêèõ îáîáù¼ííûõ ïðàâèë ýëåìåíòàðíî.
Íàïðèìåð, äëÿ ïåðâîãî èç ïðèâåä¼ííûõ ýòî
 Σ1 : Γ ` A  ïîñûëêà
 Σ2 : Γ, ∆ ` A  âîçìîæíî íåîäíîêðàòíîå ïðèìåíåíèå (+ `) ê
     ïðåäûäóùåìó
 Σ3 : ∆ ` B  ïîñûëêà
 Σ4 : Γ, ∆ ` B  âîçìîæíî íåîäíîêðàòíîå ïðèìåíåíèå (+ `) ê
     ïðåäûäóùåìó

Страницы