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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
L
1
, . . . , L
m
L
1
, . . . , L
m
, Σ Σ
h ¤
N
N
Γ ` A
¡
¢
B
Γ, A ` B
Γ ` A N ¬ A
Γ `
Γ `
Γ ` A
Γ, A `
Γ ` ¬ A
+ ¬
Γ, A ` B
Γ, ¬ B ` ¬ A
Γ ` A
¡
¢
B
Γ, A ` B
Σ : Γ ` A
¡
¢
B
Σ : Γ, A ` A
¡
¢
B + `
Σ : A ` A
Σ : Γ, A ` B −
¡
¢
Γ ` A N ¬ A
Γ `
Γ ` A N ¬ A
Γ ` A
(− N)
Γ ` A N ¬ A
Γ ` ¬ A
(− N)
Γ `
(RA)
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                                    99


ïîñòðîåíû ëèíåéíûå äîêàçàòåëüñòâà, L1 , . . . , Lm , òî ïîñëåäîâàòåëü-
íîñòü L1 , . . . , Lm , Σ áóäåò ëèíåéíûì äîêàçàòåëüñòâîì ñåêâåíöèè Σ
âûñîòû h.                                                           ¤


  Ïîêàæåì äîïóñòèìîñòü â ÈÂ N íåêîòîðûõ âàæíûõ ïðàâèë, êîòî-
ðûìè áóäåì ïîëüçîâàòüñÿ â äàëüíåéøåì.

Ëåììà 3.2. Ñëåäóþùèå ïðàâèëà ÿâëÿþòñÿ äîïóñòèìûìè â ÈÑ N :
               ¡
       Γ ` A ¢B
  1.                     RDT;
        Γ, A ` B
       Γ ` AN¬A
  2.                        çàêîí ïðîòèâîðå÷èÿ;
          Γ `
        Γ `
  3.                   ïðàâèëî DS;
       Γ ` A
       Γ, A `
  4.                    (+ ¬);
       Γ ` ¬A
         Γ, A ` B
  5.                         êîíòðàïîçèöèÿ Ctrp.
       Γ, ¬ B ` ¬ A

Äîêàçàòåëüñòâî.
                ¡
        Γ ` A ¢B
  1.
         Γ, A ` B
       Äàäèì ëèíåéíîå äîêàçàòåëüñòâî àíàëîãó ïðàâèëà RDT.
                        ¡
        Σ1   :   Γ ` A ¢ B  ïðåäïîëîæåíèå
                          ¡
        Σ2   :   Γ, A ` A ¢ B  ïî ïðàâèëó (+ `)
        Σ3   :   A ` A  àêñèîìà
                                           ¡
        Σ4   :   Γ, A ` B  ïî ïðàâèëó (− ¢)

       Γ ` AN¬A
  2.
          Γ `
       Äëÿ ýòîãî è ñëåäóþùèõ ïðàâèë äàäèì ëèíåéíîå äîêàçàòåëüñòâî.

                 Γ ` AN¬A                  Γ ` AN¬A
                             (− N)                    (− N)
                   Γ ` A                     Γ ` ¬A           (RA)
                                     Γ `

Страницы