Логика. Множества. Вероятность. Лексаченко В.А. - 24 стр.

UptoLike

ВУЗ: 

СПб ГУАП | Санкт-Петербург

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

Рубрика: 

kotoru mono prevratit~ v vyvod sekvencii Γ
`A
→ B , es-
li pered A
→
B
i
vstavit~ dopolnitel~nye formuly. Vstavki
zavist ot togo, qto predstavlet sobo$i B
i
.
Esli
B
i
=
A
, to vstavim posledovatel~no formuly 1) — 4)
dokazatel~stva teoremy
A
→ A (sm. primer 2.6).
Esli B
i
— aksioma ili dopuwenie, to vstavim posledova-
tel~nost~ dvuh formul B
i
, B
i
→ (A
→
B
i
)
.
Esli B
i
vyvodits po pravilu MP iz predxestvuwih
formul B
g
i
B
g
→ B
i
, kotorye prevraweny s sootvetstvuwim
obosnovaniem v
A → B
g
i
A
→
(
B
g
→
B
i
), to vstavim posledova-
tel~nost~ dvuh formul (
A → B
g
)
→ ((A → (
B
g
→
B
i
)) → (
A
→
B
i
)),
(
A
→
(B
g
→ B
i
)) → (A
→
B
i
).
Netrudno ubedit~s, qto posle tih vstavok my poluqim
vyvod
A
→ B
iz spiska dopuweni$i
Γ
.
J
Sledstvie. Esli
A
1
,
. . .
, A
m
`B , to
A
1
,
. . .
, A
m
−1
`
A
m
→ B,
. . . ,
`A
1
→
(A
2
→ (. . . (
A
m
→
B) . . .))
.
Pri ispol~zovanii tol~ko odnogo pravila vyvoda MP
vy-
vody i dokazatel~stva v IV poluqats slixkom dlinnymi.
Okazyvaets, qto mono dokazat~ neformal~nye teoremy, koto-
rye otliqats ot teorem razd. 2.2 tol~ko tem, qto znak |=
zamenen na `
. Budem sqitat~, qto formulirovki tih teorem
nam ue izvestny i numerovat~ ih temi e nomerami, qto
i sootvetstvuwie teoremy razdela 2.2, dobavl k nomeru
verhni$i xtrih sprava. Dokaem tol~ko svo$istva znaka ` i
pravila vvedeni i udaleni logiqeskih znakov.
V teoreme 2.3
0
dokazatel~stva svo$istv 1, 2 oqevidny. Pri
dokazatel~stve svo$istva 3 formal~ny$i vyvod sekvencii
Γ `C
moet byt~ zapisan kak posledovatel~na zapis~ formal~nyh
vyvodov dl Γ `
B
1
, Γ
`B
2
i t. d.
Γ `
B
k
i B
1
, . . . , B
k
`C
.
V teoreme 2.4
0
pravila perestanovki, sokraweni i pravilo
popolneni spiska dopuweni$i oqevidny.
Vvedenie → (Γ, A `B
togda i tol~ko togda, kogda Γ `
A→B ).
Odno$i iz qaste$i dokazatel~stva vlets teorema o deduk-
cii. Dl dokazatel~stva drugo$i qasti zametim, qto, esli
Γ `A →B , to posledovatel~nost~, sostavlenna iz
A i vyvoda
dl Γ
`A
→ B vlets vyvodom dl sekvencii Γ, A
`
B
.
Udalenie
→
(A , A → B `
B
).
1)
A — dopuwenie,
2) A →
B — dopuwenie,
3)
B —
MP 1, 2.
24

Страницы