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

UptoLike

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

Рубрика: 

` A ¬A (−∨)
¬A B ` A
¡
¢
B
A ` A ¬A ` ¬A
A, ¬A `
(RA)
A, ¬A ` B
(DS) B ` B ¬A B ` ¬A B
¬A B, A ` B
¬A B ` A
¡
¢
B
(+
¡
¢
)
−∨
A N B ' B N A
A N B ` A N B
A N B ` B
( N)
A N B ` A N B
A N B ` A
( N)
A N B ` B N A
(+ N)
B N A ` A N B
¤
Γ ` A B
Γ, A ` B Γ, B ` A
` A B
A ` A
Γ ` (A
¡
¢
B) N (B
¡
¢
A)
Γ ` A
¡
¢
B
( N)
Γ, A ` B
(
¡
¢
)
Γ, A ` B Γ, B ` A
Γ, A ` B Γ, B ` A
Γ, A ` B
Γ ` A
¡
¢
B
(+
¡
¢
)
Γ, B ` A
Γ ` B
¡
¢
A
(+
¡
¢
)
Γ ` (A
¡
¢
B) N (B
¡
¢
A)
(+ N)
Γ ` A B ¤
104                 Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


      Òåïåðü, ïðèìåíÿÿ ê ýòèì è äîêàçàííîé â ïðèìåðå 3.3 ñåêâåíöèè
      ` A ∨ ¬A ïðàâèëî (−∨), ïîëó÷àåì òðåáóåìîå.
                                                          ¡
      Ïîêàæåì òåïåðü âûâîäèìîñòü ñåêâåíöèè ¬A ∨ B ` A ¢ B :
       A ` A    ¬A ` ¬A
                          (RA)
           A, ¬A `
                               (DS) B ` B ¬A ∨ B ` ¬A ∨ B
             A, ¬A ` B
                       ¬A ∨ B, A ` B     ¡
                                   ¡ (+ ¢)
                      ¬A ∨ B ` A ¢ B
     (ïðåäïîñëåäíèé ïåðåõîä îñóùåñòâë¼í ïî ïðàâèëó ( −∨) ).
  3. A N B ' B N A
         ANB ` ANB                ANB ` ANB
                            (− N)                   (− N)
          ANB ` B                  ANB ` A                  (+ N)
                            ANB ` BNA
      è àíàëîãè÷íî ïîêàçûâàåòñÿ B N A ` A N B .
¾Îñòàëüíûå ýêâèâàëåíòíîñòè ÷èòàòåëü ëåãêî äîêàæåò ñàì, èñïîëüçóÿ
íàâûê, ïðèîáðåò¼ííûé ïðè ðàçáîðå ðàíåå ïðèâåä¼ííûõ äîêàçàòåëüñòâ¿
([6], ñ. 38).                                                   ¤


Òåîðåìà 3.3. Ñåêâåíöèÿ Γ ` A ≡ B äîêàçóåìà, åñëè òîëüêî åñëè
äîêàçóåìû ñåêâåíöèè Γ, A ` B è Γ, B ` A.
Äîêàçàòåëüñòâî. Äîñòàòî÷íîñòü. Ïóñòü ñåêâåíöèÿ ` A ≡ B äîêà-
çóåìà. Òîãäà
                           ¡        ¡
                   Γ ` (A ¢ B) N (B ¢ A)
        A ` A                   ¡           (− N)
                        Γ ` A ¢B                         ¡
                                                      (− ¢)
                        Γ, A ` B
åñòü äîêàçàòåëüñòâî ñåêâåíöèè Γ, A ` B . Äîêàçóåìîñòü Γ, B ` A
óñòàíàâëèâàåòñÿ àíàëîãè÷íî.
   Íåîáõîäèìîñòü. Ïóñòü ñåêâåíöèè Γ, A ` B è Γ, B ` A äîêàçóåìû.
Òîãäà
        Γ, A ` B       ¡         Γ, B ` A        ¡
               ¡    (+ ¢)               ¡     (+ ¢)
       Γ ` A ¢B                 Γ ` B ¢A                (+ N)
                          ¡¢        ¡¢
                   Γ ` (A B) N (B A)
åñòü äîêàçàòåëüñòâî ñåêâåíöèè Γ ` A ≡ B .                           ¤