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

UptoLike

ВУЗ: 

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

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

Рубрика: 

utverdeni teoremy 3.1 spravedlivy i v aksiomatiqeskom is-
qislenii predikatov pri uslovii, qto v nih znak
|
=
zamenen
na znak
` . Na isqislenie predikatov perenosits bol~xa
qast~ rezul~tatov isqisleni vyskazyvani$i, v qastnosti, esli
A
1
,
. . . , A
m
`
B
v isqislenii vyskazyvani$i, to
A
1
,
. . . , A
m
`
B
v
isqislenii predikatov. Spravedlivy pravila vvedeni i uda-
leni logiqeskih znakov
→, ∧,
∨
,
,
∼
.
Teorema 3.4 (Pravila vvedeni i udaleni kvantorov). Pust~
A(
x) — proizvol~ny$i predikat, soderawi$i
x svobodno;
pere-
menna
t
svobodna dl
x v
A(
x);
Γ — koneqny$i spisok predi-
katov
(
vozmono, pusto$i)
, ne soderawih
x svobodno
;
D
—
proizvol~ny$i predikat, ne soderawi$i
x svobodno. Spravedlivy
pravila, privedennye v tablice
:
Znak Pravilo vvedeni Pravilo udaleni
∀ Esli
Γ
`A(
x),
(
∀
x)A
(x) `A(t)
to Γ
`(
∀x
)A(
x
)
∃ A(
t)
`(
∃
x
)
A(
x
) Esli Γ, A
(x
) `
D
,
to
Γ,
(∃
x
)A
(
x)
`
D
D o k a z a t e l ~ s t v o . Vvedenie
∀
. Pust~
C
— aksioma, ne so-
derawa
x
svobodno.
1) Γ
`A
(
x
)
— po uslovi,
2) Γ , C `A
(x)
— svo$istvo 2, 1,
3) Γ
`C → A(x) — vvedenie
→, 2,
4) Γ
`
C →
(
∀x
)
A(
x
) — obobwenie, 3,
5) Γ , C
`
(
∀x
)A(
x
)
— vvedenie →
, 4,
6)
Γ
`(
∀x)A(x
) — udalenie aksiomy iz dopuweni$i, 5.
Udalenie ∀
.
1)
`(
∀
x)
A(x)
→
A
(
t) — AS
11
,
2) (
∀
x
)A
(x)
`
A
(t
)
— vvedenie
→ 1.
Vvedenie
∃
.
1) `A
(t)
→
(
∃x
)A(
x)
—
AS
12
,
2)
A
(
t) `
(∃x)
A(
x
)
— vvedenie →
, 1.
35

Страницы