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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Udalenie ∃
.
1) Γ , A
(x
)
`D — po uslovi,
2) Γ `
A
(x
)
→ D
— vvedenie
→ 1,
3) Γ `
(∃x
)A(
x)
→ D
— konkretizaci, 2,
4)
Γ ,
(
∃x)
A(x)
`D
— vvedenie
→
3. J
Teorema 3.5 (Pravila pereimenovani peremennyh).
Pust~ pre-
dikat
A(
x
) soderit x
svobodno, peremenna y
svobodna dl x
v A(x). Togda
: 1)
esli
`
A
(x)
, to
`
A(
y); 2)
esli `(
∀
x)A(x
)
,
to `(∀
y
)
A
(
y
); 3) esli `(
∃
x
)
A
(
x), to
`
(
∃
y
)
A(y)
.
D o k a z a t e l ~ s t v o . Dokaem 1.
1) `A(x)
— po uslovi,
2)
`
(
∀
x)
A
(x) — vvedenie
∀
, 1,
3)
`A
(y
) — udalenie
∀, svo$istvo 3, 2.
Dokaem 2.
1) `
(∀x)
A
(x)
— po uslovi,
2) `
A(
y)
— udalenie
∀
, svo$istvo 3, 1,
3)
`
(∀y)A(y)
— vvedenie ∀
, 2.
Punkt 3 sleduet iz 2 v silu punkta 5 teoremy 3.1.
J
Pravila pereimenovani peremennyh pozvolt kadu for-
mulu zapisat~ tak, qto vse razliqnye peremennye (svobodnye
i svzannye) oboznaqats razliqnymi bukvami.
Opredelenie 3.6 (Zamknutye predikaty, zamykanie). Predi-
kat, ne soderawi$i svobodno$i peremenno$i, nazyvaets zamknu-
tym. Esli predikat A
soderit svobodno tol~ko peremennye
x
1
, . . . , x
n
, to A
0
= (
∀x
1
) . . . (∀x
n
)A nazyvaets zamykaniem
A.
S pomow~ pravil vvedeni i udaleni
∀
netrudno doka-
zat~ sleduwee utverdenie.
Teorema 3.6 (O zamykanii). Esli
A
0
— zamykanie predikata
A, to `A
0
togda i tol~ko togda, kogda
`
A.
Aksiomatiqeskoe isqislenie predikatov IPS poluqaets iz
isqisleni vyskazyvani$i IS dobavleniem pravil vyvoda:
16)
Γ
4
`A(x)
Γ
4
`(
∀
x)
A(x)
(vvedenie ∀
), 17)
Γ `(
∀
x)A(
x
)
Γ `A
(t
)
(udalenie ∀
),
18)
Γ `A(
t)
Γ
`(
∃
x
)A
(
x
)
(vvedenie ∃
),
19)
Γ
4
, A
(x) `
D
Γ
4
, (
∃x
)
A
(
x
)
`
D
(udalenie ∃
).
V tih pravilah
Γ , Γ
4
— koneqnye spiski formul, vozmono,
pustye. Spisok Γ
4
i formula D
ne soderat
x
svobodno,
peremenna t
svobodna dl
x v
A(x
)
.
36

Страницы