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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
h T
h(Σ) = 0 Σ T
Σ
1
. . . Σ
m
Σ
T
h(Σ
1
) = . . . = h(Σ
m
) = h(Σ) + 1 .
h(Σ) Σ
T h(Σ)
T
P
P
Σ
1
, . . . , Σ
m
h+1
P
Σ
1
. . . Σ
m
Σ
Rl(N) Σ
1
. . . Σ
m
P Σ h
A, B ` A N B
A ` A B ` B
A, B ` A N B
(+ N)
¬¬ A ` A
¬ A ` ¬ A
¬ ¬ A, ¬ A ` ¬ A
¬ ¬ A ` ¬ ¬ A
¬ ¬ A, ¬ A ` ¬ ¬ A
¬ ¬ A, ¬ A `
¬ ¬ A ` A
(−¬)
(RA) .
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                                   97


   Îïðåäåëèì ïîíÿòèå âûñîòû âõîæäåíèÿ ñåêâåíöèè â äåðåâå. Ïóñòü
h  ôóíêöèÿ, îïðåäåë¼ííàÿ íà âõîæäåíèÿõ ñåêâåíöèé äåðåâà T , ïðè-
íèìàþùàÿ íàòóðàëüíûå çíà÷åíèÿ è îáëàäàþùàÿ ñëåäóþùèìè ñâîé-
ñòâàìè:
     1) h(Σ) = 0, åñëè Σ  çàêëþ÷èòåëüíàÿ ñåêâåíöèÿ â äåðåâå T .
             Σ1 . . . Σm
     2) Åñëè              ïåðåõîä â äåðåâå T , òî
                  Σ
                    h(Σ1 ) = . . . = h(Σm ) = h(Σ) + 1 .

   ×èñëî h(Σ) íàçûâàåòñÿ âûñîòîé âõîæäåíèÿ ñåêâåíöèè Σ â äåðå-
âå T . Î÷åâèäíî, h(Σ) îïðåäåëåíî îäíîçíà÷íî. Ìàêñèìàëüíóþ âûñîòó
ñåêâåíöèé, âõîäÿùèõ â T , íàçîâ¼ì âûñîòîé äåðåâà .
   Àíàëîãè÷íî ïðèíöèïó èíäóêöèè ïî äëèíå âûâîäà â ìîæíî ñôîðìó-
ëèðîâàòü ïðèíöèï èíäóêöèè ïî âûñîòå âõîæäåíèÿ ñåêâåíöèè â äåðåâî
âûâîäà. Ïóñòü òðåáóåòñÿ äîêàçàòü, ÷òî âñå äîêàçóåìûå ñåêâåíöèè îá-
ëàäàþò äàííûì ñâîéñòâîì P . Äëÿ ýòîãî äîñòàòî÷íî óñòàíîâèòü, ÷òî
 1) êàæäàÿ íà÷àëüíàÿ ñåêâåíöèÿ (àêñèîìà) îáëàäàåò ñâîéñòâîì P ;
 2) åñëè âñå ñåêâåíöèè Σ1 , . . . , Σm âûñîòû h + 1 îáëàäàåò ñâîéñòâîì
    P è äëÿ êàæäîãî ïðàâèëà âûâîäà
                                Σ1 . . . Σm
                                     Σ
     èç Rl(N ) âñå ñåêâåíöèè-ïîñûëêè Σ1 . . . Σm îáëàäàþò ñâîéñòâîì
     P , òî èì îáëàäàåò è ñåêâåíöèÿ Σ âûñîòû h.
Ïðèìåð 3.3. Ïðîäåìîíñòðèðóåì ïîñòðîåíèå äîêàçàòåëüñòâ â âèäå äå-
ðåâà (ïðèìåíÿåìîå ïðàâèëî óêàçûâàåòñÿ â ñêîáêàõ ó ïåðåõîäîâ).
     1)   A, B ` A N B
                         A ` A    B ` B
                                              (+ N)
                          A, B ` A N B


     2) ¬¬ A ` A
     Èìååì:
                ¬A ` ¬A             ¬¬A ` ¬¬A
             ¬ ¬ A, ¬ A ` ¬ A     ¬ ¬ A, ¬ A ` ¬ ¬ A
                                                           (RA) .
                      ¬ ¬ A, ¬ A `
                                       (−¬)
                       ¬¬A ` A

Страницы