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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

[[[ p
¡
¢
f ]
¡
¢
f ]
¡
¢
p ]
t
[f
¡
¢
f] ∼
∼ A
def
= [A
¡
¢
f]
pt∨ ∼ p
[[[[[f
¡
¢
f]
¡
¢
[[[f
¡
¢
f]
¡
¢
p]
¡
¢
f]]
¡
¢
f]
¡
¢
[p
¡
¢
f]]
¡
¢
[p
¡
¢
f] .
.
A
¡
¢
. B
¡
¢
A
[A
¡
¢
. B
¡
¢
C]
¡
¢
. [A
¡
¢
B]
¡
¢
[A
¡
¢
C]
.
`
H
f
p
¡
¢
p
F
2
H
0
H
0
H
1
H
0
H
0
T aut
A
1
, . . . , A
m
` A , A
1
, . . . , A
m
² A .
T aut
5. Òèïû ëîãè÷åñêèõ èñ÷èñëåíèé è èõ ïðåäñòàâëåíèÿ                               85

                ¡     ¡       ¡¢
       3. [[[ p ¢ f ] ¢ f ]      p].
   ˆ Ïðàâèëà âûâîäà: MP è ïîäñòàíîâêè ôîðìóëû âìåñòî ïåðåìåííîé
     (îäíîé).
   Ââîäèòñÿ ñèìâîë t (êîíñòàíòà ¾èñòèíà¿) êàê ñîêðàùåíèå
        ¡
äëÿ [f ¢ f ]. Òàêæå ââîäÿòñÿ ñèìâîëû îòðèöàíèÿ ∼ ïî ïðàâèëó
    def    ¡
∼ A = [A ¢ f ], áóëåâûõ îïåðàöèé êàê ñîîòâåòñòâóþùèå ñîêðàùåíèÿ è
ïðàâèëà ýêîíîìèè ñêîáîê. Íàïðèìåð, pt∨ ∼ p ÿâëÿåòñÿ ñîêðàùåíèåì
äëÿ
              ¡     ¡     ¡     ¡    ¡      ¡     ¡   ¡        ¡¢    ¡
       [[[[[f ¢ f ] ¢[[[f ¢ f ] ¢ p] ¢ f ]] ¢ f ] ¢[p ¢ f ]]      [p ¢ f ] .

   Äëÿ ñîêðàùåíèÿ ÷èñëà ñêîáîê ââîäèòñÿ íîâûé ñèìâîë . (òî÷êà). Åñ-
ëè âíóòðè ñêîáîê âûïîëíÿåòñÿ íåñêîëüêî îäíîðîäíûõ ïî ñèëå ñâÿçûâà-
íèÿ ëîãè÷åñêèõ ñèìâîëîâ, òî òî÷êîé âíèçó îòìå÷àþò ñèìâîë, êîòîðûé
âûïîëíÿåòñÿ â ïîñëåäíþþ î÷åðåäü. Òàêèì îáðàçîì, òî÷êà óêàçûâàåò
íà ãëàâíûé ñèìâîë ôîðìóëû èëè íåêîòîðîé å¼ ïîäôîðìóëû. Ïðè âîñ-
ñòàíîâëåíèè ñêîáîê âìåñòî òî÷êè ñòàâÿò ëåâóþ ñêîáêó. Ïàðíàÿ ê íåé
ïðàâàÿ ñêîáêà ñòàâèòñÿ ïåðåä ïåðâîé ïîñëå íå¼ ïðàâîé ñêîáêîé, íå èìå-
þùåé ïàðíîé èëè, åñëè òàêîâîé íåò, â êîíöå ôîðìóëû. Íàïðèìåð, çà-
êîíû óòâåðæäåíèÿ êîíñåêâåíòà è ñàìîäèñòðèáóòèâíîñòè èìïëèêàöèè ñ
ó÷¼òîì äàííîãî ñîãëàøåíèÿ çàïèøóòñÿ êàê
         ¡     ¡
      A ¢. B ¢A       è
         ¡¢    ¡    ¡     ¡    ¡    ¡
      [A . B ¢ C] ¢ . [A ¢ B] ¢[A ¢ C] .
Ñèìâîë . ÷àñòî ïðèìåíÿåòñÿ äëÿ ñîêðàùåíèÿ ÷èñëà ñêîáîê è â äðóãèõ
èñ÷èñëåíèÿõ.
                             ¡
   Äàëåå äîêàçûâàþòñÿ `Hf p ¢ p è äîïóñòèìîñòü ïðàâèëà Subst.

F Àäåêâàòíîé ôîðìàëèçàöèé àëãåáðû ëîãèêè C2 ÿâëÿåòñÿ ñëåäóþ-
ùåå èñ÷èñëåíèå, êîòîðîå ìû îáîçíà÷èì H0 .
   ˆ ßçûê H0 ñîâïàäàåò ñ ÿçûêîì H1 .
   ˆ Àêñèîìàìè H0 ÿâëÿåòñÿ ëþáàÿ òàâòîëîãèÿ.
   ˆ H0 èìååò åäèíñòâåííîå ïðàâèëî âûâîäà  ïðàâèëî òàâòîëîãè-
     ÷åñêîãî ñëåäîâàíèÿ (T aut):

                A1 , . . . , Am ` A ,   åñëè     A1 , . . . , Am ² A .

ßñíî, ÷òî MP è âñå ðàññìîòðåííûå ðàíåå äîïóñòèìûå ïðàâèëà âûâîäà
â ñèëó ñåìàíòè÷åñêîé ïîëíîòû ñóòü ÷àñòíûå ñëó÷àè ïðàâèëà T aut.

Страницы