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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

N
N
Al(N )
p, q, . . . z
¬
¡
¢
N ∨
`
N
N
N
H
1
≡
F m(N) A
H
Γ, ∆, . . .
Σ A, A
0
, A
0
, A
1
, B, . . . , Γ, ∆, . . .
N
N
A
1
, . . . , A
m
` B
` B
A
1
, . . . , A
m
`
`
A
1
, . . . , A
m
B N
N N
Seq(N )
Γ ` B
Γ ` Γ
Γ
Γ
Γ∪{A
1
, . . . , A
m
} ` B
1. Èñ÷èñëåíèå N íàòóðàëüíîãî òèïà                                        89


1.1 Îïðåäåëåíèå ÈÑ íàòóðàëüíîãî òèïà N .

Ñèíòàêñèñ. Àëôàâèò Al(N ) âêëþ÷àåò â ñåáÿ ñèìâîëû
   ˆ ïðîïîçèöèîíàëüíûõ ïåðåìåííûõ: p, q, . . . z (âîçìîæíî ñ èíäåê-
     ñàìè);
                                         ¡
   ˆ ïðèìèòèâíûõ ëîãè÷åñêèõ ñâÿçîê: ¬, ¢, N , ∨ ;
   ˆ âûâîäèìîñòè: ` ;
   ˆ âñïîìîãàòåëüíûå: ïàðà êðóãëûõ ñêîáîê è çàïÿòàÿ.
    Çàìåòèì, ÷òî ñèìâîë âûâîäèìîñòè âêëþ÷¼í â àëôàâèò ÈÑ N è íå
ÿâëÿåòñÿ ìåòàñèìâîëîì, êàê â ãèëüáåðòîâñêèõ èñ÷èñëåíèÿõ. Ýòî ïðè-
âåä¼ò ê íåîáõîäèìîñòè çàäàâàòü åãî ñâîéñòâà àêñèîìàòè÷åñêè (÷òî è
áóäåò ñäåëàíî íèæå).
    Âûðàæåíèÿìè ÈÑ N áóäóò ÿâëÿòüñÿ ôîðìóëû è ñåêâåíöèè.
    Îïðåäåëåíèå ôîðìóëû â ÈÑ N ñîâïàäàåò ñ àíàëîãè÷íûì îïðåäå-
ëåíèåì â H1 è ñâÿçêà òàêæå ≡ ââîäèòñÿ êàê ñîêðàùåíèå ïî D3 (ñì.
c. 49). Îòñþäà ñëåäóåò ñîâïàäåíèå ìíîæåñòâ F m(N ) è A. Ìû áóäåì
ïîëüçîâàòüñÿ òåìè æå îáîçíà÷åíèÿìè äëÿ ôîðìóë, ÷òî è â H . Äëÿ îáî-
çíà÷åíèÿ êîíå÷íûõ íàáîðîâ ôîðìóë áóäóò èñïîëüçîâàòüñÿ ãðå÷åñêèå
ïðîïèñíûå áóêâû Γ, ∆, . . . (âîçìîæíî ñ íàòóðàëüíûìè èíäåêñàìè), çà
èñêëþ÷åíèåì áóêâû Σ. Ïîíÿòíî, ÷òî A, A0 , A0 , A1 , B, . . . , Γ, ∆, . . . 
ìåòàÿçûêîâûå ïåðåìåííûå äëÿ ôîðìóë è èõ íàáîðîâ â ÈÑ N .
Îïðåäåëåíèå 3.1. Ñåêâåíèöÿìè â N ÿâëÿþòñÿ ñòðîêè ñèìâîëîâ ñëå-
äóþùåãî âèäà:
      1)   A1 , . . . , Am ` B ,
      2)   ` B,
      3)   A1 , . . . , Am ` ,
      4)   `,
ãäå A1 , . . . , Am è B  ôîðìóëû ÈÑ N .
    Åñëè ôîðìóëû ÿâëÿþòñÿ ôîðìàëèçàöèÿìè ñëîæíûõ âûñêàçûâàíèé,
òî ñåêâåíöèè  ôîðìàëèçàöèè òåîðåì èëè óòâåðæäåíèé î âûâîäèìîñòè
òåõ èëè èíûõ ôîðìóë èç ñîâîêóïíîñòè äðóãèõ (ïîäðîáíåå ñì. íèæå ïðè
ðàññìîòðåíèè ñåìàíòèêè ÈÑ N ). Ìíîæåñòâî ñåêâåíöèé ÈÑ N áóäåì
îáîçíà÷àòü Seq(N ).
    Ìû áóäåì çàïèñûâàòü ñåêâåíöèè âèäà (1) è (2) êàê Γ ` B , à âèäà
(3) è (4)  êàê Γ ` , ïîíèìàÿ ïîä Γ êîíå÷íûé íàáîð (ìóëüòìíîæåñòâî)
ñîîòâåòñòâóþùèõ ôîðìóë, âîçìîæíî ïóñòîé. Êîíå÷íîñòü Γ ñëåäóåò èç
òîãî, ÷òî ñåêâåíöèÿ  ñòðîêà ñèìâîëîâ êîíå÷íîé äëèíû. Ýëåìåíòû Γ
áóäåì íàçûâàòü ãèïîòåçàìè. Êàê îáû÷íî, âìåñòî Γ∪{A1 , . . . , Am } ` B

Страницы