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

UptoLike

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

Рубрика: 

Γ, A
1
, . . . , A
m
` B Γ, Γ
Σ Σ
1
= Σ
2
Σ
1
Σ
2
Ax(N)
A ` A .
A
N
Rl(N)
Σ Σ
1
, . . . , Σ
m
Σ
1
. . . Σ
m
Σ
,
N `
Rl(N) +
Γ
+ N
Γ ` A Γ ` B
Γ, Γ ` A N B
N
Γ ` A N B
Γ ` A
,
Γ ` A N B
Γ ` B
;
+
Γ ` A
Γ ` A B
,
Γ ` B
Γ ` A B
;
Γ ` A B Γ, A ` C Γ, B ` C
Γ ` C
;
+
¡
¢
Γ, A ` B
Γ ` A
¡
¢
B
;
¡
¢
Γ ` A
¡
¢
B Γ ` A
Γ ` B
;
RA
Γ ` A Γ ` ¬ A
Γ `
;
90                  Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


ïèøåì Γ, A1 , . . . , Am ` B è Γ, ∆ âìåñòî Γ ∪ ∆.  êà÷åñòâå ìåòàÿçû-
êîâîé ïåðåìåííîé äëÿ ñåêâåíöèé ìû áóäåì èñïîëüçîâàòü ïðîïèñíóþ
ãðå÷åñêóþ áóêâó Σ. Ðàâåíñòâî Σ1 = Σ2 îçíà÷àåò ñèíòàêñè÷åñêîå ðà-
âåíñòâî (òîæäåñòâî) ñåêâåíöèé Σ1 è Σ2 .
   Àêñèîìû Ax(N ) ïðåäñòàâëåíû åäèíñòâåííîé ñõåìîé ñåêâåíöèé
                              A ` A.
Ïðè ïîäñòàíîâêå â äàííóþ ñõåìó âìåñòî ìåòàñèìâîëà A ïðîèçâîëüíûõ
ôîðìóë ïîëó÷àþòñÿ ÷àñòíûå ñëó÷àè ñõåìû, êîòîðûå è áóäóò ÿâëÿòüñÿ
àêñèîìàìè ÈÑ N . Òàêèì îáðàçîì, â ÈÑ âûâîäÿòñÿ èìåííî ñåêâåíöèè,
à íå ôîðìóëû.
   Ïðàâèëà âûâîäà Rl(N ), ïîñòóëèðóþùèå íà âûâîäèìîñòü ñåêâåíöèè
Σ èç ñåêâåíöèé Σ1 , . . . , Σm çàïèñûâàþò â âèäå ñõåì
                             Σ1 . . . Σm
                                         ,
                                  Σ
íàçûâàÿ ñåêâåíöèè íàä ÷åðòîé ïîñûëêàì, à ñåêâåíöèþ ïîä ÷åðòîé  çà-
êëþ÷åíèåì. Ïðè ïîäñòàíîâêå â óêàçàííûõ ñõåìàõ êîíêðåòíûõ ôîðìóë
âìåñòî ìåòàñèìâîëîâ ïîëó÷èì ÷àñòíûå ñëó÷àè ïðàâèë âûâîäà . Ïðàâè-
ëà âûâîäà â ÈÑ N çàäàþò ñâîéñòâà çíàêà ` îòíîñèòåëüíî ëîãè÷åñêèõ
ñâÿçîê.
   Ìíîæåñòâî Rl(N ) ñîñòàâëÿþò ñëåäóþùèå ñõåìû, ãäå çíàêàìè +
è − îáîçíà÷åíû ââåäåíèå è óäàëåíèå ñîîòâåòñòâóþùåé ñâÿçêè, à Γ 
ìóëüòèìíîæåñòâî ôîðìóë, âîçìîæíî ïóñòîå.
              Γ ` A     Γ ` B
     (+ N)                    ;
                Γ, Γ ` A N B
              Γ ` ANB          Γ ` ANB
     (− N)            ,                ;
                Γ ` A            Γ ` B
                Γ ` A           Γ ` B
     (+ ∨)            ,               ;
              Γ ` A∨B         Γ ` A∨B
              Γ ` A∨B       Γ, A ` C         Γ, B ` C
     (− ∨)                                              ;
                             Γ ` C
        ¡      Γ, A ` B
     (+ ¢)            ¡ ;
              Γ ` A ¢B
                      ¡
        ¡     Γ ` A ¢B     Γ ` A
     (− ¢)                       ;
                     Γ ` B
             Γ ` A      Γ ` ¬A
     (RA)                      ;
                     Γ `