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

UptoLike

ВУЗ: 

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

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

Рубрика: 

Opredelenie 4.3 (Neopredelennoe opisanie). Pust~ sootnoxe-
nie
A(
x
1
, . . .
, x
n
, w
)
soderit svobodno tol~ko razliqnye pere-
mennye
x
1
, . . .
, x
n
, w (
n
>
0). Term
τ
w
A(
x
1
,
. . . , x
n
, w), v kotorom
peremenna
w
svzana, nazyvaets neopredelennym opisaniem
”nekotorogo w
, takogo, qto `(∀
x
1
) . . . (
∀x
n
)(
∃
w
)
A(
x
1
, . . . , x
n
, w)
”.
tot term opredelet predmetnu funkci
f
(
x
1
,
. . .
, x
n
)
τ
w
A(x
1
,
. . .
, x
n
, w
).
Pri ispol~zovanii v dokazatel~stvah neopredelennyh opisa-
ni$i nel~z priment~ pravila obobweni i konkretizacii po
peremennym, vhodwim svobodno v termy τ
w
A(x
1
,
. . .
, x
n
, w
)
.
Teorema 4.1 (Udalenie neopredelennogo opisani). Pust~ Γ
— spisok sootnoxeni$i (
vozmono, pusto$i
);
C — pro-
izvol~noe sootnoxenie; A
(x
1
,
. . .
, x
n
, w) i funkci f
, udov-
letvort opredeleni
4
.
5;
funkci f ne vhodit v
sootnoxeni spiska
Γ, A(x
1
, . . .
, x
n
, w), C
. Togda, esli
Γ,
(
∀x
1
) . . . (
∀x
n
)
A
(x
1
,
. . .
, x
n
, f
(x
1
,
. . . , x
n
))
`
C , to
Γ
`
C .
Term τ
pozvolet opredelit~ kvantory formulami [3]:
(∃
x
)
A
(x) A(
τ
x
A(x
)),
(
∀
x)
A(x
)
A(
τ
x
A(x)). (1)
Pri takom opredelenii shemu
AS
11
mono isklqit~, a shemu
AS
12
zapisat~ v vide A(
t
)
→ A(
τ
x
A(x
))
. Prinima aksiomati-
ku N. Burbaki [3], vvedem dl
τ
sleduwu shemu aksiom,
nakladyvawu ograniqenie na ispol~zuemye funkcii vybora.
Aksioma terma τ
. (∀x
)(
A
(
x) ∼ B
(x))
→
(τ
x
A
(
x) =
τ
x
B(x
))
.
Opredelenie 4.4 (Odnoznaqnye i funkcinal~nye sootnoxeni).
Sootnoxenie
R(
x)
, soderawee svobodno bukvu x i ne sodera-
wee razliqnye bukvy
y, z , nazyvaets odnoznaqnym po x, esli
`
(
∀
y)(∀z
)((
R(y
)
∧R(
z)) → (
y =
z
))
. Sootnoxenie R
(x)
nazyvaets
funkcional~nym po x, esli ono odnoznaqno i `
(
∃
x
)
R
(x).
Teorema 4.2 (Ob odnoznaqnyh i funkcional~nyh sootnoxenih).
1
. Pust~
R
(x) odnoznaqno po
x
. Togda `R
(
x) →
(x = τ
x
R(x
))
.
2
. Pust~ `R
(x
) → (
x = t
), gde term
t ne soderit
x svobodno.
Togda
R
(x)
odnoznaqno po x
.
3
. Pust~ R(
x) funkcional~no po x. Togda
`R(
x) ∼ (x = τ
x
R(
x))
.
4
. Pust~ `R
(
x)
∼ (
x = t
)
, gde term
t ne soderit x svobodno.
Togda R
(
x
)
funkcional~no po
x.
D o k a z a t e l ~ s t v o . 1. Pust~ R(
x)
odnoznaqno po
x
. Togda
1) `(
∀
z
)(∀
y)((R
(
y
)∧
R
(
z))
→
(y = z
))
— dopuwenie,
2)
`(∀
y)((
R(
y)
∧
R
(
τ
x
R(
x
)))
→(y
=
τ
x
R
(
x)))
— udalenie ∀, 1,
3) `R(
x)
∧
(∃
x)
R(x
)
→ (x = τ
x
R(
x))
— (1), udalenie ∀
, 2,
4) R(x
),
(∃x)R(
x) `x =
τ
x
R(x)
— udalenie ∧ i →, 3,
39

Страницы