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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

(
¡
¢
→)
0
C, A
¡
¢
B, Γ → ∆
1
C, Γ → ∆
1
, A
C, B, Γ → ∆
1
(→ ¬)
C
r A
¡
¢
B
(
¡
¢
→)
¤
S
Σ
Rl(S)
A, Γ → ∆, A
¬(A N B)
¡
¢
¬ A ∨ ¬ B
→ ¬(A N B)
¡
¢
¬ A ∨ ¬ B
¬(A N B) → ¬ A ∨ ¬ B
(→
¡
¢
)
0
¬(A N B) → ¬ A, ¬ B
→ A N B, ¬ A, ¬ B
(¬ →)
0
(→ ∨)
0
→ A, ¬ A, ¬ B
A → A, ¬ B
(→ ¬)
0
→ B, ¬ A, ¬ B
B → B, ¬ A
(→ ¬)
0
(→ N)
0
(→ ∨)
0
(¬ →)
0
120                  Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé

                                                 ¡
       Ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ, ïðàâèëî ( ¢ →) 0 ïðèìåíè-
                  ¡¢
       ìî ê C, A B, Γ → ∆1 è ïîýòîìó ñåêâåíöèè C, Γ → ∆1 , A è
       C, B, Γ → ∆1 âûâîäèìû. Ïðèìåíèâ ê íèì ïðàâèëî (→ ¬) äëÿ
       ôîðìóëû C , ïîëó÷èì òðåáóåìûå ñåêâåíöèè.
    Äëÿ îñòàëüíûõ ïðàâèë ðàññóæäåíèÿ àíàëîãè÷íû.
                                           ¡
  b) Ïðàâèëî r ïðèìåíÿëîñü ê ôîðìóëå A ¢ B , ò.å. ýòî ïðàâèëî
      ¡¢
    ( →). Íî òîãäà òðåáóåìûå ñåêâåíöèè, ÿâëÿþùèåñÿ åãî ïîñûë-
    êàìè, âûâîäèìû.

      Îñòàëüíûå ïðàâèëà ðàññìàòðèâàþòñÿ àíàëîãè÷íî.                ¤

   Ìîæíî òàêæå óòâåðæäàòü, ÷òî èñïîëüçîâàíèå äàííûõ ïðàâèë íå
óâåëè÷èâàåò âûñîòó äåðåâà âûâîäà è êîëè÷åñòâà ñåêâåíöèé â í¼ì. Çà-
ìåòèì, ÷òî îáðàù¼ííûå ïðàâèëà âûâîäà  àíàëîãè ïðàâèë âûâîäà ñå-
ìàíòè÷åñêèõ òàáëèö (ñì. ï. 3.2 ãëàâû 1). Ïîä÷åðêí¼ì, ÷òî äîïóñòèìûå
ïðàâèëà ÈÑ S ìîãóò áûòü è íåîáðàòèìûìè (íàïðèìåð, ïðàâèëà îñëàá-
ëåíèÿ).
   Îáðàòèìîñòü ïðàâèë ïîçâîëÿåò ëåãêî èñêàòü âûâîä äàííîé ñåêâåí-
öèè Σ: âçÿâ å¼ â êà÷åñòâå èñõîäíîé (åé áóäåò ñîîòâåòñòâîâàòü êîðåíü
äåðåâà âûâîäà), áóäåì ïðèìåíÿòü ïðàâèëà âûâîäà èç Rl(S) â îáðàò-
íîì ïîðÿäêå, ïîêà ýòî âîçìîæíî. Â ñèëó ñâîéñòâà ïîäôîðìóëüíîñòè
îáðàòíûé ïðîöåññ ïîñòðîåíèÿ äåðåâà âûâîäà âñåãäà çàêîí÷èòñÿ. Ê ñå-
êâåíöèÿì âèäà A, Γ → ∆, A ïðàâèëà áîëüøå íå ïðèìåíÿþò è îíè ñòà-
íîâÿòñÿ ëèñòüÿìè äåðåâà. Åñëè âñå ëèñòüÿ îêàæóòñÿ òàêîãî âèäà, òî
äàííàÿ ñåêâåíöèÿ âûâîäèìà.
Ïðèìåð 3.6. Ïîñòðîèì âûâîä îäíîãî èç ïðàâèë Äå Ìîðãàíà  ôîðìóëû
          ¡
¬(A N B) ¢ ¬ A ∨ ¬ B :
                      ¡
          → ¬(A N B) ¢ ¬ A ∨ ¬ B        ¡
                                   (→ ¢) 0
           ¬(A N B) → ¬ A ∨ ¬ B
                                            (→ ∨) 0
            ¬(A N B) → ¬ A, ¬ B        0
                                 (¬ →)
             → A N B, ¬ A, ¬ B
                                                         (→ N) 0
       → A, ¬ A, ¬ B            → B, ¬ A, ¬ B
                     (→ ¬) 0                   (→ ¬) 0
        A → A, ¬ B               B → B, ¬ A

Îáðàùàÿ ïîëó÷åííîå äåðåâî ïîëó÷èì èñêîìûé âûâîä. Çàìåòèì, ÷òî
íà âòîðîì øàãå èñïîëüçîâàíî ïðàâèëî (→ ∨) 0 , õîòÿ âîçìîæåí è âûáîð
ïðàâèëà (¬ →) 0 , ÷òî, îäíàêî, íåñêîëüêî óäëèíèò ïîèñê âûâîäà.
   Èäåÿ ñåêâåíöèàëüíûõ èñ÷èñëåíèé îòêðûâàåò øèðîêèå âîçìîæíîñòè
äëÿ äëÿ îðãàíèçàöèè ñèñòåìàòè÷åñêîãî ïîèñêà äîêàçàòåëüñòâ â ðàçëè÷-
íûõ ëîãè÷åñêèõ ñèñòåìàõ.

Страницы