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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

S
Rl(S)
(N →) (→ ∨)
Rl(S)
N Γ = ∨∆ =
N Γ = ∨∆ =
(
¡
¢
→)
Γ → ∆, A B, Γ → ∆
A
¡
¢
B, Γ → ∆
|A| = |B| = |A
¡
¢
B| =
(→ ¬)
A, Γ → ∆
Γ → ∆, ¬ A
|A| = |¬ A| = ¤
S
S
S
S
¤
S
A, A, Γ → ∆
A, Γ → ∆
(− →)
Γ → ∆, A, A
Γ → ∆, A
(→ −) .
2. Èñ÷èñëåíèå S ñåêâåíöèàëüíîãî òèïà                            121


Ëåììà 3.11. Äëÿ êàæäîãî ïðàâèëà èç Rl(S) ñåêâåíöèÿ-çàêëþ÷åíèå
òîæäåñòâåííî èñòèííà, åñëè è òîëüêî åñëè òîæäåñòâåííî èñòèííû
âñå ñåêâåíöèè-ïîñûëêè.
Äîêàçàòåëüñòâî. Îòìåòèì ñíà÷àëà, ÷òî äëÿ ïðàâèë (N →) è (→ ∨)
èñòèííîñòè ñåêâåíöèé-ïîñûëîê è ñåêâåíöèé-çàêëþ÷åíèé ñîâïàäàþò.
Ðàññìàòðèâàÿ äàëåå îñòàëüíûå ïðàâèëà èç Rl(S) çàêëþ÷àåì, ÷òî ïðè
N Γ = 0 èëè ∨∆ = 1 îäíîâðåìåííî èñòèííû âñå ñåêâåíöèè-ïîñûëêè è
ñåêâåíöèè-çàêëþ÷åíèÿ âñåõ ïðàâèë.
     ïðîòèâíîì ñëó÷àå, ïðè N Γ = 1 è ∨∆ = 0, äëÿ ëþáîãî
ïðàâèëà èñòèííîñòü âñåõ ñåêâåíöèé-ïîñûëîê è èñòèííîñòü ñåêâåíöèè-
çàêëþ÷åíèÿ ñóòü ýêâèâàëåíòíûå óñëîâèÿ. Íàïðèìåð, äëÿ ïðàâèëà
  ¡
( ¢ →)
                     Γ → ∆, A      B, Γ → ∆
                             ¡¢
                          A B, Γ → ∆
                                                 ¡
ýòèìè óñëîâèÿìè ÿâëÿþòñÿ |A| = 1, |B| = 0 è |A ¢ B| = 0 ñîîòâåò-
ñòâåííî. Äëÿ ïðàâèëà
                                   A, Γ → ∆
                       (→ ¬)
                                  Γ → ∆, ¬ A

ýòè óñëîâèÿ ñóòü |A| = 0 è |¬ A| = 1 è ò.ä.                      ¤


Òåîðåìà 3.9. ÈÑ S êîððåêòíî è ñåìàíòè÷åñêè ïîëíî.
Äîêàçàòåëüñòâî. Ïîñêîëüêó àêñèîìû ÈÑ S òîæäåñòâåííî èñòèííû,
ïî ëåììå 3.11 âñå äîêàçóåìûå ñåêâåíöèè òàêæå áóäóò òîæäåñòâåííî
èñòèííûìè. Òàêèì îáðàçîì, ÈÑ S êîððåêòíî.
   Ïîêàæåì ïîëíîòó ÈÑ S . Âîçüì¼ì âñþäó èñòèííóþ ñåêâåíöèþ, ðàñ-
ñìîòðèì å¼ êàê êîðåíü è, ïðèìåíÿÿ îáðàòíûå ïðàâèëà âûâîäà, ïîñòðî-
èì äåðåâî, êàê óêàçàíî âûøå. Ïðîöåññ ïðîäîëæèì âïëîòü äî ïîëó÷å-
íèÿ ñåêâåíöèé-ëèñòüåâ, àíòåöåäåíò è ñóêöåäåíò êîòîðûõ ñóòü íàáîðû
ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ. Ïî ëåììå 3.11 âñå ñåêâåíöèè â ïî-
ëó÷åííîì äåðåâå âñþäó èñòèííû. Îòíîñèòåëüíî ñåêâåíöèé-ëèñòüåâ ýòî
îçíà÷àåò, ÷òî îíè ñóòü àêñèîìû, ò.ê. òîëüêî àêñèîìû ÿâëÿþòñÿ âñþ-
äó èñòèííûìè ñåêâåíöèÿìè óêàçàííîãî âèäà. Òàêèì îáðàçîì, ïîëó÷åí
âûâîä èñõîäíîé ñåêâåíöèè.                                       ¤


Ëåììà 3.12. Â S äîïóñòèìû ïðàâèëà ñîêðàùåíèÿ:
       A, A, Γ → ∆                      Γ → ∆, A, A
                      (− →)      è                    (→ −) .
        A, Γ → ∆                         Γ → ∆, A

Страницы