Составители:
Рубрика:
3.3. Aksiomatiqeskie isqisleni predikatov
Aksiomatiqeskoe postroenie isqisleni predikatov neobho-
dimo prede vsego, dl togo qtoby obobwit~ rezul~taty, po-
luqennye dl koneqnyh predmetnyh mnoestv, na beskoneqnye
predmetnye mnoestva. Rassmotrim snaqala aksiomatiqeskoe is-
qislenie predikatov IP, kotoroe vlets prodoleniem aksi-
omatiqeskogo isqisleni vyskazyvani$i IV i potomu vkl-
qaet v seb vse shemy aksiom i pravilo vyvoda isqisle-
ni vyskazyvani$i IV. Pri tom de$istvi kvantorov v proiz-
vol~nom predmetnom mnoestve opredelts utverdenimi te-
oremy 3.2, printymi kak aksiomy. K pravilu MP
isqisleni
vyskazyvani$i IV dobavlts pravila obobweni i konkreti-
zacii iz teoremy 3.3.
Opredelenie 3.5 (Shemy aksiom i pravila vyvoda IP).
Pust~
A, B, C — predikaty ili vyskazyvani; A(x)
— predikat, so-
derawi$i svobodno x
; peremenna t
svobodna dl x v
A(
x);
D
ne soderit
x svobodno.
Shemami aksiom isqisleni predikatov IP vlts
:
AS
1
A
→
(
B
→ A)
,
AS
2
(A →
B
) → ((
A → (B
→ C
))
→
(A
→ C))
,
AS
3
A → (B
→
A∧B
) ,
AS
4
A∧
B
→ A ,
AS
5
A∧
B → B ,
AS
6
A → A
∨
B ,
AS
7
B → A ∨ B ,
AS
8
(
A
→ C)
→
((B → C)
→
(
A
∨
B → C
)) ,
AS
9
(
A
→ B
)
→
((
A
→
B) → A) ,
AS
10
A → A ,
AS
11
(
∀x)
A(
x) → A(t
) ,
AS
12
A(t
) → (
∃x
)A
(
x
)
.
Pravilami vyvoda isqisleni predikatov IP vlts:
A, A→B
B
(
MP )
,
D
→A
(x)
D
→(∀x)
A(x
)
(
obobwenie)
,
A
(
x)→
D
(
∃x)A(
x)→
D
(
konkre-
tizaci
)
.
Ponti dokazatel~stva i vyvoda iz dopuweni$i analogiq-
ny sootvetstvuwim pontim isqisleni vyskazyvani$i IV,
no oboznaqenie A
1
, . . .
, A
m
`B ispol~zuets tol~ko dl vyvodov,
poluqennyh bez primeneni pravil obobweni i konkretizacii
k peremennym, vhodwim svobodno v dopuweni
A
1
, . . . , A
m
. Vse
34
Страницы
- « первая
- ‹ предыдущая
- …
- 32
- 33
- 34
- 35
- 36
- …
- следующая ›
- последняя »
