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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

H
Γ ` A
¡
¢
B
Γ, A ` B
Γ
A B H
Γ, A ` B
Γ ` A
¡
¢
B
. (DT )
Γ, A ` B
B
1
, . . . , B
l
= B k = 1, . . . , l
B
k
H,
Γ,
A,
B
1
, . . . , B
k−1
(k > 3).
l B
Γ ` A
¡
¢
B
B Γ, A
B
¡
¢
(A
¡
¢
B) A1
A
¡
¢
B
A
¡
¢
B Γ
` A
¡
¢
A
Γ ` A
¡
¢
A
l > 3
B B
i
B
j
= B
i
¡
¢
B i, j ∈ { 1, . . . , l − 1 }
Γ ` A
¡
¢
(B
i
¡
¢
B)
(A
¡
¢
(B
i
¡
¢
B))
¡
¢
((A
¡
¢
B
i
)
¡
¢
(A
¡
¢
B)) A2
Γ ` (A
¡
¢
B
i
)
¡
¢
(A
¡
¢
B)
Γ ` A
¡
¢
B
i
2. Èñ÷èñëåíèå âûñêàçûâàíèé H                                           59

                                     ¡
óñòàíîâëåíèÿ âûâîäèìîñòè Γ ` A ¢ B äîêàçûâàþò ñïðàâåäëèâîñòü
Γ, A ` B , èç ÷åãî ñëåäóåò ñïðàâåäëèâîñòü èñõîäíîé âûâîäèìîñòè. Âû-
èãðûø çäåñü çàêëþ÷àåòñÿ â òîì, ÷òî îáû÷íî ýòó ïîñëåäíþþ âûâîäè-
ìîñòü äîêàçàòü çíà÷èòåëüíî ëåã÷å, ÷åì èñõîäíóþ (èñïîëüçóåìûõ ãèïî-
òåç áîëüøå è äîêàçûâàåìàÿ ôîðìóëà ïðîùå).
Òåîðåìà 2.3 (Î äåäóêöèè). Ïóñòü Γ  íàáîð ôîðìóë (âîçìîæíî
ïóñòîé), à A è B  ôîðìóëû H . Òîãäà
                               Γ, A ` B
                                      ¡ .                           (DT )
                              Γ ` A ¢B
Äîêàçàòåëüñòâî. Γ, A            ` B îçíà÷àåò, ÷òî ñóùåñòâóåò âûâîä
B1 , . . . , Bl = B , ò.å. äëÿ ëþáîãî k = 1, . . . , l ñïðàâåäëèâî îäíî èç
ñëåäóþùèõ óòâåðæäåíèé:
                
                  (a) àêñèîìà H,
                
                
                
                 (b) ýëåìåíò Γ,
  Bk åñòü          (c) ôîðìóëà A,
                
                
                
                  (d) ðåçóëüòàò ïðèìåíåíèÿ ïðàâèëà MP ê íåêîòîðîé
                
                         ïàðå ôîðìóë èç ñïèñêà B1 , . . . , Bk−1 (k > 3).

Äîêàæåì òåîðåìó èíäóêöèåé ïî äëèíå l âûâîäà ôîðìóëû B .
   Ïóñòü èìåþò ìåñòî êàêîé-ëèáî èç ïåðâûõ òð¼õ âûøåóêàçàííûõ ñëó-
                                                   ¡
÷àåâ. Ðàçáåð¼ì èõ è ïîêàæåì ñïðàâåäëèâîñòü Γ ` A ¢ B .
(a) è (b). Äîáàâèâ ê âûâîäó B èç Γ, A ôîðìóëû
             ¡   ¡
    (l+1) B ¢ (A ¢ B)   ñõåìà àêñèîì A1
            ¡¢
    (l+2) A B      ïî MP èç ïðåäûäóùåãî
                       ¡
      ïîëó÷àåì âûâîä A ¢ B èç Γ.
                           ¡
(ñ). Ñïðàâåäëèâîñòü ` A ¢ A óæå äîêàçàíà ëåììîé 2.1. Îòñþäà
             ¡¢
      Γ ` A A ïî ñâîéñòâó ìîíîòîííîñòè âûâîäèìîñòè.
 Ýòè ñëó÷àè îáåñïå÷èâàþò áàçèñ èíäóêöèè.
    Èíà÷å (øàã èíäóêöèè), ïóñòü èìååò ìåñòî ñëó÷àé (d). Òîãäà l > 3 è
                                              ¡
 âûâîä B ñîäåðæèò ôîðìóëû Bi è Bj = Bi ¢ B , i, j ∈ { 1, . . . , l − 1 }.
 Òîãäà:
              ¡      ¡
(l+1) Γ ` A ¢ (Bi ¢ B)         ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ
          ¡¢      ¡¢      ¡    ¡     ¡   ¡
(l+2) (A (Bi B)) ¢ ((A ¢ Bi ) ¢(A ¢ B))  ñõåìà A2
               ¡¢     ¡¢    ¡¢
(l+3) Γ ` (A Bi )        (A B)  ïî MP èç (1) è (2)
              ¡
(l+4) Γ ` A ¢ Bi        ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ

Страницы