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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

H
0
H
1
∨ Γ, A ` A ∨ B , Γ, B ` A ∨ B ;
¬
Γ, A ` B Γ, A ` ¬ B
Γ ` ¬ A
;
N Γ, A N B ` A , Γ, A N B ` B
Γ, A ` C Γ, B ` C
Γ, A ∨ B ` C
;
¬¬ Γ, ¬¬ A ` A .
N
A, B ` A N B
t H
1
A B
A ` t
¡
¢
A B ` t
¡
¢
B
(t
¡
¢
A)
¡
¢
((t
¡
¢
B)
¡
¢
(t
¡
¢
A N B)) A
1
5
A, B ` t
¡
¢
(A N B)
A, B, t ` A N B t
∨, N ¬¬
¬
C
A B
C A ∨ B ¤
H
1
¬¬ A ≡ A
Γ, A ` ¬ B
Γ, B ` ¬ A
.
Γ, A ` ¬ B Γ ` A
¡
¢
¬ B
A
1
9 (A
¡
¢
¬ B)
¡
¢
(B
¡
¢
¬ A) Γ ` B
¡
¢
¬ A
¬ A ` ¬ A
A ` ¬¬ A A
¡
¢
¬¬ A
¬¬ A
¡
¢
A A
1
10 N
(¬¬ A
¡
¢
A) N (A
¡
¢
¬¬ A)
4. ÈÂ H 0 è H1                                                  77


  ââåäåíèå ∨ :  Γ, A ` A ∨ B ,      Γ, B ` A ∨ B ;
                Γ, A ` B       Γ, A ` ¬ B
  ââåäåíèå ¬:                             ;
                         Γ ` ¬A
  óäàëåíèå N : Γ, A N B ` A ,       Γ, A N B ` B
                    Γ, A ` C      Γ, B ` C
  ðàçáîð ñëó÷àåâ:                           ;
                         Γ, A ∨ B ` C
  óäàëåíèå ¬¬ : Γ, ¬¬ A ` A .
Äîêàçàòåëüñòâî.
  ââåäåíèå N . Â ñèëó ñâîéñòâà ìîíîòîííîñòè âûâîäèìîñòè äîñòàòî÷-
     íî ïîêàçàòü A, B ` A N B .
     Îáîçíà÷èì ÷åðåç t ïðîèçâîëüíóþ òåîðåìó H1 . Åñëè
     A è B  ãèïîòåçû, òî ïî ïðàâèëó ñàìîäîñòàòî÷íî-
                                     ¡                 ¡
     ñòè ãèïîòåçû èìååì A ` t ¢ A è B ` t ¢ B . Äàëåå,
        ¡¢    ¡¢     ¡¢ ¡¢  ¡¢
     (t A)       ((t B) (t A N B))  àêñèîìà A1 5 ñ ïîäñòà-
     íîâêàìè. Äâàæäû ïðèìåíÿÿ MP, ñ ó÷¼òîì âûøåïðèâåä¼ííûõ
                                       ¡
     âûâîäèìîñòåé èìååì A, B ` t ¢(A N B). Ïî RDT ïîëó÷èì
     A, B, t ` A N B è, óñòðàíÿÿ òåîðåìó t  äîêàçûâàåìóþ
     âûâîäèìîñòü.
  ââåäåíèå/óäàëåíèå ∨, N è óäàëåíèå ¬¬ . Ýòè ïðàâèëà íåïîñðåä-
     ñòâåííî ñëåäóþò èç ñîîòâåòñòâóþùèõ àêñèîìíûõ ñõåì.
  ââåäåíèå ¬ è ðàçáîð ñëó÷àåâ. Äîêàçàòåëüñòâà ýòèõ ïðàâèë îñòàâëÿ-
     åì ÷èòàòåëþ.
Îòìåòèì, ÷òî ðàçáîð ñëó÷àåâ ñîîòâåòñòâóåò ñëåäóþùåé ÷àñòî èñïîëüçó-
åìîé ñõåìå ìàòåìàòè÷åñêîãî ðàññóæäåíèÿ: äîêàçûâàþò, ÷òî C ñëåäóåò
êàê èç A, òàê è èç B , îòêóäà äåëàþò âûâîä, ÷òî ìîæíî óòâåðæäàòü
ñïðàâåäëèâîñòü C , åñëè èìååò ìåñòî A ∨ B .                      ¤

Ïðèìåð 2.6. Äîêàæåì âûâîäèìîñòü â H1 ôîðìóëû ¬¬ A ≡ A (èíâî-
ëþòèâíîñòü îòðèöàíèÿ).
  Ñíà÷àëà ïîêàæåì, ÷òî
                            Γ, A ` ¬ B
                                       .
                            Γ, B ` ¬ A
                                                       ¡
Äåéñòâèòåëüíî, èç Γ, A ` ¬ B ïî DT ïîëó÷àåì Γ ` A ¢ ¬ B . Çàòåì
                     ¡¢      ¡¢    ¡¢                       ¡
èñïîëüçóÿ A1 9  (A ¬ B)        (B ¬ A)  ïî MP èìååì Γ ` B ¢ ¬ A
è ïî RDT ïîëó÷àåì òðåáóåìîå.
   Ïî äîêàçàííîìó èç òðèâèàëüíîé âûâîäèìîñòè ¬ A ` ¬ A ñëåäó-
                                           ¡
åò A ` ¬¬ A, îòêóäà ïî DT ïîëó÷èì A ¢ ¬¬ A. Ïîñëåäíåå ñ ó÷¼-
           ¡¢
òîì ¬¬ A A (àêñèîìà A1 10) ïî ïðàâèëó ïðàâèëó ââåäåíèÿ N äà¼ò
       ¡         ¡
(¬¬ A ¢ A) N (A ¢ ¬¬ A), ÷òî ýêâèâàëåíòíî òðåáóåìîìó.

Страницы