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

UptoLike

ВУЗ: 

МГУ | Москва

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

Рубрика: 

`
S
→ B
→ A
→ B, A
(→ +)
→ A
¡
¢
B
A → B
(→
¡
¢
)
0
→ B, B
→ B
(→ −)
(Cut)
H
1
S ¤
Γ → ∆ S
(Γ → ∆)
H
1
H
1
L(S) L(H
1
)
H
1
(A
1
, . . . , A
m
→ B
1
, . . . , B
n
) = A
1
N . . . N A
m
¡
¢
B
1
∨ . . . ∨ B
n
;
H
1
( → B
1
, . . . , B
n
) = B
1
∨ . . . ∨ B
n
;
H
1
(A
1
, . . . , A
m
→ ) = ¬ (A
1
N . . . N A
m
) ;
H
1
( → ) = A
0
N ¬ A
0
,
A
0
S L(H
1
)
`
S
→ A ⇒ `
H
1
H
1
(→ A)
`
S
→ A
H
1
S
Rl(S) H
1
`
H
1
H
1
(→ A)
H
1
Rl(S)
¤
S H
1
Ïåðñîíàëèÿ è àâòîðñêèé óêàçàòåëü                                                125


`S → B :
                                         ¡
             →A                      → A ¢B           ¡
                        (→ +)                      (→ ¢) 0
            → B, A                   A→B
                                                               (Cut)
                          → B, B
                                       (→ −)
                           →B
   Òàêèì îáðàçîì, ñåêâåíöèàëüíûå àíàëîãè âñåõ òåîðåì H1 âûâîäèìû
â ÈÑ S .                                                       ¤

   Äëÿ êàæäîé ñåêâåíöèè Γ → ∆ ÈÑ S îïðåäåëèì ôîðìóëó
(Γ → ∆)H1 ÈÂ H1  ïåðåâîä ñ ÿçûêà L(S) íà ÿçûê L(H1 ). Òàêîé
ïåðåâîä áóäåì îñóùåñòâëÿòü ïî ñëåäóþùèì ïðàâèëàì:
                                                              ¡¢
  H1 (A1 , . . . , Am → B1 , . . . , Bn ) = A1 N . . . N Am      B1 ∨ . . . ∨ Bn ;
  H1 ( → B1 , . . . , Bn ) = B1 ∨ . . . ∨ Bn ;
  H1 (A1 , . . . , Am → ) = ¬ (A1 N . . . N Am ) ;
  H1 ( → ) = A0 N ¬ A0 ,

ãäå A0  íåêîòîðàÿ êîíêðåòíàÿ ôîðìóëà. Ïåðåâîä ñåêâåíöèé îïðåäå-
ëÿåò è ïåðåâîä ïðàâèë ÈÑ S íà ÿçûê L(H1 ).
Ëåììà 3.14.        `S → A ⇒ `H1 H1 (→ A).
Äîêàçàòåëüñòâî. Ïóñòü `S → A. Ïîñëåäîâàòåëüíî óáåæäàåìñÿ, ÷òî
â H1 , âî-ïåðâûõ, âûâîäèìû ïåðåâîäû àêñèîì ÈÑ S è, âî-âòîðûõ, ïå-
ðåâîä âñÿêîãî ïðàâèëà èç Rl(S) äîïóñòèì â H1 . Îòñþäà ñëåäóåò, ÷òî
`H1 H1 (→ A).
   Ìîæíî âïðÿìóþ ïðîâåðèòü óïîìÿíóòûå ôàêòû èñïîëüçóÿ òåõíèêó
åñòåñòâåííîãî âûâîäà. Òàêæå ìîæíî âîñïîëüçîâàâøèñü ïîëíîòîé ÈÂ
H1 óáåäèòüñÿ, ÷òî åñëè ïåðåâîä ïîñûëîê íåêîòîðîãî ïðàâèëà èç Rl(S)
ÿâëÿåòñÿ ëîãè÷åñêèì çàêîíîì, òî è ïåðåâîä çàêëþ÷åíèÿ  ëîãè÷åñêèé
çàêîí.                                                           ¤

   Èç äîêàçàííûõ ëåìì ñëåäóåò, ÷òî ÈÑ S è ÈÂ H1 ýêâèâàëåíòíû â
óêàçàííîì ñìûñëå.

Страницы