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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Opredelenie 2.5 (Vyvod i dokazatel~stvo v IV). Vyvodom vys-
kazyvani C iz dopuweni$i
A
1
,
. . . , A
m
(m>
0)
nazyvaets ko-
neqna posledovatel~nost~ vyskazyvani$i
C
1
,
. . .
, C
n
, v kotoro$i
C
n
=
C
i kada formula C
i
(i
= 1,
. . . , n
)
vlets ili aksio-
mo$i, ili dopuweniem, ili neposredstvenno sleduet iz predydu-
wih formul po pravilu vyvoda m
´
odus p ´o
nens (
MP
)
, zapisyvae-
momu v vide shemy
A, A → B
B
, oznaqawe$i, qto posle formul
C
i
= A i
C
j
=
A →
B pri k > i, k > j
mono napisat~
C
k
=
B
.
Sekvenci A
1
, . . . , A
m
`
C qitaets tak
: ”C formal~no vyvodi-
mo iz dopuweni$i
A
1
,
. . .
, A
m
” ;
v qastnom sluqae
m = 0
vyvod
nazyvaets dokazatel~stvom, a poluqawas sekvenci
`C qi-
taets tak: ”C
vlets formal~no$i teoremo$i”.
Primer 2.5 (Formal~ny$i vyvod sekvencii
A
→B, B
→C
`
A
→C ).
1)
A →
B
— dopuwenie,
2) B
→
C
— dopuwenie,
3) (
B
→
C
) → (
A
→
(
B
→
C)) — AS
1
,
4)
A →
(
B → C)
—
MP
2, 3,
5) (
A
→ B
) →
((
A → (
B →
C)) → (A →
C)) — AS
2
,
6) (A
→ (B →
C)) → (A → C)) —
MP 1, 5,
7) A → C —
MP
4, 6.
Primer 2.6 (Dokazatel~stvo formal~no$i teoremy `A →
A
).
1)
A
→
(
A → A
)
—
AS
1
,
2) (A → (A
→ A))
→ ((A → ((A → A
) →
A)) →
(A →
A))
— AS
2
,
3) (
A
→
((
A
→ A)
→
A
)) →
(
A → A) — MP,
1
,
2
,
4) A
→ ((A
→
A
)
→
A
) — AS
1
,
5)
A
→ A —
MP, 3
,
4.
Iz opredeleni 2.5 sleduet, qto dopuweni v formal~nyh
vyvodah ispol~zuts toqno take kak i aksiomy. Qasto vste-
qawas v matematiqeskih soqinenih fraza: ”Dopustim, qto
vypolnts uslovi (vyskazyvani) A
1
, . . .
, A
m
” oznaqaet, qto
matematik vvodit dopuweni ili, qto to e samoe dopolni-
tel~nye aksiomy. No dl qego to nuno? Otvet na tot
vopros daet neformal~na teorema, dokazanna . rbranom.
Teorema 2.10 (O dedukcii).
Esli Γ, A
`
B , to
Γ
`A → B
.
D o k a z a t e l ~ s t v o . Pust~ posledovatel~nost~
B
1
,
. . .
, B
n
= B
vlets vyvodom B iz spiska dopuweni$i
Γ, A. Preobrazuem
tot vyvod v posledovatel~nost~ A
→B
1
,
. . . ,
(
A
→B
n
) = (
A
→B),
23

Страницы