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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

H
` A
` A(x
1
, . . . , x
m
k B
1
, . . . , B
m
)
(Subst)
A x
1
, . . . , x
m
B
1
, . . . , B
m
A
A l
A A
0
A A
0
A
l > 3 A
A
i
A
j
= A
i
¡
¢
A i, j ∈ { 1, . . . , l − 1 }
A
i
0
A
j
0
= A
i
0
¡
¢
A
0
A
0
¤
P
Γ
Γ P
r(A
1
, . . . , A
m
) ∈ Rl
A
1
, . . . , A
m
P
H
` x
¡
¢
x
A H
` A
¡
¢
A
2. Èñ÷èñëåíèå âûñêàçûâàíèé H                                       57


Çàìåòèì, ÷òî âñå ðàññìîòðåííûå âûøå ïðàâèëà âûâîäà, êðîìå ïðàâèëà
òðèâèàëüíîé âûâîäèìîñòè, ÿâëÿþòñÿ íåïðÿìûìè.
   Äîêàæåì äîïóñòèìîñòü åù¼ îäíîãî ïðàâèëà, íå ñâÿçàííîãî ïðÿìî ñ
óêàçàííûìè âûøå îñíîâíûì ñâîéñòâàìè âûâîäèìîñòè.
Òåîðåìà 2.2 (Ïðàâèëî ïîäñòàíîâêè).
                                   ` A
                                                              (Subst)
                  ` A(x1 , . . . , xm k B1 , . . . , Bm )
   Ïðàâèëî ïîçâîëÿåò â òåîðåìå A âìåñòî ïåðåìåííûõ x1 , . . . , xm
ïîäñòàâèòü (îäíîâðåìåííî) ôîðìóëû B1 , . . . , Bm ñîîòâåòñòâåííî.
Äîêàçàòåëüñòâî ïðîâåä¼ì èíäóêöèåé ïî äëèíå âûâîäà ôîðìóëû A.
Îáîçíà÷èì äëèíó âûâîäà ôîðìóëû A ÷åðåç l, à ðåçóëüòàò óêàçàííîé
ïîäñòàíîâêè â ôîðìóëó A  ÷åðåç A 0 .
   Ïóñòü A  àêñèîìà (áàçèñ èíäóêöèè). Òîãäà A 0 âûâîäèìà, ïî-
ñêîëüêó òàêæå ÿâëÿåòñÿ àêñèîìîé, ïîëó÷åííîé íåêîòîðîé ïîäñòàíîâêîé
èç ñõåìû, ñîîòâåòñòâóþùåé àêñèîìå A.
   Èíà÷å (øàã èíäóêöèè) èìååì ñëó÷àé l > 3, è â âûâîäå A èìåþòñÿ
                          ¡
ôîðìóëû Ai è Aj = Ai ¢ A, i, j ∈ { 1, . . . , l − 1 }. Ïî èíäóêòèâíîìó
                                                ¡
ïðåäïîëîæåíèþ ôîðìóëû Ai 0 è Aj 0 = Ai 0 ¢ A 0 âûâîäèìû. Îòñþäà
                                  0
ïî MP ïîëó÷àåì, ÷òî è ôîðìóëà A âûâîäèìà.                            ¤

   Ïðèâåä¼ííîå äîêàçàòåëüñòâî èëëþñòðèðóåò âîçìîæíîñòü ïðèìåíå-
íèÿ óïîìÿíóòîãî âûøå ïðèíöèïà èíäóêöèè ïî äëèíå âûâîäà. Êîíêðåò-
íåå, îí ñîñòîèò â ñëåäóþùåì. Ïóñòü òðåáóåòñÿ äîêàçàòü, ÷òî âñå âûâî-
äèìûå ôîðìóëû îáëàäàþò äàííûì ñâîéñòâîì P . Äëÿ ýòîãî äîñòàòî÷íî
óñòàíîâèòü, ÷òî
 1) êàæäàÿ àêñèîìà (è êàæäàÿ ôîðìóëà èç íàáîðà ãèïîòåç Γ â ñëó÷àå
    âûâîäà èç Γ ) îáëàäàåò ñâîéñòâîì P ;
 2) äëÿ êàæäîãî ïðàâèëà âûâîäà r(A1 , . . . , Am ) ∈ Rl, åñëè âñå
    ôîðìóëû-ïîñûëêè A1 , . . . , Am îáëàäàþò ñâîéñòâîì P , òî èì
    îáëàäàåò è ôîðìóëà-çàêëþ÷åíèå äàííîãî ïðàâèëà.
 ñëó÷àå È H ðàññìàòðèâàåòñÿ åäèíñòâåííîå ïðàâèëî âûâîäà MP.
                                    ¡
   Èç äîêàçàííîé âûâîäèìîñòè ` x ¢ x è ïðàâèëà ïîäñòàíîâêè ñëå-
äóåò, ÷òî èìååò ìåñòî íèæåñëåäóþùàÿ
Ëåììà 2.1. Äëÿ ëþáîé ôîðìóëû A èñ÷èñëåíèÿ H ñïðàâåäëèâî
    ¡
` A ¢A .
   Äàëåå ìû áóäåì ïðèâîäèòü ñõåìû âûâîäîâ òîé èëè èíîé ôîðìóëû,
èìåþùåé äàííóþ ñòðóêòóðó, ïîäôîðìóëû êîòîðîé áóäóò îáîçíà÷àòüñÿ
ìåòàïåðåìåííûìè.

Страницы