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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
Γ, A ` B
Γ, ¬ B ` ¬ A
Γ, A ` B ¬ B ` ¬ B
Γ, A, ¬ B `
(RA)
Γ, ¬ B ` ¬ A
(+¬)
¤
N
¬ A
¡
¢
(A
¡
¢
B)
A ` A ¬ A ` ¬ A
A, ¬ A `
A, ¬ A ` B
(DS)
¬ A ` A
¡
¢
B
` ¬ A
¡
¢
(A
¡
¢
B)
(+
¡
¢
) .
(+
¡
¢
)
(RA)
(A
¡
¢
B)
¡
¢
(¬ A ∨ B)
Σ : A
¡
¢
B ` A
¡
¢
B
Σ : A
¡
¢
B, A ` B −
¡
¢
Σ : A
¡
¢
B, A ` ¬ A ∨ B + ∨
Σ : A
¡
¢
B, ¬(¬ A ∨ B) ` ¬ A
Σ : A
¡
¢
B, ¬(¬ A ∨ B) ` ¬ A ∨ B + ∨
Σ : ¬(¬ A ∨ B) ` ¬(¬ A ∨ B)
Σ : A
¡
¢
B, ¬(¬ A ∨ B) ` Σ
5
Σ
6
RA
Σ : A
¡
¢
B ` ¬ A ∨ B −¬
Σ : ` (A
¡
¢
B)
¡
¢
¬ A ∨ B +
¡
¢
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                                101

          Γ, A ` B
  5.
        Γ, ¬ B ` ¬ A
       Ýòî ïðàâèëî  àíàëîã ïðàâèëà êîíòðàïîçèöèè.

                     Γ, A ` B      ¬B ` ¬B
                                             (RA)
                           Γ, A, ¬ B `
                                                     (+¬)
                              Γ, ¬ B ` ¬ A

                                                                  ¤

   Â íàòóðàëüíîì âûâîäå ïðèìåíÿþòñÿ äâå ïðîöåäóðû: íåïîñðåäñòâåí-
íîå ââåäåíèå îäíèõ ôîðìóë èç äðóãèõ (êàê â ãèëüáåðòîâñêèõ èñ÷èñëå-
íèÿõ) è ïîñòðîåíèå âñïîìîãàòåëüíûõ âûâîäîâ, èñïîëüçîâàíèå êîòîðûõ
ïîçâîëÿåò ñâîäèòü èñõîäíóþ çàäà÷ó äîêàçàòåëüñòâà ê áîëåå ïðîñòûì
ïîäçàäà÷àì. Ïðèâåä¼ì ïðèìåðû êâàçèâûâîäîâ â N .

       Ïðèìåð 3.4.
                                           ¡   ¡
        1) Äîêàæåì âûâîäèìîñòü ôîðìóëû ¬ A ¢(A ¢ B) (çàêîí îò-
       ðèöàíèÿ àíòåöåäåíòà).

                          A ` A     ¬A ` ¬A
                                                     (RA)
                         A, ¬ A `
                                    (DS)
                        A, ¬ A ` B             ¡
                                ¡¢          (+ ¢)
                      ¬A ` A B           ¡¢
                            ¡     ¡  (+ ) .
                     ` ¬ A ¢(A ¢ B)

                                               ¡     ¡
        2) Ïîêàæåì âûâîäèìîñòü ôîðìóëû (A ¢ B) ¢ (¬ A ∨ B). Òåõ-
       íè÷åñêè óäîáíåå äàòü ëèíåéíîå äîêàçàòåëüñòâî.
                   ¡        ¡
        Σ1   : A ¢ B ` A ¢ B  àêñèîìà
                   ¡¢                          ¡
        Σ2   : A B, A ` B  ïî ïðàâèëó (− ¢)
                    ¡¢
        Σ3   : A B, A ` ¬ A ∨ B  ïî ïðàâèëó (+ ∨)
                     ¡
        Σ4   : A ¢ B, ¬(¬ A ∨ B) ` ¬ A  ïî äîêàçàííîìó ïðàâèëó Ctrp
              èç ïðåäûäóùåãî
                     ¡
        Σ5   : A ¢ B, ¬(¬ A ∨ B) ` ¬ A ∨ B  ïî ïðàâèëó (+ ∨)
        Σ6   : ¬(¬ A ∨ B) ` ¬(¬ A ∨ B)  àêñèîìà
                     ¡
        Σ7   : A ¢ B, ¬(¬ A ∨ B) `  èç Σ5 è Σ6 ïî ïðàâèëó RA
                     ¡
        Σ8   : A ¢ B ` ¬ A ∨ B  ïî (−¬)
                       ¡   ¡                 ¡
        Σ9   : ` (A ¢ B) ¢ ¬ A ∨ B  ïî (+ ¢)

Страницы