Составители:
Рубрика:
Pravila vyvoda i logiqeskie aksiomy IPFP takie e,
kak v IPS, gde t — term, svobodny$i dl x
v A(
x
). K nim
dobavlts aksiomy ravenstva.
Aksiomy ravenstva.
E
1
x =
x ,
E
2
(
x
=
y)
∧
(y
= z) →
(
x
=
z) ,
E
3
(x = y)
→
(
y
=
x) ,
E
P
(x
1
=
y
1
)∧
. . .
∧(x
n
j
= y
n
j
) →
(P
n
j
j
(
x
1
,
. . . , x
n
)
∼ P
n
j
j
(y
1
, . . .
, y
n
)
,
E
f
(x
1
=
y
1
)∧
. . . ∧
(
x
n
j
=
y
n
j
) →
(f
n
j
j
(
x
1
,
. . .
, x
n
) = f
n
j
j
(
y
1
,
. . .
, y
n
)
,
gde
x, x
1
, . . .
, x
n
j
, y, y
1
,
. . .
, y
n
j
, z
— proizvol~nye termy.
Qasto aksiomy ravenstva zapisyvats v zamknutom vi-
de. Naprimer, aksioma E
3
v zamknutom vide zapisyvaets tak
(∀
x
)(∀y
)((
x
=
y
)
→ (y = x))
.
V matematiqeskih vyvodah qasto priments funkcii, na-
zyvaemye opisanimi, sopostavlwie sootnoxenim predmety,
pri kotoryh oni vypolnts. Naprimer, esli v stroke vy-
voda est~ vyskazyvanie
(∃
x
)A(
x), to posle frazy: ”pust~ τ
tako$i predmet, qto vypolnets
A(τ),” sootnoxenie A(τ) zapi-
syvaets v sleduwu stroku vyvoda i vyvod prodolaets,
privod v konce koncov k sootnoxeni, ne soderawemu pred-
meta
τ
. Tako$i sposob vyvoda, ne vyzyvaet vozraeni$i, esli
sno, kak konstruktivno na$iti predmet
τ
dl lbogo
A. Od-
nako, v obwem sluqae pri beskoneqnom predmetnom mnoestve
i beskoneqnom mnoestve sootnoxeni$i vozmonost~ takogo vy-
bora mono postulirovat~ lix~ aksiomo$i vybora
. Cermelo,
kotora, primenitel~no k dannomu sluqa utverdaet, qto dl
seme$istva mnoestv S
(
A) istinnosti sootnoxeni$i
A, sodera-
wih svobodno odnu peremennu
x
, suwestvuet
funkci vybora
τ(
A)
taka, qto τ
(A)
∈
S(A).
Primer. Dokazatel~stvo (∃x)(A(
x)→B(
x)),
(∀x)A(x)
`(
∃x)
B(x
).
1)
`(∃
x
)(A
(x
) → B
(
x
)) — dopuwenie,
2) `
A(
τ
) →
B(τ)
—
τ
tako$i, qto
`A(τ
) → B
(
τ)
,
3)
`(
∀x
)A
(x
)
— dopuwenie,
4)
`
A(τ) — udalenie ∀, 3,
5) `B(
τ) — udalenie →, 4, 2,
6)
`(
∃
x)
B(
x
) — vvedenie ∃
, 5.
Vvedem obwee opredelenie.
38
Страницы
- « первая
- ‹ предыдущая
- …
- 36
- 37
- 38
- 39
- 40
- …
- следующая ›
- последняя »
