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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

H
H
r (A
¡
¢
B, A) = r (A, A
¡
¢
B) = B,
A
¡
¢
B, A ` B (MP )
A
¡
¢
B A B
`
H `
I
I
H
A H
A
1
, . . . , A
l
F m(H)
A
l
= A
Ax(H)
A
l
A
` A A 0 A
[H]
H
H
H x
¡
¢
x
(x
¡
¢
((x
¡
¢
x)
¡
¢
x))
¡
¢
((x
¡
¢
(x
¡
¢
x))
¡
¢
(x
¡
¢
x))
A2 B 7→ x
¡
¢
x A, C 7→ x
x
¡
¢
((x
¡
¢
x)
¡
¢
x) A1 B 7→ x
¡
¢
x
(x
¡
¢
(x
¡
¢
x))
¡
¢
(x
¡
¢
x)
x
¡
¢
(x
¡
¢
x) A1 B 7→ x
x
¡
¢
x
`
50           Ãëàâà 2. Èñ÷èñëåíèÿ âûñêàçûâàíèé. Ãèëüáåðòîâñêèå ÈÂ


ÿâëÿåòñÿ ëè îíà àêñèîìîé H èëè íåò. Òàêèå èñ÷èñëåíèÿ íàçûâàþò
ýôôåêòèâíî àêñèîìàòèçèðóåìûìè .
   Èñ÷èñëåíèå H èìååò åäèíñòâåííîå ïðàâèëî âûâîäà
                     ¡                 ¡
                r (A ¢ B, A) = r (A, A ¢ B) = B,
êîòîðîå áóäåì çàïèñûâàòü â âèäå
                             ¡
                          A ¢ B, A ` B                                 (M P )
è îáîçíà÷àòü MP îò åãî ëàòèíñêîãî íàçâàíèÿ modus           ponens8 .
                                                            Òàêàÿ
                                ¡
çàïèñü ÷èòàåòñÿ ¾èç ôîðìóë A ¢ B è A âûâîäèòñÿ ôîðìóëà B ¿ è
ÿâëÿåòñÿ àíàëîãîì ñîîòâåòñòâóþùåãî ïðàâèëà ëîãè÷åñêîãî ñëåäîâàíèÿ.
   Ñèìâîë ` íàçûâàþò çíàêîì âûâîäèìîñòè . ßñíî, ÷òî ýòî òàêæå
ìåòàñèìâîë H . Ïèøóò `I , êîãäà íóæíî ïîä÷åðêíóòü, ÷òî ðàññìàòðè-
âàåìàÿ âûâîäèìîñòü èìååò ìåñòî â èñ÷èñëåíèè I 9 .
   Ïîíÿòèÿ òåîðåìû è âûâîäà â H ââîäÿòñÿ â ñîîòâåòñòâèè ñ ïðèâå-
ä¼ííûì âûøå îïðåäåëåíèåì, ãäå ¾âûðàæåíèå¿ çàìåíåíî íà ¾ôîðìóëà¿,
à ïîä ïðàâèëîì ïîíèìàåòñÿ MP:
Îïðåäåëåíèå 2.1. Ôîðìóëà A íàçûâàåòñÿ òåîðåìîé ÈÂ H , åñëè ñó-
ùåñòâóåò êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü A1 , . . . , Al ôîðìóë èç F m(H)
òàêàÿ, ÷òî Al = A, è êàæäûé ýëåìåíò ýòîé ïîñëåäîâàòåëüíîñòè ëèáî
ïðèíàäëåæèò Ax(H), ëèáî ïðÿìî ñëåäóåò èç êàêèõ ëèáî ïðåäûäóùèõ
ôîðìóë ïî ïðàâèëó MP.
   Óêàçàííàÿ ïîñëåäîâàòåëüíîñòü íàçûâàåòñÿ âûâîäîì òåîðåìû A, à
çíà÷åíèå l  äëèíîé âûâîäà .
    Òîò ôàêò, ÷òî A åñòü òåîðåìà ðàññìàòðèâàåìîãî èñ÷èñëåíèÿ, çàïè-
ñûâàþò â ôîðìå ` A. Åñëè A íå åñòü òåîðåìà, òî ïèøóò 0 A. Â ñî-
îòâåòñòâèè ñ ïðèíÿòûì îáîçíà÷åíèåì [H] åñòü ìíîæåñòâî âñåõ òåîðåì
èñ÷èñëåíèÿ H .
    Ñèíòàêñèñ È H ïîëíîñòüþ çàäàí.  êà÷åñòâå ïðèìåðà ïðèâåä¼ì
                                 ¡
âûâîä â ÈÂ H ôîðìóëû x ¢ x . Ýëåìåíòû âûâîäà áóäåì íóìåðîâàòü
÷èñëàìè â êðóãëûõ ñêîáêàõ è äàâàòü ïîÿñíåíèÿ ê èõ ïîëó÷åíèþ.
         ¡      ¡    ¡     ¡       ¡      ¡    ¡     ¡
 (1) (x ¢ ((x ¢ x) ¢ x)) ¢ ((x ¢ (x ¢ x)) ¢(x ¢ x))       ñõåìà àêñèîì
                                      ¡¢
      A2¡ ñ ïîäñòàíîâêàìè
               ¡    ¡        B →
                               7   x     x  è A, C →
                                                   7   x        ¡
 (2) x ¢¡((x ¢¡ x) ¢ x)
                      ¡    ñõåìà A1 ñ ïîäñòàíîâêîé B 7→ x ¢ x
                          ¡
 (3) (x ¡¢ (x ¡¢ x)) ¢ (x ¢ x)      ïî MP èç (1) è (2)
 (4) x ¢¡ (x ¢ x)     ñõåìà àêñèîì A1 ñ ïîäñòàíîâêîé B 7→ x
 (5) x ¢ x      ïî MP èç (3) è (4)
   Çàìåòèì, ÷òî ïðè âûâîäå èñïîëüçîâàëèñü òîëüêî ïåðâûå äâå ñõåìû
àêñèîì.
  8 Modus ponens  ïîëîæèòåëüíûé ñïîñîá (óìîçàêëþ÷åíèÿ); äàííîå ïðàâèëî òàê-
æå íàçûâàþò ¾ïðàâèëîì îòäåëåíèÿ¿.
  9 Çíàê ` ââ¼ë Ã.Ôðåãå.

Страницы