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

UptoLike

ВУЗ: 

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

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

Рубрика: 

5) (∃
x)
R(x
)
`R(x)
→
(
x
=
τ
x
R(x)) — vvedenie →
, 4,
6)
R(x) `
(∃x
)R(x) — vvedenie ∃,
7) R
(
x)
`R
(
x) →
(x
= τ
x
R
(
x
))
— seqenie, 5, 6,
8) R(x
)
, R
(x
)
`
x =
τ
x
R
(x) — udalenie
→ i ∧
, 7,
9)
`
R(
x
) →
(
x =
τ
x
R(
x
)) — sokrawenie, vvedenie
→, 8.
2. Pust~
`R
(x)→
(x
=
t
) i term
t ne soderit x
svobodno.
1)
`R(x
)
→ (
x =
t
) — dopuwenie,
2) `
R(
y
) →
(y = t
)
— pereimenovanie, 1,
3)
`R
(z
) →
(z
=
t
)
— pereimenovanie, 1,
4) R
(y) `
(
y
= t
)
— udalenie
→, 1,
5) R
(
z) `(
z = t
)
— udalenie →
, 1,
6) R
(y
), R
(z)
`
(y = t)
∧
(
z
=
t) — vvedenie
∧, 4, 5,
7)
R
(
y
)
, R
(
z)
`y
=
z
— seqenie, 6, E
2
,
8)
`
(R(
y
)∧
R(
z
)) → (
y =
z) — vvedenie ∧ i →
, 7,
9) `(∀y
)(
∀z)((
R
(y)
∧R(z
)) →
(
y
= z
)) — vvedenie ∀
, 8.
3. Pust~
R(x)
funkcional~no po
x
.
1) `R(x)
→ (x
= τ
x
R
(x
))
— punkt 1,
2) `
(
x
=
τ
x
R
(x)) →
(R
(
x
) ∼
(∃x
)
R
(x
))
—
E
P
, (1),
3) x
=
τ
x
R(
x) `R
(x
) ∼
(∃
x
)R
(
x) — udalenie ∧
i →, 2,
4)
x
=
τ
x
R(x)
`
(
∃
x)R(
x) →
R
(x
) — udalenie
∧
, 3,
5) `(
x = τ
x
R
(x
))
→
((
∃
x
)R(x) →
R
(x
))
— vvedenie
→
, 4,
6) `
(∃x
)
R(
x)
→
((x =
τ
x
R
(x))
→ R
(x)) — a→
(b→c) =
b→(
a→c), 5,
7) `(∃x
)R
(
x
) — dopuwenie,
8) `
(
x
=
τ
x
R(x)) → R
(x)
— udalenie →, 6, 7,
9) `R(
x
)
∼
(x = τ
x
R
(
x))
— vvedenie
∧, 1, 8.
4. Pust~
`R(x) ∼ (x = t).
1) `R
(
x) ∼
(x = t
) — dopuwenie,
2) `
R(x)
→ (x
=
t)
— udalenie ∧
, 1,
3) `
R
(
x
)
odnoznaqno po
x — punkt 2, 3,
4) `
(x = t
) → R
(
x)
— udalenie ∧
, 1,
5) `(∀x
)((
x
= t)
→
R
(
x
))
— vvedenie ∀, 4,
6) `
(
t =
t
) →
R
(
t
) — udalenie ∀, 5,
7)
R
(
t
)
`(
∃
x)
R(x)
— vvedenie
∃
,
8) `
(
∃x)R
(
x) —
E
1
, seqenie, 6, 7,
t. e.
R
(
x
)
funkcional~no po
x.
J
Sootnoxenie
(∃x
)R(
x
)∧
(∀
y
)(∀z
)((R
(y)∧R(
z)) →(y
= z))
, oznaqa-
wee, qto R(
x
) funkcional~no po
x, qasto oboznaqaets simvo-
lom
(∃!
x)
R
(x
), kotory$i qitaets tak: ”suwestvuet edinstvenny$i
(suwestvuet i edinstvenen) predmet tako$i, qto R(x)”. V tom
sluqae term
τ
x
R(x) nazyvaets
opredelennym
opisaniem.
40

Страницы