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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
A ' B ` A ≡ B
N
A ' A
1
B ' B
1
¬ A ' ¬ A
1
(A ◦ B) ' (A
1
◦ B
1
) ◦
¡
¢
N ∨
N ¬ A ` ¬ A
1
A
¡
¢
B ` A
1
¡
¢
B
1
A N B ` A
1
N B
1
A ∨ B ` A
1
∨ B
1
¬ A ` ¬ A
1
A
1
` A
¬ A ` ¬ A
1
A
¡
¢
B ` A
1
¡
¢
B
1
A
1
` A A
¡
¢
B ` A
¡
¢
B
A
¡
¢
B, A
1
` B
(−
¡
¢
)
B ` B
1
` B
¡
¢
B
1
(+
¡
¢
)
A
¡
¢
B, A
1
` B
1
A
¡
¢
B ` A
1
¡
¢
B
1
(+
¡
¢
)
(−
¡
¢
)
A N B ` A
1
N B
1
A N B ` A N B
A N B ` A
(− N)
A ` A
1
` A
¡
¢
A
1
(+
¡
¢
)
A N B ` A
1
(−
¡
¢
)
A N B ` A N B
A N B ` A
(− N)
B ` B
1
` B
¡
¢
B
1
(+
¡
¢
)
A N B ` B
1
(−
¡
¢
)
+ N
A ∨ B ` A
1
∨ B
1
A ∨ B ` A ∨ B
A ` A
1
A ` A
1
∨ B
1
(+∨)
B ` B
1
B ` A
1
∨ B
1
(+∨)
A ∨ B ` A
1
∨ B
1
(−∨)
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                                             105


Ñëåäñòâèå. A ' B , åñëè òîëüêî åñëè ñåêâåíöèÿ ` A ≡ B äîêàçóåìà.
   Ïîêàæåì, ÷òî äåäóêòèâíàÿ ýêâèâàëåíòíîñòü ñîõðàíÿåòñÿ ïîä âîç-
äåéñòâèåì ëîãè÷åñêèõ ñâÿçîê ÿçûêà ÈÑ N .
Ëåììà 3.4. Åñëè A ' A1 è B ' B1 òî ¬ A ' ¬ A1 è
                                                      ¡¢
(A ◦ B) ' (A1 ◦ B1 ), ãäå ◦  îäèí èç ñèìâîëîâ          , N, ∨.
Äîêàçàòåëüñòâî.  ñèëó ñèììåòðè÷íîñòè äîñòàòî÷íî äîêàçàòü â
                                                         ¡                ¡
ÈÑ N âûâîäèìîñòü ñåêâåíöèé ¬ A              `   ¬ A1 , A ¢ B      `    A1 ¢ B1 ,
A N B ` A1 N B1 , A ∨ B ` A1 ∨ B1 .
¬ A ` ¬ A1
                 A1 ` A
                             (êîíòðàïîçèöèÿ, ñì. ëåììó 3.2)
               ¬ A ` ¬ A1
  ¡        ¡
A ¢ B ` A1 ¢ B1
               ¡        ¡
   A1 ` A    A ¢B ` A ¢B               ¡        B `     B1        ¡
          ¡¢                        (− ¢)              ¡¢      (+ ¢)
        A B, A1 ` B                            ` B        B1                    ¡
                    ¡                                                        (− ¢)
                 A ¢ B, A1 `         B1        ¡
                   ¡                ¡¢      (+ ¢)
                A ¢ B ` A1             B1

A N B ` A1 N B1
    Èìååì
          ANB ` ANB                    A ` A1             ¡
                            (− N)          ¡           (+ ¢)
           ANB ` A                   ` A ¢ A1                        ¡
                                                                  (− ¢)
                            A N B ` A1
     Àíàëîãè÷íî
          ANB ` ANB                   B ` B1              ¡
                            (− N)         ¡            (+ ¢)
           ANB ` A                   ` B ¢ B1                        ¡
                                                                  (− ¢)
                            A N B ` B1
     Ïðèìåíÿÿ ïðàâèëî (+ N) ê çàêëþ÷èòåëüíûì ñåêâåíöèÿì äàííûõ
     âûâîäîâ, ïîëó÷àåì òðåáóåìîå.
A ∨ B ` A1 ∨ B1
                     A ` A1                        B ` B1
A∨B ` A∨B                      (+∨)                                   (+∨)
                   A ` A1 ∨ B1                   B ` A1 ∨ B 1
                                                                              (−∨)
                      A ∨ B ` A1 ∨ B1

Страницы