ВУЗ:
Составители:
Рубрика:
Rl r ∈ Rl r(E
1
, . . . , E
m
) = E E
1
, . . . , E
m
E r
I
I = h Al(I), Ex(I), Ax(I), Rl(I) i ,
L(I) = h Al(I), Ex(I) i I
E
I
E
1
, . . . , E
l
I E
l
= E
Ax(I)
Rl(I)
E l
I [I]
[I] = Ex(I)
[I] ⊂ Ex(I)
r
0
Rl(I)
[I] r
0
I
44 Ãëàâà 2. Èñ÷èñëåíèÿ âûñêàçûâàíèé. Ãèëüáåðòîâñêèå ÈÂ
îïåðàöèé íàä ìåòàÿçûêîâûìè ïåðåìåííûìè, ò.å. îíè âñåãäà ÿâëÿþò-
ñÿ ¾ñõåìàìè¿. Ìíîæåñòâà ïðàâèë âûâîäà èñ÷èñëåíèÿ áóäåì èìåíîâàòü
Rl. Åñëè r ∈ Rl è r(E1 , . . . , Em ) = E , òî âûðàæåíèÿ E1 , . . . , Em íà-
çûâàþòñÿ ïîñûëêàìè , à E çàêëþ÷åíèåì ïðàâèëà r è ãîâîðÿò, ÷òî
çàêëþ÷åíèå ïðÿìî ñëåäóåò èç ïîñûëîê ïî äàííîìó ïðàâèëó.
Òàêèì îáðàçîì, ëîãè÷åñêîå èñ÷èñëåíèå I åñòü ÷åòâåðêà
I = h Al(I), Ex(I), Ax(I), Rl(I) i ,
à ïàðà L(I) = h Al(I), Ex(I) i åñòü ÿçûê èñ÷èñëåíèÿ I .
Èñ÷èñëåíèå ïîçâîëÿåò, îòòàëêèâàÿñü îò àêñèîì, ïîëó÷àòü ñ ïîìî-
ùüþ ïðàâèë âûâîäà íîâûå âûðàæåíèÿ. Âûðàæåíèå E íàçûâàåòñÿ òåî-
ðåìîé ëîãè÷åñêîãî èñ÷èñëåíèÿ I , åñëè ñóùåñòâóåò êîíå÷íàÿ ïîñëåäî-
âàòåëüíîñòü E1 , . . . , El âûðàæåíèé èñ÷èñëåíèÿ I òàêàÿ, ÷òî El = E ,
è êàæäûé ýëåìåíò ýòîé ïîñëåäîâàòåëüíîñòè ëèáî ïðèíàäëåæèò Ax(I),
ëèáî ïðÿìî ñëåäóåò èç êàêèõ ëèáî ïðåäûäóùèõ âûðàæåíèé ïî íåêîòî-
ðîìó ïðàâèëó èç Rl(I). Ïðè ýòîì ñàìà óêàçàííàÿ ïîñëåäîâàòåëüíîñòü
íàçûâàåòñÿ âûâîäîì òåîðåìû E , à çíà÷åíèå l äëèíîé âûâîäà .
Òåîðåìû íàçûâàþò òàêæå äîêàçóåìûìè èëè âûâîäèìûìè âûðàæå-
íèÿìè. Âñå àêñèîìû òðèâèàëüíî âûâîäèìû (äëèíà âûâîäà ðàâíà 1).
Ìíîæåñòâî äîêàçóåìûõ âûðàæåíèé èñ÷èñëåíèÿ I îáîçíà÷àþò [I]. Ðà-
âåíñòâî [I] = Ex(I) îçíà÷àåò, ÷òî âûâîäèìû âñå ïðàâèëüíî ïîñòðîåí-
íûå âûðàæåíèÿ äàííîãî ÿçûêà. Òàêèå èñ÷èñëåíèÿ íàçûâàþò òðèâèàëü-
íûìè , âðÿä ëè îíè ïðåäñòàâëÿþò êàêîé-ëèáî ïðàêòè÷åñêèé èíòåðåñ, è
ïîýòîìó ìû ñ÷èòàåì, ÷òî [I] ⊂ Ex(I).
Îïðåäåëåíèå âûâîäèìîñòè âûðàæåíèé èñïîëüçóþò äëÿ äîêà-
çàòåëüñòâ êàêèõ-ëèáî èõ ñâîéñòâ: òàêèå äîêàçàòåëüñòâà ïðîâîäÿò
ìåòîäîì ìàòåìàòè÷åñêîé èíäóêöèè ïî ÷èñëó ïðèìåíåíèé ïðàâèë
(äëèíå âûâîäà). Áóäåì ãîâîðèòü, ÷òî ïðè ýòîì èñïîëüçóåòñÿ ïðèíöèï
èíäóêöèè ïî äëèíå âûâîäà .
Ïóñòü r 0 íåêîòîðîå ïðàâèëî, íå âõîäÿùåå â Rl(I), íî òàêîå, ÷òî
èñïîëüçîâàíèå åãî íå ðàñøèðÿåò ìíîæåñòâà [I]. Òîãäà r 0 íàçûâàþò
äîïóñòèìûì ïðàâèëîì äëÿ èñ÷èñëåíèÿ I . Íà ïðàêòèêå ïðè âûâîäàõ
òåîðåì äîïóñòèìûå ïðàâèëà èñïîëüçóþòñÿ ÷ðåçâû÷àéíî øèðîêî.
Ñóììèðóÿ âûøåñêàçàííîå, ìîæíî ñêàçàòü, ÷òî èñ÷èñëåíèÿ ÿâëÿþò-
ñÿ ïîëíîñòüþ ôîðìàëèçîâàííûìè èíñòðóìåíòàìè äëÿ âûâîäà òåîðåì.
1.2 Ñåìàíòèêà èñ÷èñëåíèÿ. Ìåòàÿçûê è ìåòàòîðèÿ. Î òåî-
ðèè äîêàçàòåëüñòâ
Èòàê, èñ÷èñëåíèå çàäà¼òñÿ â òåðìèíàõ îòíîøåíèé è ñâÿçåé ìåæ-
äó ñâîèìè áàçîâûìè ýëåìåíòàìè ò.å. ñèíòàêñè÷åñêè . Ñèíòàêñèñ îïðå-
Страницы
- « первая
- ‹ предыдущая
- …
- 42
- 43
- 44
- 45
- 46
- …
- следующая ›
- последняя »
