ВУЗ:
Составители:
Рубрика:
H
A H
A
` A ∅ ` A
Γ B
A
1
, . . . , A
m
A
1
, . . . , A
m
` B
Γ∪{A
1
, . . . , A
m
} ` B Γ, A
1
, . . . , A
m
` B
A
1
, . . . , A
m
Γ
A
0
Γ ` A
0
Γ ` ¬ A
0
Γ 0 A Γ 0 ¬A A
Γ
Γ ` A Γ 0 A A Γ
Γ ` A
A Γ
Γ A
H
A Γ
Γ
Γ ` A
V
1
, . . . , V
k
2. Èñ÷èñëåíèå âûñêàçûâàíèé H 53
â ìíîæåñòâî). Ïîýòîìó ïðåäñòàâëÿåòñÿ, ÷òî îïèñàíèå ñîâîêóïíîñòåé ãè-
ïîòåç èìåííî êàê ìóëüòèìíîæåñòâ ôîðìóë íàèáîëåå óäîáíî. Ïðè ýòîì
çäåñü è äàëåå ìû ñ÷èòàåì, ÷òî âñå ìóëüòèìíîæåñòâà ôîðìóë íå áîëåå
÷åì ñ÷¼òíû.
Ïîíÿòíî, ÷òî ôîðìóëà A ÿâëÿåòñÿ òåîðåìîé èñ÷èñëåíèÿ H , åñëè
è òîëüêî åñëè A âûâîäèìà èç ïóñòîãî ìíîæåñòâà ãèïîòåç. Ýòî îáîñíî-
âûâàåò çàïèñü ` A êàê ñîêðàùåíèå äëÿ ∅ ` A.
Åñëè íàáîð ãèïîòåç Γ, èç êîòîðîãî âûâîäèòñÿ ôîðìóëà B êîíå÷åí è
ñîñòîèò èç ôîðìóë A1 , . . . , Am , òî ïèøóò A1 , . . . , Am ` B . Äàëåå âìå-
ñòî Γ∪{A1 , . . . , Am } ` B áóäåì ñîêðàù¼ííî ïèñàòü Γ, A1 , . . . , Am ` B .
Çäåñü ìû, â ñîîòâåòñòâèè ñî ñêàçàííûì âûøå, èìååì â âèäó îáúåäèíå-
íèå ìóëüòèìíîæåñòâ è ïîýòîìó âîçìîæåí ñëó÷àé ðàâåíñòâà íåêîòîðûõ
ôîðìóë A1 , . . . , Am .
Îïðåäåëåíèå 2.3. Ìíîæåñòâî ôîðìóë Γ íàçûâàþò ïðîòèâîðå÷èâûì ,
åñëè äëÿ íåêîòîðîé ôîðìóëû A0 ñïðàâåäëèâî êàê Γ ` A0 , òàê è
Γ ` ¬ A0 , è íåïðîòèâîðå÷èâûì , åñëè òàêîâîé ôîðìóëû íå ñóùåñòâóåò.
×èòàòåëþ ïðåäëàãàåòñÿ ñðàâíèòü ýòî îïðåäåëåíèå ñ îïðåäåëåíèåì
âûïîëíèìîñòè/íåâûïîëíèìîñòè ñîâîêóïíîñòè ôîðìóë (ñ. 24) è íå ñìå-
øèâàòü ýòè ïîíÿòèÿ.
Åñëè îäíîâðåìåííî è Γ 0 A è Γ 0 ¬A, òî ôîðìóëà A íàçûâàåòñÿ
íåçàâèñèìîé îò íàáîðà ôîðìóë Γ.
Îäíèì èç îñíîâíûõ âîïðîñîâ èñ÷èñëåíèé ÿâëÿåòñÿ óñòàíîâëåíèå
ôàêòîâ Γ ` A èëè Γ 0 A. Äîêàçàòåëüñòâî âûâîäèìîñòè A èç Γ ìî-
æåò îñóùåñòâëÿòüñÿ ïðÿìûì ìåòîäîì ïðåäúÿâëåíèåì âûâîäà. Îäíà-
êî êàê ìû âñêîðå óâèäèì, äàæå äëÿ äîñòàòî÷íî ïðîñòûõ ôîðìóë òàêîé
ââîä îáû÷íî îêàçûâàåòñÿ ÷ðåçâû÷àéíî äëèííûì.  òîæå âðåìÿ, äëÿ
äîêàçàòåëüñòâà Γ ` A äîñòàòî÷íî â ðàìêàõ ìåòàòåîðèè ïîêàçàòü, ÷òî
ñîîòâåòñòâóþùèé âûâîä ñóùåñòâóåò. Ñ äðóãîé ñòîðîíû, óñòàíîâëåíèå
ôàêòà íåâûâîäèìîñòè A èç Γ âîçìîæíî òîëüêî â ðàìêàõ ìåòàòåîðèè
èñ÷èñëåíèÿ. Çàìåòèì, ÷òî, êàê ïðàâèëî, òàêîå äîêàçàòåëüñòâî ðåäêî
óäà¼òñÿ ïðîâåñòè ÷èñòî ñèíòàêñè÷åñêè, â ñâÿçè ñ ÷åì ïðèáåãàþò ê ìå-
òîäàì ñåìàíòè÷åñêèì, ò.å. ê êîíñòðóèðîâàíèþ èíòåðïðåòàöèè, ÿâëÿþ-
ùåéñÿ ìîäåëüþ äëÿ Γ è êîíòðìîäåëüþ äëÿ A. Òàêîé ïîäõîä âîçìîæåí
â ñèëó ýêâèâàëåíòíîñòè ïîíÿòèé âûïîëíèìîñòè è íåïðîòèâîðå÷èâîñòè
äëÿ ìíîæåñòâà ôîðìóë ÈÂ H , ÷òî áóäåò ïîêàçàíî íèæå.
Ïîíÿòíî, ÷òî åñëè óäàëîñü äîêàçàòü ñóùåñòâîâàíèå âûâîäà ôîðìó-
ëû A èç íàáîðà ôîðìóë Γ, òî çàìåíÿÿ (âçàèìíî îäíîçíà÷íî) â ôîð-
ìóëàõ èç Γ ïðîïîçèöèîíàëüíûå ïåðåìåííûå ìåòàñèìâîëàìè ôîðìóë,
ïîëó÷àåì âûâîäèìîñòü Γ ` A, êîòîðàÿ áóäåò äîïóñòèìûì ïðàâèëîì
âûâîäà. Åñëè óäà¼òñÿ äîêàçàòü, ÷òî èç íåêîòîðûõ âûâîäîâ V1 , . . . , Vk
Страницы
- « первая
- ‹ предыдущая
- …
- 51
- 52
- 53
- 54
- 55
- …
- следующая ›
- последняя »
