ВУЗ:
Составители:
Рубрика:
Γ, A
1
, . . . , A
m
` B Γ, ∆ Γ ∪ ∆
Σ Σ
1
= Σ
2
Σ
1
Σ
2
Ax(N)
A ` A .
A
N
Rl(N)
Σ Σ
1
, . . . , Σ
m
Σ
1
. . . Σ
m
Σ
,
N `
Rl(N) +
− Γ
+ N
Γ ` A Γ ` B
Γ, Γ ` A N B
− N
Γ ` A N B
Γ ` A
,
Γ ` A N B
Γ ` B
;
+ ∨
Γ ` A
Γ ` A ∨ B
,
Γ ` B
Γ ` A ∨ B
;
− ∨
Γ ` A ∨ B Γ, A ` C Γ, B ` C
Γ ` C
;
+
¡
¢
Γ, A ` B
Γ ` A
¡
¢
B
;
−
¡
¢
Γ ` A
¡
¢
B Γ ` A
Γ ` B
;
RA
Γ ` A Γ ` ¬ A
Γ `
;
90 Ãëàâà 3. Ãåíöåíîâñêèå èñ÷èñëåíèÿ âûñêàçûâàíèé
ïèøåì Γ, A1 , . . . , Am ` B è Γ, ∆ âìåñòî Γ ∪ ∆.  êà÷åñòâå ìåòàÿçû-
êîâîé ïåðåìåííîé äëÿ ñåêâåíöèé ìû áóäåì èñïîëüçîâàòü ïðîïèñíóþ
ãðå÷åñêóþ áóêâó Σ. Ðàâåíñòâî Σ1 = Σ2 îçíà÷àåò ñèíòàêñè÷åñêîå ðà-
âåíñòâî (òîæäåñòâî) ñåêâåíöèé Σ1 è Σ2 .
Àêñèîìû Ax(N ) ïðåäñòàâëåíû åäèíñòâåííîé ñõåìîé ñåêâåíöèé
A ` A.
Ïðè ïîäñòàíîâêå â äàííóþ ñõåìó âìåñòî ìåòàñèìâîëà A ïðîèçâîëüíûõ
ôîðìóë ïîëó÷àþòñÿ ÷àñòíûå ñëó÷àè ñõåìû, êîòîðûå è áóäóò ÿâëÿòüñÿ
àêñèîìàìè ÈÑ N . Òàêèì îáðàçîì, â ÈÑ âûâîäÿòñÿ èìåííî ñåêâåíöèè,
à íå ôîðìóëû.
Ïðàâèëà âûâîäà Rl(N ), ïîñòóëèðóþùèå íà âûâîäèìîñòü ñåêâåíöèè
Σ èç ñåêâåíöèé Σ1 , . . . , Σm çàïèñûâàþò â âèäå ñõåì
Σ1 . . . Σm
,
Σ
íàçûâàÿ ñåêâåíöèè íàä ÷åðòîé ïîñûëêàì, à ñåêâåíöèþ ïîä ÷åðòîé çà-
êëþ÷åíèåì. Ïðè ïîäñòàíîâêå â óêàçàííûõ ñõåìàõ êîíêðåòíûõ ôîðìóë
âìåñòî ìåòàñèìâîëîâ ïîëó÷èì ÷àñòíûå ñëó÷àè ïðàâèë âûâîäà . Ïðàâè-
ëà âûâîäà â ÈÑ N çàäàþò ñâîéñòâà çíàêà ` îòíîñèòåëüíî ëîãè÷åñêèõ
ñâÿçîê.
Ìíîæåñòâî Rl(N ) ñîñòàâëÿþò ñëåäóþùèå ñõåìû, ãäå çíàêàìè +
è − îáîçíà÷åíû ââåäåíèå è óäàëåíèå ñîîòâåòñòâóþùåé ñâÿçêè, à Γ
ìóëüòèìíîæåñòâî ôîðìóë, âîçìîæíî ïóñòîå.
Γ ` A Γ ` B
(+ N) ;
Γ, Γ ` A N B
Γ ` ANB Γ ` ANB
(− N) , ;
Γ ` A Γ ` B
Γ ` A Γ ` B
(+ ∨) , ;
Γ ` A∨B Γ ` A∨B
Γ ` A∨B Γ, A ` C Γ, B ` C
(− ∨) ;
Γ ` C
¡ Γ, A ` B
(+ ¢) ¡ ;
Γ ` A ¢B
¡
¡ Γ ` A ¢B Γ ` A
(− ¢) ;
Γ ` B
Γ ` A Γ ` ¬A
(RA) ;
Γ `
Страницы
- « первая
- ‹ предыдущая
- …
- 88
- 89
- 90
- 91
- 92
- …
- следующая ›
- последняя »
