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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
N
Σ = A
1
, . . . , A
m
` B C
1
, . . . , C
n
N
A
k
0
= A
k
(x
1
, . . . , x
n
k C
1
, . . . , C
n
), k = 1, m ,
B
0
= B(x
1
, . . . , x
n
k C
1
, . . . , C
n
) .
Σ
0
= A
1
0
, . . . , A
m
0
` B
0
Σ Σ
0
T Σ
T Σ
Rl(N)
+ N
Σ = Γ, ∆ ` A N B
Γ ` A ∆ ` B
Γ, ∆ ` A N B
.
Γ Γ
0
(Γ ` A)
0
(∆ ` B)
0
Γ
0
` A
0
∆
0
` B
0
+ N Σ
0
Rl(N) ¤
` N
+ `
N
102                   Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé


1.3 Îñíîâíûå ñâîéñòâà ÈÑ N

    ÈÑ N , òàêæå êàê è â äðóãèõ ïîäîáíûõ èñ÷èñëåíèÿõ, ñïðàâåäëèâû
ïðàâèëî ïîäñòàíîâêè è òåîðåìà î çàìåíå äåäóêòèâíî ýêâèâàëåíòíûõ.
Òåîðåìà 3.2 (Ïðàâèëî ïîäñòàíîâêè). Ïóñòü ñåêâåíöèÿ
Σ = A1 , . . . , Am ` B âûâîäèìà, à C1 , . . . , Cn ñóòü íåêîòî-
ðûå ôîðìóëû ÈÑ N . Îáîçíà÷èì
           Ak 0 = Ak (x1 , . . . , xn k C1 , . . . , Cn ),   k = 1, m ,
                      0
                   B = B(x1 , . . . , xn k C1 , . . . , Cn ) .
Òîãäà ñåêâåíöèÿ
                          Σ 0 = A1 0 , . . . , Am 0 ` B 0
òàêæå âûâîäèìà.
Äîêàçàòåëüñòâî. Ïðàâèëî ïîäñòàíîâêè â äîêàçóåìóþ ñåêâåíöèþ äî-
êàçûâàåòñÿ ñ èñïîëüçîâàíèåì ñòàíäàðòíîãî ïðè¼ìà  èíäóêöèåé ïî âû-
ñîòå äåðåâà âûâîäà.
   Åñëè Σ  àêñèîìà, òî Σ 0 òàêæå àêñèîìà è, ñëåäîâàòåëüíî, âûâî-
äèìà ïî îïðåäåëåíèþ.
   Èíà÷å, ðàññìîòðèì äåðåâî T äîêàçàòåëüñòâà Σ. Ïîñêîëüêó çàêëþ-
÷èòåëüíûé ïåðåõîä â äåðåâå T ê ñåêâåíöèè Σ ìîæåò áûòü îñóùåñòâë¼í
ïî îäíîìó èç ïðàâèë Rl(N ), â ñèëó èíäóêòèâíîãî ïðåäïîëîæåíèÿ äî-
ñòàòî÷íî ïîêàçàòü, ÷òî ïåðåõîä ïî êàæäîìó èç ýòèõ ïðàâèë ïðèâîäèò
ê äîêàçóåìîé ñåêâåíöèè.
   Ïîêàæåì ýòî íà ïðèìåðå ïðàâèëà (+ N), ò.å. êîãäà ïîñëåäíèé ïåðå-
õîä â äîêàçàòåëüñòâå ñåêâåíöèè Σ = Γ, ∆ ` A N B èìååò âèä
                              Γ ` A    ∆ ` B
                                             .
                                Γ, ∆ ` A N B
Óêàçàííóþ ïîäñòàíîâêó â íàáîð ôîðìóë Γ áóäåì îáîçíà÷àòü Γ 0 . Ïî èí-
äóêòèâíîìó ïðåäïîëîæåíèþ, ñåêâåíöèè (Γ ` A)0 è (∆ ` B)0 èëè,
÷òî òî æå, Γ 0 ` A 0 è ∆ 0 ` B 0 âûâîäèìû. Ïðèìåíÿÿ ê íèì ïðàâèëî
(+ N), ïîëó÷èì ñåêâåíöèþ Σ 0 .
   Ðàññóæäåíèÿ äëÿ äðóãèõ ïðàâèë Rl(N ) àíàëîãè÷íû.               ¤

   Çíàê âûâîäèìîñòè ` ââîäèòñÿ â ÈÑ N êàê îñíîâíîé ñèìâîë è
åãî ñâîéñòâà îïèñûâàþòñÿ ñõåìîé àêñèîì è ïðàâèëàìè âûâîäà. Îäíàêî
ëåãêî âèäåòü, ÷òî àêñèîìà è ïðàâèëî (+ `) îáåñïå÷èâàþò äëÿ ñåêâåí-
öèé ÈÑ N âûïîëíåíèå îñíîâíûõ ñâîéñòâ âûâîäèìîñòè, ïðèâåä¼ííûõ
â ï. 2.1 ãëàâû 2. Äåéñòâèòåëüíî, ñâîéñòâà ðåôëåêñèâíîñòè, ìîíîòîí-
íîñòè è ôèíèòàðíîñòè ïîêàçûâàþòñÿ ýëåìåíòàðíî, à ñâîéñòâî òðàíçè-
òèâíîñòè ñëåäóåò èç äîêàçàííîãî ïðàâèëà ñå÷åíèÿ Cut (çäåñü òðåáóåòñÿ

Страницы