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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

` A ∨ ¬ A
¬ A ` ¬ A
¬ A ` A ∨ ¬ A
(+ ∨) ¬ (A ∨ ¬ A) ` ¬ (A ∨ ¬ A)
¬ (A ∨ ¬ A), ¬ A `
¬ (A ∨ ¬ A) ` A
(−¬)
(RA) .
¬ (A ∨ ¬ A) ` A
¬ (A ∨ ¬ A) ` A ∨ ¬ A
(+ ∨) ¬ (A ∨ ¬ A) ` ¬ (A ∨ ¬ A)
¬ (A ∨ ¬ A) `
` A ∨ ¬ A
(−¬)
(RA) .
Σ N
Σ N
Σ
1
, . . . , Σ
l−1
, Σ
l
= Σ Σ
N
Σ T = Σ
T
T
1
, . . . , T
l−1
Σ
1
, . . . , Σ
l−1
Σ
i
1
. . . Σ
i
k
Σ
, i
1
, . . . , i
k
< l
T
i
1
. . . T
i
k
Σ
Σ
Σ
h T
T
Σ
1
, . . . , Σ
m
h + 1
98                   Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


       3) ` A ∨ ¬ A
      Ìû ðàçîáü¼ì äåðåâî âûâîäà íà äâå ÷àñòè èç-çà ïîëèãðàôè÷åñêèõ
      òðóäíîñòåé. Èìååì:
         ¬A ` ¬A
                     (+ ∨)     ¬ (A ∨ ¬ A) ` ¬ (A ∨ ¬ A)
        ¬A ` A ∨ ¬A                                            (RA) .
                  ¬ (A ∨ ¬ A), ¬ A `
                                       (−¬)
                   ¬ (A ∨ ¬ A) ` A
      Äàëåå:
          ¬ (A ∨ ¬ A) ` A
                              (+ ∨)    ¬ (A ∨ ¬ A) ` ¬ (A ∨ ¬ A)
       ¬ (A ∨ ¬ A) ` A ∨ ¬ A
                                                                   (RA) .
                          ¬ (A ∨ ¬ A) `
                                        (−¬)
                           ` A ∨ ¬A

     Ñïðàâåäëèâà ñëåäóþùàÿ ìåòàòåîðåìà.
Òåîðåìà 3.1. Ñåêâåíöèÿ Σ èìååò äîêàçàòåëüñòâî â ÈÑ N â âèäå
äåðåâà, åñëè è òîëüêî åñëè Σ  òåîðåìà N .
Äîêàçàòåëüñòâî. Íåîáõîäèìîñòü. Ïóñòü êîíå÷íàÿ ïîñëåäîâàòåëü-
íîñòü Σ1 , . . . , Σl−1 , Σl = Σ  ëèíåéíîå äîêàçàòåëüñòâî ñåêâåíöèè Σ
â N . Äîêàçàòåëüñòâî íåîáõîäèìîñòè óòâåðæäåíèÿ òåîðåìû ïðîâåä¼ì
èíäóêöèåé ïî äëèíå âûâîäà.
    Åñëè Σ  àêñèîìà, òî T = Σ áóäåò å¼ äîêàçàòåëüñòâîì â âèäå
äåðåâà T .
    Èíà÷å, ïóñòü           T1 , . . . , Tl−1  äîêàçàòåëüñòâà ñåêâåíöèé
Σ1 , . . . , Σl−1 â âèäå äåðåâà. Åñëè
                  Σi1 . . . Σik
                                , i1 , . . . , ik < l
                       Σ
 ïðèìåíåíèå íåêîòîðîãî ïðàâèëà, òî äåðåâî
                                Ti1 . . . Tik
                                     Σ
áóäåò äîêàçàòåëüñòâîì ñåêâåíöèè Σ â âèäå äåðåâà.
   Äîñòàòî÷íîñòü. Ïóñòü òåïåðü äàíî äîêàçàòåëüñòâî ñåêâåíöèè Σ
â âèäå äåðåâà. Äîêàçàòåëüñòâî äîñòàòî÷íîñòè ïðîâåä¼ì èíäóêöèåé ïî
âûñîòå h âõîæäåíèÿ ñåêâåíöèè â äåðåâå T .
   Íà÷àëüíûå ñåêâåíöèè â äåðåâå T áóäóò ëèíåéíûìè äîêàçà-
òåëüñòâàìè. Åñëè äëÿ âñåõ ñåêâåíöèé Σ1 , . . . , Σm âûñîòû h + 1

Страницы