ВУЗ:
Составители:
Рубрика:
` A ∨ ¬A (−∨)
¬A ∨ B ` A
¡
¢
B
A ` A ¬A ` ¬A
A, ¬A `
(RA)
A, ¬A ` B
(DS) B ` B ¬A ∨ B ` ¬A ∨ B
¬A ∨ B, A ` B
¬A ∨ B ` A
¡
¢
B
(+
¡
¢
)
−∨
A N B ' B N A
A N B ` A N B
A N B ` B
(− N)
A N B ` A N B
A N B ` A
(− N)
A N B ` B N A
(+ N)
B N A ` A N B
¤
Γ ` A ≡ B
Γ, A ` B Γ, B ` A
` A ≡ B
A ` A
Γ ` (A
¡
¢
B) N (B
¡
¢
A)
Γ ` A
¡
¢
B
(− N)
Γ, A ` B
(−
¡
¢
)
Γ, A ` B Γ, B ` A
Γ, A ` B Γ, B ` A
Γ, A ` B
Γ ` A
¡
¢
B
(+
¡
¢
)
Γ, B ` A
Γ ` B
¡
¢
A
(+
¡
¢
)
Γ ` (A
¡
¢
B) N (B
¡
¢
A)
(+ N)
Γ ` A ≡ B ¤
104 Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé Òåïåðü, ïðèìåíÿÿ ê ýòèì è äîêàçàííîé â ïðèìåðå 3.3 ñåêâåíöèè ` A ∨ ¬A ïðàâèëî (−∨), ïîëó÷àåì òðåáóåìîå. ¡ Ïîêàæåì òåïåðü âûâîäèìîñòü ñåêâåíöèè ¬A ∨ B ` A ¢ B : A ` A ¬A ` ¬A (RA) A, ¬A ` (DS) B ` B ¬A ∨ B ` ¬A ∨ B A, ¬A ` B ¬A ∨ B, A ` B ¡ ¡ (+ ¢) ¬A ∨ B ` A ¢ B (ïðåäïîñëåäíèé ïåðåõîä îñóùåñòâë¼í ïî ïðàâèëó ( −∨) ). 3. A N B ' B N A ANB ` ANB ANB ` ANB (− N) (− N) ANB ` B ANB ` A (+ N) ANB ` BNA è àíàëîãè÷íî ïîêàçûâàåòñÿ B N A ` A N B . ¾Îñòàëüíûå ýêâèâàëåíòíîñòè ÷èòàòåëü ëåãêî äîêàæåò ñàì, èñïîëüçóÿ íàâûê, ïðèîáðåò¼ííûé ïðè ðàçáîðå ðàíåå ïðèâåä¼ííûõ äîêàçàòåëüñòâ¿ ([6], ñ. 38). ¤ Òåîðåìà 3.3. Ñåêâåíöèÿ Γ ` A ≡ B äîêàçóåìà, åñëè òîëüêî åñëè äîêàçóåìû ñåêâåíöèè Γ, A ` B è Γ, B ` A. Äîêàçàòåëüñòâî. Äîñòàòî÷íîñòü. Ïóñòü ñåêâåíöèÿ ` A ≡ B äîêà- çóåìà. Òîãäà ¡ ¡ Γ ` (A ¢ B) N (B ¢ A) A ` A ¡ (− N) Γ ` A ¢B ¡ (− ¢) Γ, A ` B åñòü äîêàçàòåëüñòâî ñåêâåíöèè Γ, A ` B . Äîêàçóåìîñòü Γ, B ` A óñòàíàâëèâàåòñÿ àíàëîãè÷íî. Íåîáõîäèìîñòü. Ïóñòü ñåêâåíöèè Γ, A ` B è Γ, B ` A äîêàçóåìû. Òîãäà Γ, A ` B ¡ Γ, B ` A ¡ ¡ (+ ¢) ¡ (+ ¢) Γ ` A ¢B Γ ` B ¢A (+ N) ¡¢ ¡¢ Γ ` (A B) N (B A) åñòü äîêàçàòåëüñòâî ñåêâåíöèè Γ ` A ≡ B . ¤
Страницы
- « первая
- ‹ предыдущая
- …
- 102
- 103
- 104
- 105
- 106
- …
- следующая ›
- последняя »