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

UptoLike

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

Рубрика: 

Γ `
Γ ` A
Γ ` RA
Γ ` A
0
Γ ` ¬ A
0
A
0
Γ ` A
0
Γ ` ¬ A
0
Γ ` A
0
Γ, ¬ A ` A
0
(+ `)
Γ ` ¬ A
0
Γ, ¬ A ` ¬ A
0
(+ `)
Γ, ¬ A `
Γ ` A
(−¬)
(RA) .
Γ, A `
Γ ` ¬ A
−¬
Γ, A ` RA
Γ, A ` A
0
Γ, A ` ¬ A
0
A
0
Γ, A ` A
0
Γ, A, ¬¬ A ` A
0
Γ, ¬¬ A ` A
¡
¢
A
0
(+
¡
¢
)
Γ, A ` ¬ A
0
Γ, A, ¬¬ A ` ¬ A
0
Γ, ¬¬ A ` A
¡
¢
¬ A
0
.
¬¬ A ` A
¡
¢
Γ, A ` A
0
¬¬ A ` A
Γ, ¬¬ A ` A
0
Γ, A ` ¬ A
0
¬¬ A ` A
Γ, ¬¬ A ` ¬ A
0
.
RA Γ, ¬¬ A ` −¬
Γ ` ¬ A
100                  Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé

         Γ `
  3.
        Γ ` A
       Ýòî ëîãè÷åñêîå ïðàâèëî  ôîðìàëèçàöèÿ ïðàâèëà Äóíñà Ñêîòà.
       ßñíî, ÷òî ñåêâåíöèþ Γ ` ìîæíî ïîëó÷èòü ëèøü ïî ïðàâèëó RA.
       Ïîýòîìó, åñëè äàííàÿ ñåêâåíöèÿ äîêàçóåìà, òî äîêàçóåìà ïàðà ñå-
       êâåíöèé Γ ` A0 è Γ ` ¬ A0 , ãäå A0  íåêîòîðàÿ êîíêðåòíàÿ
       ôîðìóëà. Ïîýòîìó äëÿ äîêàçàòåëüñòâà äîïóñòèìîñòè ðàññìàòðè-
       âàåìîãî ïðàâèëà äîñòàòî÷íî ïîñòðîèòü äåðåâî, íà÷àëüíûìè ñå-
       êâåíöèÿìè êîòîðîãî áóäóò ïàðà ñåêâåíöèé Γ ` A0 è Γ ` ¬ A0 .
       Ñëåäóþùåå äåðåâî ñëóæèò òàêèì äîêàçàòåëüñòâîì:

               Γ ` A0                    Γ ` ¬ A0
                          (+ `)                         (+ `)
            Γ, ¬ A ` A0               Γ, ¬ A ` ¬ A0
                                                                (RA) .
                           Γ, ¬ A `
                                       (−¬)
                            Γ ` A

       Γ, A `
  4.
       Γ ` ¬A
       Ýòî äâîéñòâåííîå ê (−¬) ëîãè÷åñêîå ïðàâèëî ôîðìàëèçóåò ðàñ-
       ñóæäåíèÿ îò ïðîòèâíîãî: åñëè ïðèíÿòèå ðàññìàòðèâàåìîãî óòâåð-
       æäåíèÿ âåä¼ò ê ïðîòèâîðå÷èþ, òî ýòî îçíà÷àåò, ÷òî óòâåðæäåíèå
       íåñïðàâåäëèâî.
       Ïîñêîëüêó Γ, A ` ìîæíî ïîëó÷èòü ëèøü ïî ïðàâèëó RA, òî
       äîëæíû áûòü âûâîäèìû ñåêâåíöèè Γ, A ` A0 è Γ, A ` ¬ A0 ,
       ãäå A0  íåêîòîðàÿ êîíêðåòíàÿ ôîðìóëà.
       Èìååì
           Γ, A ` A0                                      Γ, A ` ¬ A0
        Γ, A, ¬¬ A ` A0      ¡                         Γ, A, ¬¬ A ` ¬ A0
                     ¡    (+ ¢) è àíàëîãè÷íî                        ¡    .
       Γ, ¬¬ A ` A ¢ A0                               Γ, ¬¬ A ` A ¢ ¬ A0

       Çàòåì, äîáàâèâ ê äàííûì âûâîäàì ñåêâåíöèþ ¬¬ A ` A (ñì.
                                  ¡
       ïðèìåð 3.3), ïî ïðàâèëó (− ¢) ïîëó÷èì, ÷òî ñïðàâåäëèâû âûâîäû

         Γ, A ` A0 ¬¬ A ` A                   Γ, A ` ¬ A0 ¬¬ A ` A
                                      è                            .
             Γ, ¬¬ A ` A0                         Γ, ¬¬ A ` ¬ A0

       Çàòåì, ïðèìåíèâ ê çàêëþ÷èòåëüíûì ñåêâåíöèÿì äàííûõ âûâîäîâ
       ïðàâèëî RA, áóäåì èìåòü Γ, ¬¬ A `, îòêóäà ïî (−¬) ïîëó÷èì
       òðåáóåìîå Γ ` ¬ A.