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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

A N
N
A N N
A
Σ N
N Σ
N
A
1
, . . . , A
k
` B A
1
, . . . , A
k
`
A
1
¡
¢
(A
2
¡
¢
. . .
¡
¢
(A
k
¡
¢
B) . . .)
A
1
¡
¢
(A
2
¡
¢
. . .
¡
¢
(A
k
¡
¢
A
0
N ¬ A
0
) . . .) A
0
N
A
A
0
= D
1
N . . . N D
m
D
i
, i = 1, m
B
0
∨¬ B
0
∨C
0
B
0
∨¬ B
0
B
0
C
0
N
` B
0
∨¬ B
0
+∨ ` B
0
∨ ¬ B
0
∨ C
0
` D
i
, i = 1, m + N
` A
0
A ¤
N
N H
A
1
, . . . , A
m
`
N
B ⇔ A
1
, . . . , A
m
`
H
B
A
1
, . . . , A
m
`
N
⇔ A
1
, . . . , A
m
`
H
B
0
N ¬ B
0
B
0
108                  Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


Ëåììà 3.6. Ëþáàÿ òîæäåñòâåííî èñòèííàÿ ôîðìóëà A ÈÑ N ìî-
æåò áûòü ïðåäñòàâëåíà â âèäå äåäóêòèâíî ýêâèâàëåíòíîé åé ÊÍÔ,
â êîòîðîé êàæäàÿ äèçúþíêöèÿ ñîäåðæèò íåêîòîðóþ ïðîïîçèöèîíàëü-
íóþ ïåðåìåííóþ âìåñòå ñ å¼ îòðèöàíèåì.
   Òåïåðü, ðàññìàòðèâàÿ äëÿ ïðîñòîòû ãëàâíóþ èíòåðïðåòàöèþ, ìû
ñìîæåì äîêàçàòü òåîðåìó î ñåìàíòè÷åñêîé ïîëíîòå èñ÷èñëåíèÿ ñåêâåí-
öèé N .

Òåîðåìà 3.6 (Î ïîëíîòå ÈÑ N ).
à) Äëÿ òîãî, ÷òîáû ôîðìóëà A ÈÑ N áûëà äîêàçóåìà â N íåîáõî-
     äèìî è äîñòàòî÷íî, ÷òîáû A áûëà òîæäåñòâåííî èñòèííîé.
á) Äëÿ òîãî, ÷òîáû ñåêâåíöèÿ Σ èñ÷èñëåíèÿ N áûëà äîêàçóåìà â
     N íåîáõîäèìî è äîñòàòî÷íî, ÷òîáû Σ áûëà òîæäåñòâåííî èñ-
     òèííîé.
Äîêàçàòåëüñòâî. Íåîáõîäèìîñòü óòâåðæäåíèé ñëåäóåò èç òåîðåìû 3.5
î êîððåêòíîñòè N .
   Â ñèëó ëåììû 3.2 è îïðåäåëåíèÿ òîæäåñòâåííîé èñòèííîñòè ñå-
êâåíöèé è ôîðìóë, äîêàçóåìîñòü è òîæäåñòâåííàÿ èñòèííîñòü ñåêâåí-
öèé A1 , . . . , Ak ` B è A1 , . . . , Ak ` ðàâíîñèëüíû äîêàçóåìîñòè
                                            ¡    ¡    ¡    ¡
è òîæäåñòâåííîé èñòèííîñòè ôîðìóë A1 ¢(A2 ¢ . . . ¢(Ak ¢ B) . . .) è
     ¡¢     ¡¢     ¡¢  ¡¢ 0     0                          0
A1 (A2 . . . (Ak A N ¬ A ) . . .) ñîîòâåòñòâåííî, ãäå A  íåêî-
òîðàÿ êîíêðåòíàÿ ôîðìóëà. Ïîýòîìó óòâåðæäåíèå á) ñëåäóåò èç à).
   Ïîêàæåì âûâîäèìîñòü â ÈÑ N ëþáîé òîæäåñòâåííî èñòèííîé ôîð-
ìóëû. Ïóñòü A  òîæäåñòâåííî èñòèííàÿ (â ãëàâíîé èíòåðïðåòàöèè)
ôîðìóëà. Òîãäà ïî ëåììå 3.6 ñóùåñòâóåò äåäóêòèâíî ýêâèâàëåíòíàÿ åé
ÊÍÔ A 0 = D1 N . . . N Dm , â êîòîðîé äèçúþíêòû Di , i = 1, m èìåþò
âèä B0 ∨ ¬ B0 ∨ C 0 èëè B0 ∨¬ B0 è ãäå B0 è C 0  íåêîòîðûå êîíêðåò-
íûå ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ è ôîðìóëà ÈÑ N ñîîòâåòñòâåííî.
   Â ïðèìåðå 3.3 ïîêàçàíà âûâîäèìîñòü ñåêâåíöèè ` B0 ∨¬ B0 . Ïî ïðà-
âèëó (+∨) äîêàçóåìà è ñåêâåíöèÿ ` B0 ∨ ¬ B0 ∨ C 0 . Òàêèì îáðàçîì,
âñå ñåêâåíöèè ` Di , i = 1, m âûâîäèìû. Íî òîãäà ïî ïðàâèëó (+ N)
âûâîäèìà è ñåêâåíöèÿ ` A 0 è, ñëåäîâàòåëüíî, ôîðìóëà A.            ¤


Ñëåäñòâèå 1. Èñ÷èñëåíèå N ðàçðåøèìî.
Ñëåäñòâèå 2 (Òåîðåìà î ðàâíîñèëüíîñòè ÈÑ N è ÈÂ H ).
  1. A1 , . . . , Am `N B ⇔ A1 , . . . , Am `H B ;
  2. A1 , . . . , Am `N ⇔ A1 , . . . , Am `H B 0 N ¬ B 0 , ãäå B 0  íåêî-
     òîðàÿ êîíêðåòíàÿ ôîðìóëà.

Страницы