Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://www.mccme.ru/free-books/gerasimov-3ed-mccme.pdf Äàòà èçìåíåíèÿ: Mon Aug 22 16:06:34 2011 Äàòà èíäåêñèðîâàíèÿ: Tue Oct 2 00:54:30 2012 Êîäèðîâêà: IBM-866 Ïîèñêîâûå ñëîâà: http www.badastronomy.com bad tv foxapollo.html

. .





,

( PDF-) http://www.mccme.ru/free-books http://gas-teach.narod.ru.

- 2011


510.6+510.2+510.5+512.54.05+004.05 22.12 3 7 . . : . 3- ., . . .: , 2 0 1 1 . 2 8 4 . ISBN 978-5-98709-292-7
. , . , . -. , . . 190 . , , ( ), .

12.01.2011. 60 ½ 84/16. . 25 . . . . 16,7. N 1865. "" 199004, , -, . ., ., . 24, ./: 323-67-74 email: izd_lema@mail.ru

ISBN 978-5-98709-292-7

c . . , 2009, 2010, 2011



1. 1.1. . . . . . . . 1.1.1. . . . . . . . . . . . . . . . . . . . . . 1.1.2. . . . . . . . . . . . . . . . . 1.1.3. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1.4. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2. . . . . . . . . . . . . . . . . . . . . . 1.2.1. . . . . . . . . . . . . 1.2.2. . . . . . . . . . . . . . . . . . . . . . . 1.3. . . . . . . . . 1.3.1. . . . . . . . . . . . . . . . . . 1.3.2. . . . . . . . . . . . . . . . . . 1.3.3. . . . . . . . . 1.3.4. . . . . . . . . . . . . . . . . . . . . 1.3.5. . . . . . . 1.4. . . . . . . . . . . . 1.4.1. 1.4.2. . . . . . . . . . . . . . . . . . 1.4.3. . . . . . . . . . . . 1.4.4. . . . . . . . . . . . . . . . . . . . . 1.5. . . . . . . . . . . 2. 2.1. . . . . . . . . . . . . . . . . . . . 2.1.1. . . . . . . . . . 2.1.2. 2.2. . . . . . . . . . . . . 2.2.1. . . . . . 2.2.2. 2.2.3. , . . . . . . . . . 2.3. . . . . . . . . . . 3 . . . . . . . ... ... ... ... ... ... ... 7 9 11 11 11 13 17

26 31 31 35 35 36 37 38 43 46 48 48 49 53 55 56 60 61 61 63 65 65 68 70 70


4

. . 2.3.1. . 2.3.2. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.6.1. . . . . . . . . . . . . . . . . . 2.6.2. . . . . . . . . . . . . . . . . 2.6.3. . . . . . . . . . . . . . . . . . . . . 2.6.4. . . . . . . . . . . . . . . . . . . . . . 2.7.1. . . . 2.7.2. . . . . . . . . . . . . . . . . . 2.7.3. . . . . . . . . . . . 2.7.4. . . . . . . . . . . . . . . . . . . . . . . . . . . 2.7.5. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. .. .. .. .. .. .. .. .. .. .. .. .. .. . . . . . . . . . . . . . . . . . . . . . . . . . 71 72 74 81 83 83 84 89 95 97 97 101 102 107 108 110 111 113 117 118 119 120 123 124 125 126 126 132 134 136 137 140 140 144 145 147 150 1 1 1 1 1 5 5 5 5 6 1 2 3 5 0

2.4. 2.5. 2.6.

2.7.

3.1. 3.2. 3.3.

3. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3.1. . . . . . . . . . . . . . . . 3.3.2. . . . . . . . 3.3.3. 3.4. . . . . . . . . . . . . . . . . . 3.4.1. . . . 3.4.2. . . . . . . . . . . . . . . . . . . 3.5. - Z F . . . . . . . . 3.5.1. Z F . . . . . . . . . . . . . 3.5.2. Z F . . . . . . . 3.5.3. Z F . . . . . . . . . . . . . . . . . 3.5.4. Z F C . . . . . . . . . . 3.5.5. Z F C

4. 4.1. . . . . . . . . . . . . . . . 4.2. . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.1. 4.2.2. . . . . . . . . . . . . . . . . . . 4.2.3. . . . . . . . . . . . . . . . . . . . . . 4.2.4. . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3.1. . . . . . . . . . . . . . . 4.3.2. . . . . . . . . . . . . . . . . . . 4.4. . . . . . . . . . . . . . . . . . . . . . . . . . 4.4.1. . . . . . . . . . . . . . . . . . . . . .

. 160


4.4.2. 4.4.3. 4.5. 4.5.1. 4.5.2. 4.5.3. . . . . . . . . . . . . . . . . . . . . . . . . . SLD- . . . . . . . . . . . . . . . . . . . . . .. .. .. .. .. . . . . . .

5 163 166 167 168 169 1 74 179 179 180 185 1 87 195 198 200

5. 5.1. . . . . . . . . . . . . . . 5.1.1. . . . . . . . . . . . . . . . . . . . . 5.1.2. . . . . . . . . . . . . . . . . . 5.1.3. - - 5.1.4. . . . . . . . . . . . . 5.1.5. . . . . . . . . . . . . . . . . . . . . . . . . 5.2. . . . . . . . . . . . . 5.2.1. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.2. . 5.2.3. . . . . . . . . . . . . . . . . . . . 5.2.4. . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3. . . . . . . . . . . . . . . . 5.3.1. 5.3.2. . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3.3. . . . . . . . . . . . . . . . . 5.4. . . . . . . . . . . . . . . 5.4.1. . . . . . . . . . . . . . . . 5.4.2. , . . . . . . . . . . . . . . . . . . . . . . 5.4.3. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.4.4. m- m- . . . . . . . . . . . . . . . . 5.4.5. . . . . . . . . . . . . . . . . . . . . 5.5. . . . . . . . . . . . . . . . 5.5.1. . . . . . . . . . . 5.5.2. . . . . . . . . . . . . . . . 5.5.3. . . . . . . . . . . . . . 5.5.4. . . . . . . . . . . . . . . . 6.1. 6.2. 6.3. 6. . . . . .

. . . . . . .

. 200 . 203 . 204 . 205 . 206 . 207 . . . . 2 2 2 2 09 11 12 12

. 213 . . . . . 215 219 224 226 226

. 231 . 233 . 234

241 . . . . . . . . . . . . 241 . . . . . . . . . . . . 242 . . . . . . . . . . . . 24 5


6

. .

. 252 .1. 252 .1.1. . . . . . . . . . . . . . 253 .1.2. . . . . . . . . . . . . . . . . . . . . 254 .1.3. , . . . . 255 .2. . . . . . . . . . . . . . . . . . . . . 258 .2.1. . . . . . . . . . . . . . . . . . . . . . 258 .2.2. . . . . . . . . . . . . . . . . . . . . . . 260 .2.3. . . . . . . . . . . . . . . . . . . . . . . . 262 264 268


:


. , , ( ), . , , , . , , ( ). . , , . , . , , , - . , , , , () , , . , ; , . ; , , Prolog. , . ; . , , , . 7


8

. .

: , . . ( ) , , . , , , , . , . , , . . : , , - ‡. . , , . (, , , , , ), , , , , , - (, Pascal). , . . . . . . - , . . . Email: Alexander.S.Gerasimov@ya.ru



( , , ), . x X x X . , x X , x X . . / {x1 , . . . , xn } , x1 , . . . , xn . {x1 , . . . , xn , . . .}, , . {x X | (x)} x X , (x). , X Y X Y , X Y X \ Y . iI Xi Xi , i I . X Y , X Y . f : X Y , f () X Y . f dom(f ) rng (f ) . X1 ½ . . . ½ Xn ( n 1) X1 , . . . , Xn , . . n- x1 , . . . , xn x1 X1 , . . . , xn Xn . X n n- X , , X n X1 ½ . . . ½ Xn X = X1 = . . . = Xn , . . n- X . N {0, 1, 2, . . .}. {1, 2, . . .} N+ . , , . (, , ) . .

9


10

. .

. ( , .) A, B, , , E , Z, H, , I , K, , M , ² N, , O, , P, , T, , , X, , , o

( ) , . A B C D F G H A B, B C D F G H M N P Q R S Z M N P Q R, R S , S, S Z


1.


, , , . , , . () . : 4 , 5 , , . : 4 5 , , . , . , ; . , ; . ( ) , - ? .

1.1.
, , . , , (, ) , . , , , .

1.1.1.
. 11


12

. .

. , , , . , . , : . , , a1 a2 , , a1 = a2 . . ( , ) , ( ) . , , . a1 , . . . , am , b1 , . . . , bn ( ) , . , a1 . . . am b1 . . . bn ( ) a1 . . . am = b1 . . . bn , m = n ai = bi i = 1, . . . , m. , ( ). , . , , . , ( ), , = . , k , , k - . n N n- . ( ) (k - m-, k < m), , . . . k - , . . , = k . ( ) . 1.1.1. {A, a, B , b, C, c, . . . , Z, z }.1 mathematics 11. 2 ma mathematics: 0- 5-. 5- ma mathematics F GH matheF GH tics. 0 1 , 0-. 2 aba ababa: 0- 2-. . (, .)
1 , , .


1.

13

( ) . 1.1.2. LettersAndDigits {A, a, B , b, C, c, . . . , Z, z , 0, 1, 2, . . . , 9}. Identifiers LettersAndDigits, , {A, a, B , b, C, c, . . . , Z, z }. C lause33, dv g j f 683X itr Identifiers, 73abc . Identifiers : 1) {A, a, B , b, C, c, . . . , Z, z } Identifiers; 2) Identifiers, LettersAndDigits, (. . ) Identifiers. , ( ) . , () . .

1.1.2.
1.1.3. V ars {V |V , V ||V , V |||V , . . .} {V , |}. V ars (, , ). ( ) : 1) ; 2) F T ( ); 3) A B , ìA, (A B ), (A B ) (A B ) . P L ( ).2 , P L {V , |, F, T, (, ), ì, , , }. 1.1.4. V ||V , ìV |V , (ìT V |V ), (ìV |V V |V ), (ì(V |V V ||||V ) V ||V )
2

P L

Propositional Language .


14

. .

. (ìV |V V ||V , (ìV |V - V ||V ), (ìV |V Z ), ìV |V V ||V . 1.1.5. , , , V |V V ||V , V | V ||. , V | (V | V ||) A, (A A|). , , V |V (V |V V ||V ) A (A V ||V ). , . , p, q , r, , . , : p, p1 , pf , pf2 , q0 , r, r2007 . , , : p3 , ìp, ((p q ) p). , , , . , A, B , C , D, E G (, ) , . ì ( ), ( ), ( ) ( ) ( ). , , . ( , .) , : 1) ìA A , A , , A ; A B , A B ;

2) (A B )

3) (A B ) A B ( , ), A B ; 4) (A B ) A B , A, B , B , A , A, () B , A B , A B , B A , B A , B A , A () B , A () B , A B , B A , A B , B A . , C P . 1) : P ;


1.

15

2) : ( ) , A B P , , ìA, (A B ), (A B ) (A B ) P . C , P L. , , C ( ) . . C P [C ]. , C P [C ], C . . C , , P [C ], C 0 0 . . , A P [A], B P [B ]. P [ìA] , ìA A , P [A] . P [(A B )] , (A B ) A B , P [A] P [B ] . P [(A B )] P [(A B )]. 1.1.6. , . , P L, ( ) P L, , : 1) p F [p], Q F [Q]; 2) , A B F [A] F [B ], F [ìA], F [(A B )], F [(A B )] F [(A B )]. A F [A]. 1.1.7. A l[A] ( , P L): 1) l[A] = 0, A ; 2) l[ìA] = l[A] + 1, l[(A B )] = l[A] + l[B ] + 1, A, B , , , . , l[A] A. ( ), . A B . (A B ) ((A B ) (B A)). (A B ) : A,


16

. .

B , A , B , A B , A B , A B . : ( , , ), , . , , , . : (A B ) ((A B ) (B A)). , , , . , A, A. . -, . , (p ìq ) p ìq . -, , . , ((A B ) C ) (A B C ), . , p ((q (r ìp)) r) p (q (r ìp) r). -, , , , , . , , , (. . ). ((A B ) C ) (A B C ), (A (B C )) (A B C ). , ((p q ) r) p (p q r) p, (p (q r)) p (p q r) p. 1.1.8. ((((p ìq ) r) ì(p q ))) p ìq r ì(p q ), . , ìp p , p q ìp p q , (ìp p) q . ìp , ì(p q ) ìp q r , (ìp q ) r . ì , ì. 1.1.9. .


1.

17

1.1.3. .
, - (). , , P L , . : , , , . : , , , (). : pu ( ) , pf , pr , A. , pf , pr pu , , , . . A . , pf pr , pu , , , . . A . , , , , , A (ìpf (pf pr)) pu, pf , pr pu . A, , pf pr , ìpf pf . , , , , A, , A . ‡ . , , 1 ( ). , , 0 ( ). {0, 1} ( ) B. , , . 1.1.10. ( ) P L M : V ars B, p M (p). , , A B . , ìA, (A B ), (A B ) (A B ). Fì B B F , F , F B2 B , . 1.1. ()


18

. .

( ) , , . , 0 0 1 1 0 1 0 1 F (, ) 0 0 0 1 F (, ) 0 1 1 1 F (, ) 1 1 0 1

0 1

Fì () 1 0

. 1.1. , Fì , F , F F . ìA, (A B ), (A B ) (A B ) Fì (), F (, ), F (, ) F (, ) . 1.1.11. F , A B , A B ; : A B , , A (B , ). , , A B . , k : k 5, k 2 . k , , . k = 1 ; k = 3 ; , . , F . . 1.1.12. M P L. A A M . |A|M ( |A|, , ). |A|M 3 : 1) A , |A|M = M (A); 2) A F, |A|M = 0; 3) A T, |A|M = 1; 4) A ìB , |A|M = Fì (|B |M ); 5) A (B C ), |A|M = F (|B |M , |C |M ); 6) A (B C ), |A|M = F (|B |M , |C |M );
3 P L (. 1.1.2). .


1. 7) A (B C ), |A|M = F (|B |M , |C |M ).

19

|A|M = 1, , A () M , M A. |A|M = 0, , A () M , M A. , , , , . 1.1.13. A ((p q ) p). M1 . M1 (p) = 0, M1 (q ) = 1. p q , M1 (r) = 1 r V ars \ {p, q }. |A| = F (|p q |, |p|) = F (F (|p|, |q |), |p|) = F (F (M1 (p), M1 (q )), M1 (p)) = F (F (0, 1), 0) = F (1, 0) = 0, , M1 A. M2 , M2 (r) = 1 r, M2 (p q ) M2 p, M2 A. , . , , . , p (p q ) , , , p q , , p, : p q . . 1.1.14. , , ( , ). , A , A. , , . , A , A. , , ( ). , , ( ). 1.1.15. p (p q ) , . ì(p (p q )) , . p q , . , , A . A , A , 1.1.12. A n ,


20

. .

. , (, 2n ) . , , . , . p1 , . . . , pn , n > 0, A , p1 , . . . , pn ( , A ). A , 1.1. () , 2n , 1 , . . . , n A M , M (p1 ) = 1 , . . . , M (pn ) = n . (, = |A|M M , , .) p1 ... 1 ... . . . . . . . . . . . . pn ... n ... A ... ...

1.1. . 1.1.16. p q 1.2. p 0 0 1 1 q 0 1 0 1 pq 1 0 0 1

1.2. p q . 1.1.17. (. 1.3) ì(p q ) (ìp ìq ) , 1, , . , ( ) ( ), . . : 1) (p q ) (q p); 2) ((p q ) r) (p (q r)).


1.

21

p 0 0 1 1

q 0 1 0 1

ì(p q ) 1 1 1 0

ìp ìq 1 1 1 0

ì(p q ) (ìp ìq ) 1 1 1 1

1.3. ì(p q ) (ìp ìq ).

: 3) (p q ) (q p); 4) ((p q ) r) (p (q r)). : 5) (p (q r)) ((p q ) (p r)); 6) (p (q r)) ((p q ) (p r)). : 7) (p (p q )) p; 8) (p (p q )) p. : 9) ì(p q ) (ìp ìq ); 10) ì(p q ) (ìp ìq ). : 11) p ìp. : 12) p ììp. : 13) (p q ) (ìq ìp). : 14) ìp (p q ). : 15) (p q ) (ìp q ). 1.1.18. 1í15, .


22

. .

p, G2 qA (p q ). . , , G1 , , G1 G2 , A. , A {G1 , G2 }. , . 1.1.19. A ( ) ( A), M : G M G, M A. , A, A. , A. A G1 , . . . , Gn A, G1 , . . . , Gn A , () G1 , A G1 , . . . , Gn . . . , Gn . A A ,

1.1.20. , p p q , p q, r p r p, p q q . p p q ( , p , q ). 1.1.21 ( ). G1 , . . . , Gn (n N+ ), A . G1 , . . . , Gn A, G1 . . . Gn A. . G1 . . . Gn A , (a) M M (G1 . . . Gn ) A. (a) (b): M , M G1 . . . Gn , M A. , (b) : M , G {G1 , . . . , Gn } M G, M A, . . ( ) G1 , . . . , Gn A. A ì(p q ) B (ìp ìq ). ( 1.3 . 21) , A B . , . , . 1.1.22. A B ( ), M : M A , M B (, , |A|M = |B |M ). , A B , A B . , A B , (A B ) .


1.

23

A B , A B B A . , A A (. . ); A B B A (. . ); A B B C A C (. . ); , . , 1í15, . , . , , p (p q ). p , , (ìq r). (ìq r) ((ìq r) q ). , . , , ( ) . . . p1 , . . . , pn ; A, B1 , . . . , Bn ; {B1 /p1 , . . . , Bn /pn } ( , , , - / ). , A p1 , . . . , pn A B1 , . . . , Bn . A: 1 ) pi Bi i = 1, . . . , n;

2) A , p1 , . . . , pn , A A; 3) A ìC , A 4) A (C A (C D). ìC , C C ; , , ,

D),

1.1.23. A , A . ( : , A p1 , . . . , pn A B1 , . . . , Bn .) , , . A - , . , . , , , A , . , -


24

. .

, . A . A , ( ) 1) A, A ; 2) ì, A ìC , C ; 3) , A C D ( , , ), C D . , ìp (p q ) : ì p p q.

, A , . A. , , . 1.1.24. A (p (p q r)). A{(ìq r)/p, ìr1 /q , ìq /r2 } (ìq r) ((ìq r) ìr1 r). 1.1.25 ( ). p1 , . . . , pn , A, B1 , . . . , Bn , {B1 /p1 , . . . , Bn /pn }. A, A . . M P L. M , M (pi ) = |Bi |M i = 1, . . . , n M (q ) = M (q ) q V ars \ {p1 , . . . , pn }. , E |E |M = |E |M , , E A, |A|M = |A|M = 1. M , A, . , , E |E |M = |E |M . E . . E . E pi i = 1, . . . , n, |E |M = |pi |M = |Bi |M = M (pi ) = |E |M .


1.

25

E V ars \ {p1 , . . . , pn } , |E |M = |E |M = |E |M . . , C D . E ìC . |E |M = |ìC |M , C C . |C |M = |C |M . , |E |M = Fì (|C |M ) = Fì (|C |M ) = |E |M . , E (C D), , , . |E |M = |C D|M . |C |M = |C |M |D|M = |D|M . , |E |M = F (|C |M , |D|M ) = F (|C |M , |D|M ) = |E |M .

1.1.26. p1 , . . . , pn , A, B1 , . . . , Bn , C , {B1 /p1 , . . . , Bn /pn }. A C , A C . . A C . (A C ), 1.1.25 (A C ) . (A C ) (A C ), , (A C ) A C , . , . , ì(p q ) (ìp ìq ), , (ìp ì(p q ) ) r (ìp (ìp ìq ) ) r. . , . 1.1.27 ( ). A, B B , A B A B . B B , A A . 1.1.28. :
A A

ì(p q ) (ìp ìq ) (ìp ì(p q ) ) r (ìp (ìp ìq ) ) r .
B B B B

1.1.29. , A.


26

. .

1.1.4. . .
n N+ Bn B n- . A, p1 , . . . , pn , f (p1 , . . . , pn ), A. , 1 , . . . , n B f (1 , . . . , n ) = |A|M , M , M (p1 ) = 1 , . . . , M (pn ) = n (, f (1 , . . . , n ) M ). , A f (p1 , . . . , pn ), , , A f (p1 , . . . , pn ). 1.1.30. ìp1 Fì (p1 ), f (p1 , p2 ) = Fì (p1 ). p1 ìp2 g (p1 , p2 ) = F (p1 , Fì (p2 )). 1.1.31. f (p1 , . . . , pn ) A, f . . f , 1.4. . p1 0 0 1 1 p2 0 1 0 1 f (p1 , p2 ) 1 0 0 1

1.4. , f . A, , f . 1 f , , . 4 1.4 (ìp1 ìp2 ), (p1 p2 ). A : (ìp1 ìp2 ) (p1 p2 ). f , f ; f , , (p1 ìp1 ). f , ‡ f ; f , , (p1 ìp1 ). A, , f .
4

.


1.

27

0 f , , . 1.4 (p1 ìp2 ), (ìp1 p2 ). A : (p1 ìp2 ) (ìp1 p2 ). , , , . 1.1.32. A1 , . . . , An (n 1) . A1 . . . An A1 , . . . , An . A1 . . . An A1 , . . . , An . Ai (i = 1, . . . , n) (, ). . 1.1.33. . , , . ( ). 1.1.34. : p, ìp, ìp q , p ìq , (p ìq ) (ìp r p) ìq , . 1.1.35. . , , . ( ). 1.1.36. : p, ìp, ìp q , p ìq , (p ìq ) (ìp r p) ìq . , B A, A B . 1.1.37. (, ) A , (, ) A. 1.1.38. , 1.4 1.1.31 A (p1 p2 ). (ìp1 ìp2 ) (p1 p2 ) (p1 ìp2 ) (ìp1 p2 ) , , A. 1.1.31 . 1.1.39. ( ) , , , .


28

. .

1.1.40. , , . . 1.1.41. , , : , . 1.1.42. , , , . . | : (A | B ) ì(A B ) (A B ) ì(A B ). 1.1.43. , : (a) ì , (b) ì , (c) |, (d) . . 1.1.39 C , ì, . (a) , C , ì . (, 5 ) C . . 0 C . . . , C , n, . C n + 1 . , (p q ) ì(ìp ìq ); 1.1.26 (A B ) ì(ìA ìB ) A B . C (A B ) ì(ìA ìB ). C . 1.1.27 C C . C n . C , C , ì , C C . , C C . , C , (a) . , A B : (b) (A B ) ì(ìA ìB ); (c) ìA (A | A), (A B ) ì(A | B ); (d) ìA (A A), (A B ) ì(A B ).
5 k N. , , P (n) n k ,

1) : P (k ); 2) : n k ( ) P (n) P (n + 1).


1.

29

(b), (c) (d) , (a). 1.1.44. (a) . , , . (a) : , (A B ) ì(ìA ìB ), , C (A B ) ì(ìA ìB ), , C ì . 1.1.45. , , ì . 1.1.46. 1.1.39 , , ì, . : Fì , F F . , f (p1 , p2 ) (ìp1 ìp2 ) (p1 p2 ), f (p1 , p2 ) F (F (Fì (p1 ), Fì (p2 )), F (p1 , p2 )). 1.1.47. , , F| (p1 , p2 ) F (p1 , p2 ), (p1 | p2 ) (p1 p2 ) , F , , F . . ? F 0 1 (. . F (, ) = = 0 = 1 )? , 0 1? ( ) 2, Z2 . , Z2 0 1; + § : 0 + 0 = 0, 0 + 1 = 1, 1 + 0 = 1, 1 + 1 = 0, 0 § 0 = 0, 0 § 1 = 0, 1 § 0 = 0, 1 § 1 = 1. x1 , . . . , xn Z2 a
{i1 ,...,im }{1,2,...,n} {i1 ,...,im } xi1

. . . xim ,

{i1 , . . . , im } {1, 2, . . . , n}, a{i1 ,...,im } Z2 , , , . x Z2 n N+ xn = x ( , ). P (x1 , . . . , xn ) Z2 P (x1 , . . . , xn ), . . x1 , . . . , xn Z2 P (x1 , . . . , xn ) = P (x1 , . . . , xn ). 0 1 Z2 0 1 . ,


30

. .

, . . . 1.1.46 Fì , F F . . , Fì (q ) = q + 1, F (q1 , q2 ) = q1 § q2 . , q1 q2 ì(ìq1 ìq2 ), F (q1 , q2 ) = Fì (F (Fì (q1 ), Fì (q2 ))) = (q1 + 1) § (q2 + 1) + 1 = q1 § q2 + q1 + q2 . , . 1.1.48. , 1.4 . 26. : D (ìp1 ìp2 ) (p1 p2 ).

(p1 p2 ) p1 § p2 ( p1 p2 ); (ìp1 ìp2 ) (p1 + 1) § (p2 + 1) = p1 § p2 + p1 + p2 + 1. , D (p1 § p2 + p1 + p2 + 1) § p1 § p2 + (p1 § p2 + p1 + p2 + 1) + p1 § p2 = p1 + p2 + 1.

1.1.49. , , . . n- n . , . . f . f (. ., , 0 1). , f , , f . , f F , 0, f 0, 1. . Fì , F F (. 1.1.46), : Fì , F F . : . , , , , .


1.

31

1.2.
, , () , ( ). 1.2.1. , , ( ). , , , , , . f , , , , f1 f2 , f1 f2 . , (x ) = x-1 . (f1 ) = g1 (f2 ) = g2 (f1 + f2 ) = g1 + g2 (f1 ) = g1 ; (f2 ) = g2 . (f1 + f2 ) = g1 + g2 (x5 ) = 5x4 (x6 ) = 6x5 (x5 + x6 ) = 5x4 + 6x5 . , (x7 ) = 7x6 (x5 + x6 + x7 ) = 5x4 + 6x5 + 7x6 . , , , , , () , . ( ) , ( , ) .

1.2.1.
, L . , ( ) C , Ax L R, L. Ax C . R C . C , L C , , C ( L). , C L, C C (L). R , (n + 1)- , n N+ . 1 , . . . , n , R, , ( ) 1 , . . . , n R, R 1 , . . . , n . i (i = 1, . . . , n)


32

. .

, () . , (n + 1)- , n- . n- : A1 ; . . . ; An , A A1 , . . . , An , A . , ; , . , . ( , , 1 , . . . , n , , 1 , . . . , n .) ( ) C 1 , 2 , . . . , k , i (i = 1, 2, . . . , k ) C C i1 , . . . , in , i1 , . . . , in i. ( , , : ). k . , , , L , ( , ). , {, }. C 1 , . . . , k , k . C , C ( C ) C . C , C C . C C , , . : , , , . ( , .) 1.2.2. { a , b } L . , , , , . x1 . . . xn ( xi i = 1, . . . , n) , n > 0 j = 1, . . . , n xj = xn+1-j . P al, , , L . : 1) a, 2) b, 3) aa 4) bb.


1. P al : (a), a a (b), b b

33

L. . (a) (, (b)) a a (, b b). P al . abababa P al , ( ): b , ab a, b ab ab , ab ab ab a . : 1) b 2; ()

2) aba 1 (a); 3) babab 2 (b); 4) abababa 3 (a). , L : , . . . , . . P al. (, 6 ) , . . 1. . , , . . , , , n (n > 1), . n . , , , . (a) (b). = a a = b b. . , . . . , . . 1 2. , , a, b, aa bb. , .
6 k N. , , P (n) n k , , n k ( ) P (k ), P (k + 1), . . . , P (n - 1) P (n) ( , n = k P (k )). , P (n) n . , ( ).


34

. .

. , , n (n > 2), . n. , , x x, x , , . . x = a x = b, (a) (b) x x. , . . , P al , . , , , , : , c c L, c . , , a, aaa , a, bab . ( 1.2.2.) 1.2.3. , , , . . ( , , , . , , , .) - , , , () . , () L 1.2.2 P al. ( ) . , ( ). (, ) , ; , ( ) .7 ( ). , ( P al), - ( ). , , .
7 , ( , ), 3.3.3, 3.5.5, 2.5.7, 2.6.23 5.1.5. , , . , , .


1.

35

- , .

1.2.2.
. . P al , , ab, . ab, babb, aaba, baabab. , P al, , ab , , ab . , . C L, L. C , , C . . . C 1 , . . . , k , k . , C C , C . C , C C . C C , , . , . , C . { } , . 1 , . . . , n , 1 , . . . , n . 1.2.4. 1.2.2 baabab {ab, bbba} P al: 1 ) ab ;

2) aaba 1 (a); 3) baabab 2 (b).

1.3.
, . -


36

. .

, .

1.3.1.
, P L . H. H , : 1) A (B A), 2) (A (B C )) ((A B ) (A C )), 3) A (B A B ), 4) A B A, 5) A B B , 6) (A C ) ((B C ) (A B C )), 7) A A B , 8) B A B , 9) (A B ) ((A ìB ) ìA), 10) ììA A, 11) F A, 12) A T, A, B , C . , 1í12 ; A, B C . H , (mo dus ponens, M P ), , A A B B , A B . : A; A B . B , . , , 8 : B , A B . : A , A B , B . , . H P L


1.

37

, . 1.3.1. A A ( A ): 1) A ((A A) A) 1; 2;

2) (A ((A A) A)) ((A (A A)) (A A))

3) (A (A A)) (A A) 1 2 M P ; 4) A (A A) 1;

5) A A 4 3 M P .

1.3.2.
P L . . P L , , . , , . , , : . , H , , . 1.3.2. P L , ( ), , . , . H . , . 1.3.3 ( H). , A . A, A. . A. . A. A . , H : , ,


38

. .

, , 1.1.25 . , A , A, , A. A , . . A , A. . , , , n (n > 1). A n. , A , . , A B B A M P . B B A, B B A. , , A. 1.3.4. , A . A, A. . 1.3.3 A A A. A.

1.3.5 ( H). H , . . A, A, A. . 1.3.3, , A A, A A. 1.3.6. H , . . A , A ìA. . A, A ìA, A ìA, .

1.3.3. .
A B : , A, B . H . 1.3.7 ( H). , A, B . , A B , A B . . , A B , A B , M P A B , A A. , , A B A B . , A B .


1.

39

. B . 3 : (a) B , (b) B A, (c) B . . (a) M P B (B ) B (A B ) ( 1) A B . , A B . (b) 1.3.1 A A, , A A, . . A B ( B A ). (c) M P B (B ) B (A B ) ( 1) A B . . , , n (n > 1). , A B n. (a), (b), (c), B M P C C B . , A C , A C B , () A C () A (C B ). M P () 2 (A (C B )) ((A C ) (A B )) (A C ) (A B ). () M P A B . , 1.3 (, ) , . H , , . . 1.3.1, . . , H (. . , ). , . . 1.3.7 : AB , A B , . AB , A B : , A B , A B . , . (, , - ). : A B , , A B . , A A B , M P B . , A; B AB ,

(, , - ).


40

. .

( ), . : , , , . 1.3.8. , A, B C (A B ) ((B C ) (A C )). - AB (B C ) (A C ).

, , - A B, B C A C.

- A B , B C, A ( ) - A B, B C , A B C, C. ()

(. ), A B , B C, A B , () . ( ) - A B , B C, A , A B , B C, A A. A B,

, . : 1) (A B ) ((B C ) (A C )) 2 -; (B C ) (A C ) 3 -; A C 4 -; C 5, 6 -; B C ; B 7, 8 -; A B ;

2) A B

3) A B , B C

4) A B , B C , A 5) A B , B C , A 6) A B , B C , A 7) A B , B C , A


1.

41

ì

- , A B , AB , A A; B ; , A ìA B , AB B , AB ìB ,

- A; ììA , A AB , A AB , B B AB ,

A , AB

, A C ; , B C . , A B C

1.6. H .

8) A B , B C , A

A .

1.5, .
1

A1 ;

...; A

n

An

,

n N+ .

()

( ) ( H) , : 1 A1 ; . . . ; n An A. , , , , . , 1.5 . . - - . ì- , A B , A ìB . () A B () A ìB . M P 9 (A B ) ((A ìB ) ìA) () (A ìB ) ìA. () M P ìA, . ì- : ììA 10 ììA A M P A. , - : A, B 3 A (B (A B )), M P , A B . , -, : A B 4 A B A M P A; , A B 5 A B B M P B . , -, : A 7 A A B M P A B ; , B 8 B A B M P A B .


42

. .

, , - . , A C , B C A C B C . 6 (A C ) ((B C ) (A B C )), M P , A B C . M P A B A B (, , ) A B C , , A B C . , , , . , ì- , ( , ): ìA, A , . . B B ìB . - : , A B C , , A C , B C . 1.3.9. , A B ìA (A B ). ( A, ìA B : .) , 1.3.8: 1) ìA (A B ) 2 -; A B 3 -; B 4 ì-; ììB 5, 6 ì-; A ; ìA .

2) ìA

3) ìA, A 4) ìA, A

5) ìA, A, ìB 6) ìA, A, ìB

1.3.10. , , , :
1

A; 2 , A B . 1 2 B

1.3.11. , , -, : A B; , A C ; C , B C .

1.3.12. , , -, : , A, B C . , A B C


1. 1.3.13. , : , A B ; , B AB A , AB , , A B AB . , B A

43

1.3.14. , 1.1.3.

1.3.4.
1.3.2 H: H . : H. , . 1.3.15. , A , A ìA. . 1.3.16. , A A ìA. . 1.3.17. . P L , , . , , ( ). 1.3.18. , , . . M . G M G. , A A ìA. 1.3.3 H M A M ìA, . . 1.3.19, . 1.3.19. . 1.3.19 , . p : (1) p, (2) ìp (3) p ìp. , . . M , . 1.3.3 H (1)


44

. .

M p, (2) M ìp , , M p. (3) , p. M , , : (3) . , , M , , . 1.3.20. , A . {A} {ìA} . . , {A} {ìA} . B C , , A B , , A ìB , ìA C , , ìA ìC . ì- (. . 41) , A B , A ìB ìA. , ìA C , ìA ìC ììA. , ìA ììA, . . 1.3.21 ( ). . . , P L . A1 , A2 , . . . , . 0 . i N+ i . i-1 {Ai } , i i-1 {Ai }. ( i-1 {ìAi } 1.3.20) i i-1 {ìAi }. i N i . iN i . . A A, ìA, . , , . , A , A ìA. , , j , j A j ìA, j . , . 1.3.19. 1.3.21 , , . p p, ìp, . , , , 1.3.3 H, p , . M P L, p 1, p, 0 (. . ìp).


1.

45

, M , , A M A , A. A. . A . A , M . A F, M F F ( F 11 M P , ). A T, M T T ( T M P 12). . , B C . 1. A ìB . M A , M B . M B B . : B , ìB , . . A. 2. A B C . M A , M B M C . M B M C , B C . B , C - B C . , B C - B C . , B C , B C , . . A. 3 (A B C ) 4 (A B C ) 2 . 1.3.22. 3 4 . 1.3.23 ( ). . , . . . , . 1.3.19 , . . A , A ìA. 0 , 0 A 0 ìA. , 0 . 1.3.18 0 , 0 . , , . 1.3.24 ( H). , A . A, A. . , , , B ì- ììA, A, {ìA} 1.3.19 . , , ìA B , ìA ìB . ì- A.


46

. .

1.3.25 ( H). H, . . A, A, A. . . , H , . 1.3.26. H . 1. , A B A A, B A, ìB ìA, B ìA, ìB ììA, A B, ì(A B ), ì(A B ), ì(A B ), ìA A, B A, ìB ìA, B ìA, ìB ìA, A B, A B, A B, ì(A B ),

A, B A, ìB ìA, B ìA, ìB

A B, ì(A B ), A B, A B.

2. A , p1 , . . . , pn . , M p1 , . . . , pn A, B B , M B , ìB . ( 1.) 3. A , p1 , . . . , pn . , p1 ìp1 , . . . , pn ìpn A. H.

1.3.5.
H : . , , H, . , . A H : A , , A M P , , , , M P , . . , M P , , M P , . H . H .


1.

47

: , , , , , , , . . . , C . C , ( ), A A, A C ( , A C ). ( C ) : ( ), A 1, A C . , 0, , . ( , , , 0 .) , 1 0 ; 1 , , , , 0 , , , . . H : A , A, . H. , . . , H, . H ( ) : (, )8 , . ; , . , , . H, , H, . 8 H , .


48

. .

, , ; . 1.3.27. H. ( , , , .)

1.4.
, , , , , .

1.4.1.





, P L , . M A, M A. , . 1.4.1. - A ì(p q ) (ìp r).

, A , M . A M , ì(p q ) M (ìp r) M . , M , , M . : ì(p q ) (ìp r) ì(p q ) (ìp r). : ì(p q ) (ìp r) (ìp r), (p q ). , (ìp r), (p q ), (a) (ìp r), p (b) (ìp r), q ; , : (a), (b). , . , (a). (ìp r), p ìp, r, p, p r, p. , : p M . (b) : (ìp r), q ìp, r, q , p r, q . p r, q M : M (p) = 1, M (r) = 0, M (q ) = 0, M ,


1.

49

0. , A, . , A : p r, p p r, q ìp, r, p ìp, r, q (ìp r), p (ìp r), q (ìp r), (p q ) ì(p q ) (ìp r) . ì(p q ) (ìp r) 1.4.2. ì(p q ) (ìp ìq ) : q ìp, q p ìq , p ìp, ìq , p ìp, ìq , q (ìp ìq ), p (ìp ìq ), q (ìp ìq ), (p q ) ì(p q ) (ìp ìq ) . ì(p q ) (ìp ìq ) p ìq , p, , p ( -), q ìp, q , , q . , , . , , , : , , , . , 1.4.2.

1.4.2.
, , , , . G . A1 , . . . , Am B1 , . . . , Bn , A1 , . . . , Am , B1 , . . . , Bn , m, n N. A1 , . . . , Am ( m = 0) . B1 , . . . , Bn ( n = 0)


50

. .

. Ai (i = 1, . . . , m) . Bj (j = 1, . . . , n) . . P L S , S S . S A1 , . . . , Am B1 , . . . , Bn M : M M S (

(S ) , S , (S ). S ) (S )

A1 . . . Am B1 . . . Bn ,

, (, ) T (, F). S (S ). , m > 0 n > 0 S : A1 , . . . , Am B1 , . . . , Bn . m = 0 n > 0 : B1 , . . . , Bn . m > 0 n = 0 : A1 , . . . , Am . S , (S ) . , , . G : , , A, B . G : , A (ì ), , ìA , A, B ( ), , A B , A ; , B ( ), , A B , A; , B (), , A B , A ( ì), , ìA , A; , B ( ), , A B , A, B ( ), , A B , A , B (). , A B

. : , . . : , . .


1.

51

, , , . 1.4.1 . , M : M - , M . , , , , A; , B , A B M . , M , A B , M , A B , . M : A B , A B . M , A B , M , A , B . G : , A , A; , F ; , T. , , , , , . , G . 1.4.3. , . , , , () , : 1 , 2 1 , A, 2 ; 1 , B , 2 1 , 2 , 1 , A B , 2 1 , 2 : 1 , A, 2 1 , A, 2 , i , i (i = 1, 2) , A, B . , . G ; , (. 1.2), G . G . A ( G ) A. A ( G ), A .


52

. .

, , , , , . , (. 1.3.5). S ( , ) S , . 1.4.4. ì(p q ) (ìp ìq ) G . ( 1.4.2.) ì(p q ) (ìp ìq ). 1) ì(p q ) (ìp ìq ) 2 (); 2) ì(p q ) (ìp ìq ) 3 (ì ); 3) (ìp ìq ), (p q ) 4 5 ( ); 4) (ìp ìq ), p 6 ( ); 5) (ìp ìq ), q 8 ( ); 6) ìp, ìq , p 7 ( ì); 7) p ìq , p ;

8) ìp, ìq , q 9 ( ì); 9) q ìp, q .

, 1 ( ) , 9, 8, . . . , 2, 1 1. S , S , - S . . . , ( ) , S , (a) S , (b) S S - S . (b) : S S , S . . S ( , S ), S . 1.4.5. ì(p q ) (ìp ìq ) 1.4.2. , , .


1.

53

, ( 1.4.2 1.4.4). 1.4.6. . . 1.4.7. ( ) , 1.1.3, , 1.3.1.

1.4.3.
1.4.8. G ; , . . , . . , , . , , . . 1.4.9 ( G ). G . . , , . , , . , . . . , 1.4.8. . , , , n (n > 1), . n. S ( S ), R. R, S , . 1.4.8 S R. , S . 1.4.10. , G .


54

. .

1.4.11. G , . . A , A ìA . . A, A ìA , A ìA, . 1.4.12. S , . S , S . . , S , 1 0, (S ) , . S.

1.4.13 ( G ). G . . S . ( ), S , . S , 1.4.8 ( ). 1.4.12 . , . , S . 1.4.14. , G . (. 1.4.10.) , , . 1.4.15. S . S , - Sl , Sl , Sl . . 1.4.12 Sl . 1.4.8 S . G S . 1.4.16. ì(p q ) (ìp r) 1.4.1. 1) ì(p q ) (ìp r) 2 (); 2) ì(p q ) (ìp r) 3 (ì ); 3) (ìp r), (p q ) 4 ( );


1. 4) ìp, r, (p q ) 5 ( ì); 5) p r, (p q ) 6 7 ( ); 6) p r, p ;

55

7) p r, q . 7 , 1.4.15 1 ( ) . 1 : p r, p p r, q p r, (p q ) ìp, r, (p q ) (ìp r), (p q ) ì(p q ) (ìp r) . ì(p q ) (ìp r) , ( 1.4.1), . 1.4.17. , , G . , . ( G S (S ) , (S ) , . , G , .) , G : G , , . G H. G : , .

1.4.4.
, , . , (A B ) ((A B ) (B A)), . ( ), , (A B ) (B A) G :


56

. . 1) , (A B ) (B A) 2 3 ( ); 2) , A B 4 (); 3) , B A 5 (); 4) , A , B ; 5) , B , A.

, , A , B , B , A, , A B . ( G ) , A , B ; , B , A (), , A B (). G (. . ). ( G ) R ( ), S1 , . . . , Sn , S R, S1 , . . . , Sn S . , 1.2.1. () . , 1.2.1. 5, 4, 3, 2, 1 () . , (), : , A, B ; , A, B (). , A B , () (), G , , 1.4.8. 1.4.18. , .

1.5.
, , . ( ). , , . , .


1.

57

A (ìp q ) p ìq . , A , . . M , M A. : (ìp q ), p q . , (ìp q ) p A, A q M q . , ìq A, A ìq M ìq . : M q M ìq . A . . : , , . , , . . A ìA, A ìA. 1.1.39 , A1 . . . An , Ai (i = 1, . . . , n) . , Ai , Ai . {A1 , . . . , An }, , . , . , . 1.5 . . , . . 1.5.1. , . 1.5.2. C1 ) L1 , L2 , L1 L2 . C1 C2 (C1 \ {L1 ( C2 }) (C2 \ {L2 }).

, . 9 , . , ( ). , , p ìp ( p
9

1.1.35 . 27 .


58

. .

) , p ìp . 1.5.3. ìp q p q . ìq q . p ìq ìr q r p ìr r, p ìq q . ìp q ìp r . 1.5.4. . . C1 C1 {p}, C2 C2 {ìp}, C1 C2 . , M , M C1 M C2 , M C1 C2 . , M p M ìp. . 1. M p. M ìp, M C2 M C2 , M C1 C2 . 2. M ìp. M p, M C1 M C1 , M C1 C2 . , M C1 C2 . 1.5.5. C , S . C S , S , C . , C S , S , , . . , . 1.5.6 ( ). S . S , S . . S : C1 , . . . , Ck , Ck . , S , . . M S . 1.5.4 i = 1, . . . , k Ci M , Ck . S . 1.5.7. : 1) p q , 2) ìp q ,


1. 3) p ìq , 4) ìp ìq . : 5) q 6) ìq 7) 1 2, 3 4, 5 6.

59

7 , . S S . : , , S , , S . , . . , . (. 4 4.4.17). , ( ) . , ?

, . - ( ), . : . , P L . : , ( ). , , , , . , , .


2.


( , , ) ( , ). , x , y x y , N , xy R(x, y ), R(x, y ) x y . xy R(x, y ) , , R(x, y ) x y . R(x, y ) y x , . , y R(x, y ), N R(x, y ) x y , , x. x 0, , x 2, . , , : x , y x y N. xy R(f (x), y ), R(z , y ) z y , f (x) x. . , . . P (z ) , z P . x P (x), y , P (y ) , , P . xP (x) y P (y ). P . , . , , , . , , 60


2. , .

61

2.1.
, .

2.1.1.
; . 2.1.1. P S, F S, # , P S , F S (, ) , # P S F S N, P S F S = . P S 1 . , P, p, Q, q , R, r, , . (, : P, P add, p1 , Q0 , r, Rxy z2007 .) P #(P ) ( ). 0- . F S 2 . , a, b, c, f , g , h, . (, : a, f , f y , f y1 , g2007 .) f #(f ) ( ). 0- ( ) . 2.1.2. , . I V () V ars, 1.1.3. I V 3 ( ) , I V . , u, v , w, x, y , z , . (, : v ar, x, z0 , x1 , y2007 , z2008 .)
1 2 3

PS FS IV

Predicate Symbols . Function Symbols . Individual Variables .


62

. .

2.1.3. . . , , . P S, F S, # , F OL(P S, F S, #).4 , . F OL(P S, F S, #). 2.1.4. : 1) F S ; 2) f n- F S , n > 0, t1 , . . . , tn , f (t1 , . . . , tn ) . t1 , . . . , tn f (t1 , . . . , tn ) f . 2.1.5. : 1) P S F T ; 2) P n- P S , n > 0, t1 , . . . , tn , P (t1 , . . . , tn ) . t1 , . . . , tn P (t1 , . . . , tn ) P . 2.1.6. : 1) ; 2) A B , x , ìA, (A B ), (A B ), (A B ), xA xA . , , , , . ( ) ( ) . , . xA, xA, ìA, (A B ),
4

F OL

First-Order Language .


2. 2.1.7. F OL(P S, F S, #) , 1) P S = {P }, #(P ) = 2, . . P P S, F S, #

63

,

2) F S = {a, f , g }, #(a) = 0, #(f ) = 1, #(g ) = 2, . . a ( ), f g . , , 1) x, y , z , 2) a, 3) -: f (a), g (f (y ), a). , , 1) : T, P (a, a), P (x, y ), P (f (a), g (f (y ), a)), 2) , : ìP (x, y ), ìP (f (x), y ) z P (y , g (a, z )). z P (y , g (x, z )), g (x, y ),

(, ) (, ) (, ) , (. 1.1.2). , 1.1.2 . , , , . , , , , , . , , . , , s t (, ) , A, B , C , D, E G (, ) , .

2.1.2.
, . t , t .


64

. .

A , A . x ; x ( x) , x . (, ) A. (, ) A, (, ). ( , .) 2.1.8. ìxP (x, y ) z Q(f (x), z , x) . (, , ì, , .) ìx(P (x, y ) z Q(f (x), z , x)) . x A , xB xB , A ( , x x). x , . x A, x ( ) A. A B V (A).5 x A ( A), x ( ) A. A F V (A).6 2.1.9. x y , z , A ìxP (x, y ) z Q(f (x), z , x)

, , F V (A) = {y , x}, B V (A) = {x, z }. 2.1.10. , .
5 6

BV FV

Bound Variables . Free Variables .


2.

65

k - x A. , k - x ( ), k -. 2.1.11. x z , ìx(P (x, y ) x Q(f (x), z , x)) x x, x x. , , ( ). , , ( ). A , x1 , . . . , xn A, ( ) A. ( n = 0 A) x1 . . . xn A A ( A A ) A. A ( A), A. , , .

2.2.
, ( ) . , . , .

2.2.1.
. , , , D , . D, n- D. n- , . .


66

. .

2.2.1. X n N+ . X n n- X . , n N+ X1 , . . . , Xn . X1 ½ . . . ½ Xn n- X1 ½ . . . ½ Xn . 2.2.2. n- R, X1 ½ . . . ½ Xn , n- R, R(x1 , . . . , xn ) , x1 , . . . , xn R, . , n- R X1 ½ . . . ½ Xn n- { x1 , . . . , xn X1 ½ . . . ½ Xn | R(x1 , . . . , xn ) }. , , . 2.2.3. ( ) F OL(P S, F S, #) D, ² , 1) D , ; 2) ² , ) n- P S n > 0 n- D, n = 0 ; ) n- F S n > 0 Dn D, n = 0 D. P S, F S, # . 2.2.4. (, ), (, ) . 2.2.5. , R, A y R(x, y ), x y . : N, R R(x, y ), x y . , , A , x . , , . , .


2.

67

D, ² M 2.2.1. 2.2.6. M I V D . M .

2.2.7. t t M . |t|M , . |t|M , : 1) t , |t|M 2) t , |t|M 3) t f (t1 , . . . , tn ), |t|M
, , ,

= (t);

= ²(t);

= ²(f )(|t1 |M , , . . . , |tn |M , ).

t , , , , |t|M , |t|M . 2.2.8. X Y , X Y , x x X Y . x X Y , (z ) = (z ) z X \ {x} x x (x) = . ( , x .) 2.2.9. A A M . |A|M , . |A|M , : 1) A F, |A|M
, ,

= 0; = 1;
,

2) A T, |A|M

3) A , |A|M 4) A P (t1 , . . . , tn ), |A|M , = ²(P )(|t1 |M , , . . . , |tn |M , ); 5) A ìB , |A|M , = Fì (|B |M , ) (Fì , . 1.1.3);

= ²(A);

-

6) A (B C ), |A|M , = F (|B |M , , |C |M , ), , , (F , . 1.1.3); 7) A xB , |A|M , = 1 , x D |B |M , = 1; 8) A xB , |A|M , = 1 , x D , |B |M , = 1.


68

. .

|A|M , = 1, , A M ( () M ), M , A. |A|M , = 0, , A M ( () M ), M , A. , , . A , , , , |A|M , |A|M , M , A M A, M , A M A. A M , M , A . M A.

2.2.2.
, P t1 t2 , P (t1 , t2 ) (t1 P t2 ) t1 P t2 . , f (t1 , t2 ) (t1 f t2 ) , , t1 f t2 . . 2.2.2 , -. Ar . 0, S , + § =. , Ar w = (x, +(§(y , z ), w)), w(x = (y § z ) + w). , , St S (t). , § , +. w(x = y § z + w). D, ² Ar: D {0, 1, 2, . . .}, N; 0 0 (, ²(0) 0); S (, ²(S ) ); + § (²(+) ²(§) ); = , (²(=) ). Ar.


2.

69

Ar: x (x) y y |x z (y = x + z ), z (x = y § z ),

ì(x = S 0) y (y |x y = S 0 y = x).

, (x) = 6 (y ) = 2, , y |x. , (x) = 6 (y ) = 5, , y |x. Ar: ; ( ). xy (x + y = 0), . - - = . , z (z x z y ) y ì(y x). x y x = . . N N. = , . x = y x z y z ( ), x(x x) . ( ) § =. xy z ((x § y ) § z = x § (y § z )) () § . , : z (x(x § z = x z § x = x) xy (x § y = z y § x = z )). : (1) ; (2) ; (3) , ; ()


70

. .

(4) ; (5) . (1), (2), (3) () (). (4), (5) () ().

2.2.3. ,
2.2.3 , . Ar, x y z (y = x + z ) . x y . Ar , x y (x) (y ) x y . , (x) (y ), . , x y ( ) x y , N2 x y . , . 2.2.10. M D. n- D; x1 , . . . , xn ; A , . , A (x1 , . . . , xn ) M , |A|M , = ( (x1 ), . . . , (xn )). 2.2.11. Ar . z (y = x + S z ) z (y = x + z ) ì(x = y ) x y , y x. y |x (x) (. 2.2.2) y x x . ev en1 (x) ev en2 (x, y ) x . z (x = z § S S 0) z (x = z + z ). ‡ 2.2.12. Ar, : 1) z x y , 2) z x y , y , 3) x .

2.3.
2.3 , -.


2.

71

, , z (y = x + z ) Ar, x y . Ar. le2(u, z ) u z Ar, , z (y = x + z ) le(x, y ) x y . I. le2(u, z ) Ar, u x z + z y z (y = x + z ): z (z + z = u + z ). , ! - , , , z z + z , . , , , . , . Ar le2(u, v ) u v , , z (v + v = u + z ), . , , , . I I. . 2.2.9 , , z ( ) (. . ) w. ( 2.3.2) z . , le2(u, z ) Ar z z (y = x + z ) w. w(y = x + w), u x z + z y . w(z + z = u + w), le2(u, z ).

2.3.1. .
.


72

. .

2.3.1. t x A [A]x t t x A. 2.3.2. E
x [E ]g( w ,y )

xP (x, y ) z Q(f (x), z , x).

xP (x, y ) z Q(f (g (w, y )), z , g (w, y )).

[xP (x, y )]x xP (x, y ). w 2.3.3. , t x A, x A , t. , t x A . 2.3.4. E , . x g (w, y ) x E . z , g (z , y ) x E . 2.3 , , . 2.3.5. .

2.3.2. .
. . , , ; . 2.3.6. A A, , , , , , ( , ) , . 2.3.7. A B ( A B ), A B k , i = 1, . . . , k : 1) i- A , i- B ; 2) i- A , i- B ;


2.

73

3) i- A , , 7 j - , i- B , , j - B . A B , , B A. 2.3.8. : ìx(P (x, y ) xQ(f (x), z , x)), ìu(P (u, y ) xQ(f (x), z , x)), ìu(P (u, y ) v Q(f (v ), z , v )).

2.3.9. . 2.3.10. , A A (. . ); A B B A (. . ); A B B C A C (. . ); , . 2.3.11. , A , B V (A) F V (A) = A . , , , . 2.3.12. xP (x, y ) z Q(z ) , xP (x, y ) xQ(x) xP (x, y ) y Q(y ) . 2.3.13 ( ). A V A , A , A A B V (A ) V = . . A. . A . A A. . , C D. A ìC . C , , C C B V (C ) V = . A ìC . A (C D), , , . V V F V (D).
7 (, ) , .


74

. .

C , , V F V (C ) B V (C ). C C B V (C ) V = . V D , , D D B V (D ) V = . A (C D ). , A QxC , Q . y , A V . C , x , [C ]y C B V (C ) (V {y }) = . A Qy C . 2.3.14. () () , . . . 2.3.15. A . A [A ]x t , t í , x , A A t x A . t x A [[A]]x . t

2.3.16. [[xP (f (x), y , x)]]y (x) f z P (f (z ), f (x), z ), v P (f (v ), f (x), v ). 2.3.13 2.3.15 A (, A , B V (A ) , t). [[A]]x A . , t [[A]]x , t , A , . . 2.3.10, . , , A A t x A A , [A ]x [A ]x . , t t . , 2.4 2.6.4, .

2.4.
( ), . (. 2.1.1), , . 2.4.1. , , ( , ). , A , A.


2.

75

, , . , A , A. , , ( ). , , ( ). , . , , . 2.4.2. A ( ) ( A), M : G M , G, M , A. , A, A. , A , A. G1 , . . . , Gn A {G1 , . . . , Gn } A, G1 , . . . , Gn A {G1 , . . . , Gn } A. 1.1.21 . 2.4.3 ( ). G1 , . . . , Gn (n N+ ), A . G1 , . . . , Gn A, G1 . . . Gn A. () , : (A B ) ((A B ) (B A)). 2.4.4. A B ( ), M : M , A , M , B . , A B , A B . (A B ) , A B , . , , , .

2.4.5. , A x ìxA xìA. () , () , M D, ² : (1) M , (2) M , ìxA, M , xìA, M , xìA; ìxA.


76

. .

(1) M , ìxA. ì , M , xA. : , D x x M , A. , D , M , A. ì D x , M , ìA, , , M , xìA. (2) , M , xìA M , ìxA, (1) . 2.4.6. , A B x xA xB x(A B ). , , M D, ² : M , xA xB , M , x(A B ). M , xA xB . M , xA M , xB . : x D M , A D x x M , B . , D M , A x M , B . , x , D M , A B . M , x(A B ). 2.4.7. , x(P (x) Q(x)) xP (x) xQ(x) , P Q . M D, ² , , . . M , x(P (x) Q(x)) M , xP (x) xQ(x). , M . D {d, e}. ²(P ) , ²(P )(d) = 1, ²(P )(e) = 0. ²(Q) , ²(Q)(d) = 0, ²(Q)(e) = 1. , . , : , P Q . 2.4.8. , . , . 2.4 A B ( 2.1.1), x y ; A, B , x y . 2 . 1. ìxA xìA.


2. 2. ìxA xìA.

77

3í10 , x A. . 3. A xB x(A B ). 4. A xB x(A B ). 5. A xB x(A B ). 6. A xB x(A B ). 7. A xB x(A B ). 8. A xB x(A B ). 9. xB A x(B A). 10. xB A x(B A). x A. 11. xA xB x(A B ). 12. xA xB x(A B ). 13. 14. xA xB x(A B ). x(A B ) xA xB .

15í16 y A. 15. xA y [A]x . y 16. xA y [A]x . y 17. A B , A B . (. . .) 18. t x A, 19. t x A, xA [A]x . t [A]x xA. t

20. A B , t x A B , [A]x [B ]x . t t 2.4.9. C , p1 , . . . , pn C , B1 , . . . , Bn . , p1 , . . . , pn C B1 , . . . , Bn , C . 2.4.10 ( ). .


78

. . q p q ,

2.4.11.

ìxQ(x, y ) R(y ) R(z ) ìxQ(x, y ). . : , () , , , . -

2.4.12 ( ). A, B B , A B A B . B B , A A . 2.4.13. : ìxQ(x, y ) xìQ(x, y )
B B A A



y (P (x, y ) ìxQ(x, y ) ) y (P (x, y ) xìQ(x, y ) ) .
B B

2.4.14. , 2í12, 14í18 20, 2.4.10 2.4.12. - , ? . , . . 19, . 2.4.15. t x A, [A]x xA. t . t x s [s]x . t 2.4.16. s, t , x , M , . |[s]x |M , = |s|M , x . t
|t|M ,

D, ²

-

. s. . s .


2.

79

s , . x, |[s]x |M , = |s|M , = |s|M , x t s x, |[s]x |M t
|t|M , ,

= |t|M

,

= |x|M

. , s1 , . . . , sn , s. s f (s1 , . . . , sn ). |[si ]x |M , = |si |M , x t i = 1, . . . , n. |[s]x |M t
, |t|M ,

, x |t|M ,

= |s|M

, x |t|M ,

.

= |[f (s1 , . . . , sn )]x |M t
x 1 ]t |M ,

,

= |f ([s1 ]x , . . . , [sn ]x )|M t t
, x |t|M ,

,

=
, x |t|M ,

²(f )(|[s

, . . . , |[s

x n ]t |M ,

) = ²(f )(|s1 |M

, . . . , |sn |M
, x |t|M ,

)= .

|f (s1 , . . . , sn )|M

= |s|M

, x |t|M ,

. 2.4.17. A , x , t , x A, M D, ² , . |[A]x |M , = |A|M , x . t
|t|M ,

. A. . A . A , |[A]x |M , = |A|M , = |A|M , x . t A P (s1 , . . . , sn ). 2.4.16 x i = 1, . . . , n |[si ]t |M , = |si |M , x . |[A]x |M t
, |t|M ,

= |A|M

, 2.4.16. . , B C , A. 1. A ìB . , , , |[B ]x |M , = |B |M , x t
|t|M ,

, x |t|M ,

,

|t|M ,

|[A]x |M t

,

= |[ìB ]x |M t

,

= |ì[B ]x |M t Fì (|B |M

,

, |t|M ,

= Fì (|[B ]x |M , ) = t x ) = |ìB |M , x

|t|M ,

= |A|M

, x |t|M ,

,

Fì (. 1.1.3). 2í4. 2í4, A B C , B C B C , 1. 5. A y B . x A, .


80

. .

x A, x y , |[A]x |M , = |[y B ]x |M , = |y [B ]x |M , . () t t t
x , |y [B ]t |M , = 1, D x |[B ]t |M , y = 1.

|[B ]x |M t

y ,

= |B |M ,( y )x |t|

.
y M ,

(

)

t x A ( y B ), y t, |t|M , y = |t|M , . , x y ; , y y yx . ( ) , ( )x | y = ( )|t| = |x| |t t
M , M , M ,

|[B ]x |M t |y [B |B |
M, x |t|M ,

y ,

= |B |

y

M, x |t|M ,

.

]x |M , = 1, t y = 1.


D = |y B |M = |A|M ,

x |y [B ]t |M

,

, x |t|M ,

, x |t|M ,

( ) . 6. , A y B , 5. 2.4.15. [A]x xA, M D, ² t , , M , [A]x , , M , xA. t M , xA , D x , , |A|M , = 1. 2.4.17 |[A]x |M , = |A|M , x t |[A]x |M , t = 1, |t|M , .
|t|M ,

2.4.18. . A ; B1 , . . . , Bn A , ; p1 , . . . , pn ; A , A Bi pi (i = 1, . . . , n). A , A . ( : , . . 2.4.10.) : (P (x) P (y )) (P (y ) R(z )) (P (x) R(z )), (px py ) (py r) (px r),


2.

81

, .

2.5.
2.5.1. , A ( ) , A Q1 x1 . . . Qn xn B , n 0, Qi i = 1, . . . , n, B . A ( ). B A. A ( A) B , , A B. 2.5.2. A xP (x) xQ(x). (. 2.4), A1 x(P (x) xQ(x)), A. A1 , x x y : A2 x(P (x) y Q(y )), A1 . xy (P (x) Q(y )), A2 , , A. , xy (P (x) Q(y )) A. 2.5.3. A B A. . A. . A . B A. . , C D. A ìC . C Q1 x1 . . . Qn xn E , Qi i = 1, . . . , n, E . B Q1 x1 . . . Qn xn ìE , . A (C D), , . E F C D . 2.3.13 , B V (E ) F V (F ) = B V (F ) (F V (E ) B V (E )) = . , , (E F ) A. , A QxC , Q . E C . B QxE .


82

. .

2.5.4. , . 2.5.5. . , . 2.5.6. A x(y P (y ) (ìz Q(z ) y R(x, y ))),

, . :8 A xy (P (y ) (ìz Q(z ) y R(x, y ))) xy (P (y ) (z ìQ(z ) y R(x, y ))) xy (P (y ) z (ìQ(z ) y R(x, y ))) xy z (P (y ) (ìQ(z ) y R(x, y ))) xy z (P (y ) y (ìQ(z ) R(x, y ))) xy z (P (y ) y1 (ìQ(z ) R(x, y1 ))) xy z y1 (P (y ) (ìQ(z ) R(x, y1 ))).

2.5.7. 2.5.3 (), () , . , 9 . 2.3.13 ; () , , () . , , () , , , 2.4.5 . : , D A; c, D , A. , . , , , . .
8 A B C ( A, B C ) : A B B C . . ‡ 9 , .


2.

83

2.6.
, .

2.6.1.
(. 1.3.2). . , , : , . , 2.4, : . , , : , -, , -, . . , H(). H() , : , H (. 1í12 1.3.1), A, B C ; 13) xA [A]x ; t 14) [A]x xA; t 15) x(B A) (B xA); 16) x(A B ) (xA B ). 13í16 A B ; x , B ; t , x A. H() (, , M P ) ( Gen)10 : A; A B (M P ), B A (Gen), xA

A, B , x .
10

Ge n

Gener aliz ation .


84

. .

H() . 1.3.1. : A, , , x, , x A. , H() H : H() . H, H() A A A . , A A H() H (. 1.3.1). 2.6.1. xA y [A]x , A y , x y , y A.
y 1) [[A]x ]x y [A]x 14 ( y y , [[A]x ]y A, y A); yx

2) x(A y [A]x ) 1 Gen; y 3) x(A y [A]x ) (xA y [A]x ) y y y [A]x ); y 16 (x -

4) xA y [A]x 2 3 M P . y 2.6.2. , y [A]x xA, y
x xA y [A]y ,

y [A]x xA, y

A , x y , y A. y A ? 2.6.3. , H() 15 16 : BA , B xA AB , xA B

A, B ; x , B . , H() .

2.6.2. . . .
. , .


2.

85

2.6.2 . , P . P (x) Gen xP (x), P (x) xP (x) ( , P (x) xP (x)). 1.3.3 H ( - ) H(). - , , Gen, , . H() , (. 1.2.2). . H() , , , M P , xA A Gen, x - . , , , , xA A Gen x . , , , x. H() , (, ) H(), H() , 1.2.2. , A (, ) H() ( 2.6.2 ), H() A , , A (, H() A A). 2.6.4 ( H()). , A . A, A. 1.3.3 A. 2.4 , H() . , A xB B Gen, x . M D, ² , G M , G. , M , xB . D. x x , G M , G. -


86

. .
x

B B . M , D, M , xB .

B .

3 2.6.4 , (. 1.3.2). 2.6.5. , A . A, A. 2.6.6 ( H()). H() , . . A, A, A. 2.6.7. H() , . . A , A ìA. . , 1.3.7 H H(): P (x) Gen xP (x), P (x) xP (x) . , , , H() , . . . H() . 2.6.8 ( H()). , A B . , A B , A B . 1.3.7 , A B . , B xC C Gen, x {A}. , A C A C , Gen x(A C ). 15 x(A C ) (A xC ) M P A xC . , 2.6.2 . H() , 1.3.3. H() H , 1.3.3. , , 1.5 . 41, . , H(). , H(), H ( -, ) H().


2.

87

H() , : [A]x y (-), xA [A]x t (-), xA xA (-), [A]x t B (-), B

, [A]x y , xA

1) - y ( ) x A {xA}, 2) - - t x A, 3) - y x A {xA, B }. , - : xA y , [A]x . - y ( C Choice ): , xA B , y x x, A xA, , [A]y B . , - : [A]x y Gen y [A]x . 2.6.2 y y [A]x xA. y [A]x M P y y xA. - : xA 13 xA [A]x t M P [A]x . t 2.6.9. - -. 2.6.10. , , -, : xA; , [A]x y B B ,

y x A {xA, B }. 2.6.11. , xìA ìxA, A , x . (. 1.3.3), , : 1) xìA ìxA 2 -;

2) xìA ìxA 3 - ( y x); 3) ìA ìxA 4, 5 ì-;


88

. . 4) ìA, xA 5) ìA, xA 6) ìA, xA A 6 -; ìA ; xA .

. 2.6.12. H() . . B p1 , . . . , pn C B1 , . . . , Bn (. 2.4.9 . 77). 1.3.25 H, C H. p1 , . . . , pn B1 , . . . , Bn , . , C H B H(). 2.6.12 . , ìA B , ìB A ( A B ). , (ìA B ) (ìB A) , , 2.6.12 . ìA B M P ìB A, . ( H()) ìA B , ìB A ()

. 2.6.8 ìA B , ìA B , ìB A , ìB A, () , ìA B , , ìB A . , , A , B ìB , ìA , A , ìB B , ìA , ìA , B ìB , A



.

2.6.13. , A x ìxA xìA.


2. 1) ìxA xìA 2 -; xìA 3 ; xA 4 -; A 5 ;

89

2) ìxA 3) ìxìA 4) ìxìA 5) ìA 6) ìA

xìA 6 -; ìA .

2.6.14. 2.4 1í12 . , , . , , 13, 14 . 2.6.15. ( 2.6.3.) , A , G1 , . . . , Gn , G1 , . . . , Gn A. (a)

2.6.8 (a) G1 (G2 (. . . (Gn A) . . .)), (. ) G1 . . . Gn A. 2.6.8 (c) G1 . . . Gn A. (c) (b)

2.6.16. (b) (c) . . 2.6.12.

2.6.3.
, 2.6.3, . H(): . (. 2.6.21 ). 2.6.21 1.3.19. . 2.6.17. , A , A ìA. .


90

. .

2.6.18. , A A ìA. . 2.6.19. . , , . , , ( ).

1.3.18 2.6.4 H(). 2.6.20. , , . 2.6.21, 2.6.20.

2.6.21 ( ). . , . 2.6.22. , A . {A} {ìA} . 1.3.20, 2.6.23. , {A} {ìA} . B C , , A B , , A ìB , ìA C , , ìA ìC . ì- , A B , A ìB ìA. , ìA C , ìA ìC ììA. , ìA ììA, . . 2.6.23. (. 2.5.7 .) () . ( , , B ìB .) , 2.6.22 : , {A} {ìA} . , 2.6.22 . , . 2.6.22 , {A} {ìA} . , , ? ( ì-), {A} ìA. , ìA


2.

91

{A}. , , {A} , , ìA . , , , , , . 5.5.2 ( ), . 2.6.24 ( ). . . 1.3.21 , 2.6.22, , . 2.6.25. F OL(P S, F S, #); ; xA ; xA; c , P S F S ; c F OL(P S, F S {c}, #c ), #c (c) = 0 (. . c c ) #c # P S F S . {[A]x } c . c . , {[A]x } c , . . B c , , [A]x B c , [A]x ìB . ì- ì[A]x , c c ì[A]x H(c ). c c ( ) z , ì[A]x H(). ì[A]x z z (. 2.6.15 . 89) 0 , ì[A]x , z 0 , z . ì[A]x [A]x ì . - z [A]x ì . z z z ìz [A]x . , z ìz [A]x . z xA, (. 2.6.1 . 84) z [A]x . , z x ìz [A]z z [A]x , z . , {[A]x } c . 2.6.26. , xA , xA, t, [A]x . t 2.6.27. F OL(P S, F S, #); . C S , P S F S , , ,


92

. .

C S F OL(P S, F S C S, #C S ), #C S 0 C S (. . C S C S ) #C S # P S F S . . , xA, , . xi Ai (i I ) , I = {1, 2, . . . , k } k N I = N+ . C S (1) {c1 , c2 , . . .} , P S F S . ( , C S .) (1) 0 i I
(1) i



(1) i-1

{[Ai ]xii }. c

2.6.25 i I i (1) (1) F OL(P S, F S C Si , #C S (1) ), i CS
(1) i
i

(1)

{c1 , . . . , ci }, #C
(1) i (1) I (1) 0

S

(1) i

#C S ,

C S
(1) I

C S . , (iI
(1) i



).


(1)

F OL(P S, F S C S

(1)

, #(1) ),

#(1) #C S , C S (1) C S . (1) I , (1) (1) A (1) , I H((1) ) ìA. , H((1) ) A I I , i, (1) (1) i H((1) ) ìA. H((1) ) A i C S (1) \ C Si , A (1) (1) i (1) ìA , (1) A i H( ) H ( ) i . I . 2.6.24 (1) (1) (1) (1) , I . , I , (1) . (1) (1) , (2) (2) , (1) . , j N+ (j ) (j ) , . j N+ (j ) . , C S , C S j N+ C S (j ) C S .
(1)
i

(1)

(1)

(1)

i


2.

93

C S . . , (1) , I , . , C S (j ) j , (j ) (j ) . , xA C S , H(C S ) xA, (j ) j , c C S [A]x (j +1) . c 2.6.21. , , F OL(P S, F S, #) , , F S . M D, ² . D ( , , ). n- f F S (n > 0) ²(f ) , t1 , . . . , tn D ²(f )(t1 , . . . , tn ) = f (t1 , . . . , tn ); 0- f ²(f ) = f . n- P P S (n > 0) ²(P ) , t1 , . . . , tn D ²(P )(t1 , . . . , tn ) = 1, P (t1 , . . . , tn ), ²(P )(t1 , . . . , tn ) = 0 (. . ìP (t1 , . . . , tn )). ²(P ) 0- P : ²(P ) = 1, P , ²(P ) = 0 . , () M , , A : M A , A. A. ( A ) 1í4, A (ì, , , ), , 1.3.19. 5í6, A . 5. A xB . xB , t , [B ]x . t M [B ]x , M xB . t M xB , t , M [B ]x . t [B ]x . t 14 [B ]x xB M P xB . t 6. , , A xB . xB , t 13 xB [B ]x xB M P t [B ]x . M [B ]x t t t, M xB . M xB . , xB . ìxB . (. 2.6.13 . 88) xìB . t , [ìB ]x . , t ,


94

. .

M [ìB ]x . , M [B ]x , M xB . t t , xB , xB . 2.6.21 , . 2.6.28 ( ). . 2.6.29 ( -). - , . . 2.6.20 , , . 2.6.28 . 3 2.6.21 1.3.23, 1.3.24 1.3.25. 2.6.30 ( ( )). . , . 2.6.31 ( H()). , A . A, A. ( 1.3.24), A . , A , . 2.6.32. , A . , ) A A; ) A A. 2.6.33 ( H()). H(), . . A, A, A. 2.6.34. , , ? 2.6.35. , , ? . A A1 A2 < xy z (x < y y < z x < z ), xì(x < x), A3 xy (x < y ), ì(A1 A2 A3 ),

.


2.

95

2.6.4.
2.6.1 . , () . , (). . , , , . 11 . A B ( ), A B . A B A B . A B , A B (A B ) (B A). 1.3.13 . 43, A B , A B B A. . 2.6.36. , . , A B : A B , A B . : A B , A B . . , 2.4.12 . 2.6.37 ( ). A, B B , A B A B . B B , A A . , , , , , . -

2.6.38. A, B C , x . A B , (1) ìA (2) A C (3) A C ìB , B C, C A B C, C A C B, C B,

11 . 2.6.4 , , 3, .


96

. . B C, C A xB , xB . C B,

(4) A C (5) xA (6) xA

. (1) (A B ) (ìA ìB ) , , 2.6.12 . M P A B , , ìA ìB . , ìA ìB . (, , . , ìA ìB A B , . 1.3.3 2.6.2.) (2)í(6) . 2.6.39. (2)í(6) 2.6.38. 2.6.37. B B . , A A , A. . A . B A, B A , A A . . , C D, A. A, ìC . B A, ( ). B C . A ìC , C B C B . C C . , 2.6.38 A A . A, C D. B A, . A A B C D. B C . A C D, C B C B . C C . , 2.6.38 A A. , A C D, C D, xC xC , . , . 2.6.40. , , . . 2.6.1, 2.6.2 2.6.37. 2.6.41. , , A , A.


2.

97

: x y z (y = x + z ). , - x y , , : u z + z . (. 2.3), z z (y = x + z ) , x y . , (. 2.3.2). , , , , (. 17 2.4). , , , , (. 2.6.40). , , .

2.7.
1.3.5 H H() ( ). H() , , , , . H H() , . , . . , , , (. 1.4). , , .

2.7.1.
A , , A . , M , A, M , A. , .


98

. .

2.7.1. - , D, ² , M xP (x) Q(z ) x(P (x) Q(z )). , , , , , . xP (x) Q(z ) x(P (x) Q(z )), xP (x) Q(z ) x(P (x) Q(z )). x(P (x) Q(z )) M ; , P (y1 ) Q(z ), y1 (. . ) , M , y1 . , x(P (x) Q(z )), , P (y1 ) Q(z ), . , x(P (x) Q(z )) , P (y1 ) Q(z ), y1 , . , xP (x) Q(z ) P (y1 ) Q(z ), xP (x) Q(z ) P (y1 ), Q(z ). , xP (x) P (y1 ), Q(z ) Q(z ) P (y1 ), Q(z ),

. Q(z ) P (y1 ), Q(z ) , Q(z ), , . xP (x) P (y1 ), Q(z ). , , : xP (x), , P (y2 ), . , ()

, y2 ()

P (y2 ) P (y1 ), Q(z ).


2.

99

, y2 , - (): , , xP (x) , , , (). , y1 y2 , P (y1 ) P (y1 ), Q(z ) . y2 , y2 (). , () , M = D, ² . D {y1 , y2 , z }. , () = D . ²(P ) ²(Q) () (, , ): ²(P )(y2 ) = 1, ²(P )(y1 ) = 0, ²(Q)(z ) = 0.

M . : P (y2 ) P (y1 ), Q(z ) xP (x) P (y1 ), Q(z ) Q(z ) P (y1 ), Q(z ) xP (x) Q(z ) P (y1 ), Q(z ) xP (x) Q(z ) P (y1 ) Q(z ) xP (x) Q(z ) x(P (x) Q(z )) . xP (x) Q(z ) x(P (x) Q(z )) 2.7.2. - xP (f (x)) Q(z ) x(P (x) Q(x)). : E x(P (x) Q(x)). xP (f (x)) Q(z ) E , xP (f (x)) Q(z ) E , , , xP (f (x)) E Q(z ) E .

. Q(z ) E . ( ) E x(P (x) Q(x)) P (t1 ) Q(t1 ), t1 ( , t1 ,


100 . . Q(z ) E ). P (t1 ) Q(t1 ) t1 , , E , E . E , E P (t1 ) Q(t1 ) . , Q(z ) E , P (t1 ) Q(t1 ), , t1 . t1 , . Q(z ) E , P (t1 ), Q(t1 ). , t1 z Q(z ) E , P (z ), Q(z ), , (Q(z ) ). : xP (f (x)) E . xP (f (x)) xP (f (x)) P (f (t2 )), t2 . t2 . , xP (f (x)), P (f (t2 )) E . , E , xP (f (x)), P (f (t2 )) E , P (t3 ) Q(t3 ), t3 , . , , xP (f (x)), P (f (t2 )) E , P (t3 ), Q(t3 ). () t2 t3 , ( ) . , t2 , , u, t3 f (u). , . , . : xP (f (x)), P (f (t2 )) E , P (t3 ), Q(t3 ) Q(z ) E , P (t1 ), Q(t1 ) xP (f (x)), P (f (t2 )) E , P (t3 ) Q(t3 ) xP (f (x)), P (f (t2 )) E Q(z ) E , P (t1 ) Q(t1 ) xP (f (x)) E Q(z ) E xP (f (x)) Q(z ) E . xP (f (x)) Q(z ) E , : . .


2.

101

2.7.2.
, 2.7 . G (), . , S (S ), . 1.4.2, . , S , , S S . , (, ), (, ) . G () . , (. 1.4.2), , , A, B . , . G () : , xA, [A]x t ( ), , xA , [A]x y ( ), , xA , [A]x y ( ), , xA , xA, [A]x t ( ). , xA

x ; t , x A; y , x A ( ) ( ). G (). : . : . G () -, , , - . ( ) ( ) y . G () , , , , A .


102 . . , , (. 1.4.2). 2.7.3. 2.7.2: A xP (f (x)) Q(z ) E , E x(P (x) Q(x)).

1) xP (f (x)) Q(z ) E 2 (); 2) xP (f (x)) Q(z ) E ( ); 3 4

3) xP (f (x)) E 7 ( ); 4) Q(z ) E 5 ( ); 5) Q(z ) E , P (z ) Q(z ) 6 ( ); 6) Q(z ) E , P (z ), Q(z ) ;

7) xP (f (x)), P (f (u)) E 8 ( ); 8) xP (f (x)), P (f (u)) E , P (f (u)) Q(f (u)) 9 ( ); 9) xP (f (x)), P (f (u)) E , P (f (u)), Q(f (u)) .

, A , 9, 8, . . . , 1 . . , 2.7.2, , A, t1 , t2 , t3 , . t1 , t2 , t3 z , u, f (u) , . ( ) ( ) ( t) . , ( , ). 2.7.5. 2.7.4. ( ) , 2.6.14 . 89.

2.7.3.
, (. 1.4.3); 2.7.5, 2.7.6. 2.7.5. G () ; , .


2.

103

2.7.6. 2.7.5 . . 2.4.17. 2.7.7 ( G ()). G () . 2.7.8. G () , . . A , A ìA . 2.7.9. , , ( ) ( ). . ( .) (, ) , . 2.7.10 ( G ()). S0 , . S0 , S0 G (). 2.7.11. (. 2.3.11). , xP (x, y ) xQ(x) , . 2.7.12. C S1 S2 , S1 S2 S1 S2 , - . , xP (x) Q(x), y R(y ) uP (u) v R(v ), Q(x), , . 2.3.13 (, ) (, ). , () , G () . 2.7.10. , S0 , , S0 , S0 . , , . , 0- . S0 , , , , . :


104 . . (1) S0 .

(2) T erms , S0 . T erms = , T erms , S0 . (3) . (3.1) , , , . (3.2) , , , . (3.3) ( ), S S . (3.4) S C S ( ). C S . (3.5) C , S C , () S - . . (3.6) C S C , C S C , (3.6.1) y , y T erms / y ; (3.6.2) ( ) , , ( ) S C , y ; (3.6.3) S - ; (3.6.4) T erms y . (3.7) (. . C S C , C S C ) t T erms :


2.

105

(3.7.1) ( ) , , ( ) S C , , t, t ; (3.7.2) Sl S - ; (3.7.3) , C Sl , S (3.7.1), S Sl . , S0 . S0 . (3.1), S0 . : (3.2) . (3.2), 12 , . , , . , , . , (, , ). , B r, . S0 . (, ) (, ) B r. , F, T: B r , . M D , ² . D , , - T erms . a D ²(a) = a; b ²(b) . n P (n > 0) ²(P ) , t1 , . . . , tn D ²(P )(t1 , . . . , tn ) = 1, P (t1 , . . . , tn ) , ²(P )(t1 , . . . , tn ) = 0. 12 T T (, i = 0, 1, . . . , k - 1 Si ,

. ( ) S0 , S1 , . . . , Sk S0 , S1 , . . .) , S0 T , (, i = 0, 1, . . .) Si+1 Sk T .


106 . . ²(P ) 0- P : ²(P ) = 1, P , ²(P ) = 0. , (x) = x x D ; z ²(z ) . , M S0 , : F , F , M , F , F , M , F . F . ( F ) M . . , F , n. F n + 1 . F xA. F , [A]x y y D. M , [A]x . y , M , xA. x F , [A]t t D . M , [A]x t t D. , M , xA. , F ìA, A B , A B , A B xA . 2.7.13. , 2.7.10. 2.7.14. 2.7.10 2.7.1 2.7.2, x(P (x) ìP (x)), xQ(x).

2.7.15. A 2.6.35 . 94. A 2.7.10 . . 2.7.10 G (). S0 S0 , S0 ; S0 , . 2.7.16. , , 2.7.10. . : ; ( ), ; ( ) ( ).


2.

107

2.7.17. 2.7.10 , . . 2.7.10 , , , ( ) ( ) . ( ) . 2.7.18. ( ), .

2.7.4.
G () , H() , , A : A H() , A G (). , A H(), G () A. , , , , G (). ( G () G , 1.4.4.) : , A ; , A , , , A , . , ( , , , , ). , . - . G () . , - , ( ). , , . . , , G () , . , (. 1.3.5). (


108 . . ) , . 2.7.5. 2.7.19. , 2.7.8 ( 2.7.7).

2.7.5.
1.4.3 . , ( ) ( ), , - . , - , ( ) ( ), , , . ( ) ( ) ( t), . , , P (f (z )) xP (x), : P (f (z )) xP (x), P (f (z )), P (z ) P (f (z )) xP (x), P (z ) . P (f (z )) xP (x) ( ) z , f (z ) , . , , , , , . , ( ) ( ). . . , ( ) ( ) , , . , . , , , ( ), - , . , , , 4.3.2.


2.

109

, 2.7.2. , , . 2.7.20. : x(P (a) P (f (b)) P (x)), xy (P (x) P (y )).

, , , 4.


3.


, H(Ar) Ar , . Ar, , . . Ar. , , . , , A (S (0) + 0 = S (0)) Ar. A , 1 0 1. A H(Ar), . (. 2.6.4), , , , , . , , , , . , . , A x(x + 0 = x), . . , , , . . : , , -, (, ,1
1 .

110


3.

111

, , ).

3.1.
3.1.1. ( ) , , , . ( ) . 3.1.2. T , , A . A T ( T ), H() A. , A T , T A. T A. T ; A A T . 3.1.3. , (, , , ), (, , , ). 3.1.4. T , . T . T (. . , ). , H() ; . , . 2.6.20, 2.6.21, 2.6.28í2.6.30 c . , 2.6.21 : . . 3.1.5. T , , A . T A, A T . . H() A A. A , : , A . , : A, T A. 3.1.5 , , .


112 . . . , T , T T . , 2.6.20 . 3.1.6. T . T , T . . , T , T . , , : T , T . T , . . A , T A T ìA. B ìA (A B ). , T B . , T . 3.1.7. , T : ) AìA T , ) A ìA T . . . , . - . , , , . , . , . , , , , , . , . . 3.1.8. T , M , [T ] , T , T h(M ) M . T M , [T ] = T h(M ). , 1) T , T ; 2) T , M T M .


3.

113

3.1.9. , 3.1.2 . , . T , , A . A T ( T ), {G1 , . . . , Gn } , G () G1 , . . . , Gn A, G1 , . . . , Gn , G1 , . . . , Gn , . 3.1.10. ? , G1 , . . . , Gn , G1 , . . . , Gn . , 3.1.2 . 3.1.11. G (), , 3.1.2, ? T , , A . A T ( T ), {G1 , . . . , Gn } , G () G1 , . . . , Gn A. . . .

3.2.
, , , . . , , . 3.2.1. T , , =. = (. 2.2.2): t1 = t t1 = t
2

(t1 = t2 ) (t1 = t2 )

= (t1 , t2 ), ì(t1 = t2 ).

2

T , (, , ) : 1) x(x = x); 2) xy (x = y y = x);


114 . . 3) xy z (x = y y = z x = z ); 4) x1 . . . xn y1 . . . yn (x1 = y1 . . . xn = yn f (x1 , . . . , xn ) = f (y1 , . . . , yn )) n N ; 5) x1 . . . xn y1 . . . yn (x1 = y1 . . . xn = yn (P (x1 , . . . , xn ) P (y1 , . . . , yn ))) n N+ n- P , =. 1í3 , , 4í5 . 1í5 . 3.2.2. , =, M D, ² . M , ²(=) ( ) D. , , , ( ) . , , =, , , . . . . , (. . , ) . ( ) , (, ) (, ). 3.2.3. x1 x2 y1 y2 (x1 = y1 x2 = y2 (x1 = x2 y1 = y2 )). - ( =)
+

n- f


3.

115

3.2.1 . 3.2.4. , § = (. 2.2.2). . : 1) x(x = x), 2) xy (x = y y = x), 3) xy z (x = y y = z x = z ), 4) x1 x2 y1 y2 (x1 = y1 x2 = y2 x1 § x2 = y1 § y2 ). , § : 5) xy z ((x § y ) § z = x § (y § z )). . . ( , .) , , : 6) z (x(x § z = x z § x = x) xy (x § y = z y § x = z )). . 7) xy (x § y = y § x), ( ) . , , § , = , , , . , , § , = , , . 3.2.5. , . 3.2.6 ( ). T , .


116 . . . 2.6.28 T D, ² D. M M D , ² , M T . D , ²(=) D. ( , D D, ²(=).) D , D . D []. n- f n > 0 ² (f ) : [1 ], . . . , [n ] [²(f )(1 , . . . , n )], n = 0 ² (f ) = [²(f )]. n- P n > 0 ² (P ) : [1 ], . . . , [n ] ²(P )(1 , . . . , n ), n = 0 ² (P ) = ²(P ). M , ² 1 , . . . , n . D ² ² (=) D . , M T . , A : I V D : M , A, M , A, : I V D , x I V (x) = [ (x)]. A . 3.2.7. , . 3.2.8. , . 3.2.9. , . . . 2.6.35 . 94. 3.2.6 , 2.6.30 2.6.31 2.6.21 . 3 T .2.10 ( ). , . , T .

3.2.11 ( ). T , A . T A , T A.


3.

117

3.2.12. ( ) . , , 3.2.1. . =, A , , x ( , , x A, , x A ). : !xA xA xy (A [A]x x = y ), y

y , A. !xA x , A x, A . , !xA. M D, ² . M , !xA, x D , M , A. , !xA xA x, A, xy (A [A]x x = y ) , x y , y A, . 3.2.13. y A , !xA? , , , !xA x, A. 3.2.14. , : !xA x(A y ([A]x x = y )) y !xA y x(A (x = y )),

y A. ( , , !xA , , !xA .)

3.3.
, , .


118 . .

3.3.1.
, , Ar (. 2.2.2). P A.2 P A. : E 1) x(x = x), E 2) xy (x = y y = x), E 3) xy z (x = y y = z x = z ). E 4) xy (x = y S x = S y ), E 5) x1 x2 y1 y2 (x1 = y1 x2 = y2 x1 + x2 = y1 + y2 ), E 6) x1 x2 y1 y2 (x1 = y1 x2 = y2 x1 § x2 = y1 § y2 ). : P 1) x(S x = 0), P 2) xy (S x = S y x = y ), P 3) ([A]x x(A [A]x x ) xA) 0 S A Ar x, P 3 , , . , : A1) x(x + 0 = x), A2) xy (x + S y = S (x + y )), M 1) x(x § 0 = 0), M 2) xy (x § S y = x § y + x). P A . , P 3 , xA Ar. , Ar ( 2.2.2) P A, , 3.1.5 , P A, . P A , P A , Ar ( , P A Ar, ). , 5.5.4, , P A, .
2

PA

Peano Arithmetic .


3.

119

3.3.2.
, Ar . , , P A , . m m SS . . . S 0
m

( S S . . . S 0, , m S ). x 0 P1 = P2 n = 0, 2) (f1 (1 , . . . , n )) = f2 ((1 ), . . . , (n )) n > 0 (f1 ) = f2 n = 0. M1 M2 , M1 M2 , . 3.3.2. , M1 M2 , A : M1 A , M2 A. (, .)


120 . . , N, ²1 c D2 , ²2 . , : N D2 c . m (m) = ²2 (c). , Si ²i (S ), 0i ²i (0) (i = 1, 2) , (m) = (| S S . . . S 0| ) = (S1 S1 . . . S1 01 ) =
m m

S2 S2 . . . S2 02 = | S S . . . S 0|c = ²2 (m).
m m

, ²2 (m) = ²2 (c), , c m = c , c T m < c . , c . P A, , . , c P A.

3.3.3.
, , P A S S 0 + S 0 = S S S 0. A2 ( ) S S 0 + S 0 = S (S S 0 + 0). , A1 S S 0 + 0 = S S 0. , S (S S 0 + 0) = S (S S 0). ( ) S S 0 + S 0 = S S S 0, . ( ) . , S S . . . S 0 , , P 1íP 3, A1, A2, M 1, M 2 . () , . , A1 : x x + 0 = x . , , , . , , , . , . , , . , , , , ; ; , . . .


3.

121

- . , . , , , , . . , , , . , , . , . 3.5.5. , P A S S 0 + S 0 = S S S 0, . . S S 0 + S 0 = S S S 0 P A. : , A2, ( ) S S 0 + S 0 = S (S S 0 + 0) (. 1í5 ); , A1 S S 0 + 0 = S S 0 (. 6í8); , E 4, ( ) S (S S 0 + 0) = S S S 0 (. 9í14); , E 3 ( ) ( ) S S 0 + S 0 = S S S 0 (. 15í25). 1) xy (x + S y = S (x + y )) A2 P A; -

2) xy (x + S y = S (x + y )) y (S S 0 + S y = S (S S 0 + y )) 13 H(Ar); 3) y (S S 0 + S y = S (S S 0 + y )) 1 2 M P ; 4) y (S S 0 + S y = S (S S 0 + y )) S S 0 + S 0 = S (S S 0 + 0) 5) S S 0 + S 0 = S (S S 0 + 0) 3 4 M P ; 6) x(x + 0 = x) A1; 13;

13;

7) x(x + 0 = x) S S 0 + 0 = S S 0 8) S S 0 + 0 = S S 0 6 7 M P ; 9) xy (x = y S x = S y )

E 4; -

10) xy (x = y S x = S y ) y (S S 0 + 0 = y S (S S 0 + 0) = S y ) 13; 11) y (S S 0 + 0 = y S (S S 0 + 0) = S y ) 9 10 M P ; 12) y (S S 0 + 0 = y S (S S 0 + 0) = S y ) (S S 0 + 0 = S S 0 S (S S 0 + 0) = S S S 0) 13;

13) S S 0 + 0 = S S 0 S (S S 0 + 0) = S S S 0 11 12 M P ; 14) S (S S 0 + 0) = S S S 0 8 13 M P ; 15) xy z (x = y y = z x = z ) E 3;


122 . . 16) xy z (x = y y = z x = z ) y z (S S 0 + S 0 = y y = z S S 0 + S 0 = z )

13;

17) y z (S S 0 + S 0 = y y = z S S 0 + S 0 = z ) 15 16 M P ; 18) y z (S S 0 + S 0 = y y = z S S 0 + S 0 = z ) z (S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = z S S 0 + S 0 = z ) 13;

19) z (S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = z S S 0 + S 0 = z ) 17 18 M P ; 20) z (S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = z S S 0 + S 0 = z ) (S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0 S S 0 + S 0 = S S S 0) 13; 21) S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0 S S 0 + S 0 = S S S 0 19 20 M P ; 22) S S 0 + S 0 = S (S S 0 + 0) (S (S S 0 + 0) = S S S 0 S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0) 3; 23) S (S S 0 + 0) = S S S 0 S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0 5 22 M P ; 24) S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0 14 23 M P ; 25) S S 0 + S 0 = S S S 0 21 24 M P . 3.3.3. , , P A S 0 = 0 P A S 0 = S S 0. 3.3.4. , , P A S S 0 + S 0 = S S S 0 P A S S 0 § S S 0 = S S S S 0. ( , P A .) , P A , , Ar. , . . , P A x + y = y + x x y . , P A. A x + y = y + x. , P 3 A, [A]x ( ) 0 A [A]x x ( ). S B [A]x , . . 0 + y = y + 0, 0 . [B ]y B [B ]y y . 0 S [B ]y 0 + 0 = 0 + 0 , , A1. B [B ]y y 0 S 0 + y = y + 0 0 + Sy = Sy + 0 0 + S y = S (0 + y ) = S (y + 0) = S y = S y + 0,
3
3 , t = t = t 1 2 3 : t1 = t2 t2 = t3 . ‡ .


3. 0 + y

123

A2, = y + 0 , A1. A [A]x x , . . S x + y = y + x S x + y = y + S x.

A2 x + y = y + x y + S x = S (y + x) = S (x + y ), , S x + y = S (x + y ). C S x + y = S (x + y ), [C ]y C [C ]y y . [C ]y S x + 0 = S (x + 0) 0 0 S A1. C [C ]y y S S x + y = S (x + y ) S x + S y = S (x + S y ) S x + S y = S (S x + y ) = S S (x + y ) = S (x + S y ), A2, S x + y = S (x + y ) . . 3.3.5. ((x + y ) + z = x + (y + z )), (x § y = y § x (x § y ) § z = x § (y § z )), (x § (y + z ) = x § y + x § z ). 3.3.6. P A x(y (y < x [A]x ) A) xA, y ()

A Ar, x y , y A, x < y 3.3.2 (. ()). (, () , xA Ar.)

3.4.
, . 3.5, .


124 . .

3.4.1.
. , . . , s t, s t. s t, , s t t s. , . , : 1) ; 2) s t , (s = t) (s t) ;

3) A B , x , ìA, (A B ), (A B ), (A B ), xA xA ; 4) A . , x , {x | A}

, {x | ì(x y )} = z . . , 4 . 3.1.1. , , , , . {x | A} A; x : x | . , , : 1) (): xy (z (z x z y ) x = y ). , x y , , ; 2) : y ((y {x | A}) [A]x ), y A , x y , y A. , {x | A} x, A.


3.

125

. - : , , , , , . . , {x | ì(x = x)}, x y {z | z x z y }. , , . . , . ( .) , , , . ( , ), . , ( 3.1.6). .

3.4.2.
u {x | ì(x x)}, . . , . y y u ì(y y ). , y u, u u ì(u u). ()

, u u, () ì(u u), ; ì(u u) (, , . 1.3.3). ì(u u) () u u. , u u ì(u u), . , . : , , , . ? , , , , , . , . : . , ( , ).


126 . .

3.5. - Z F
, , , . , , , , , . , , , , , .

3.5.1. Z F
-, . Z F .4 = . ì(s t) (s t) / s t. / Z F . , , . 3.5 () A A , A Z F , , A Z F , . , 5 . A, . Z F ( ) . 1. (). x y , , : xy (z (z x z y ) x = y ). , , , xy (x = y z (z x z y )) .
4 Z F Zermelo Fraenkel. 5 , .


3.

127

2. . x, : xy (y x). / x, (. . y (y x)), . / , , , , . . 6 !xy (y x). / x x1 , y (y x) y (y x1 ), / / y (y x y x1 ). , y (y x y x1 ), / / x = x1 , . Z F , . y (y ). / , , , Z F . , w = y (y w). / 3. . x y z , x y : xy z w(w z (w = x w = y )). 3.5.1. , 3.5.1 , z , , xy !z w(w z (w = x w = y )). z {x, y }. h(x, y ). : xy w(w {x, y } (w = x w = y )). x {x} {x, x} . , {x} x. x, y {{x}, {x, y }} x y . x y , , x, y . . 3.5.2. xy uv ( x, y = u, v (x = u y = v )).
6 3.5 , .

x y h : -


128 . . . (x = u y = v ) x, y = u, v , , . x, y = u, v , . . {{x}, {x, y }} = {{u}, {u, v }}. (I) {u} x, y (II) {u, v } x, y , : (I) (1) {u} = {x} (2) {u} = {x, y } (II) (3) {u, v } = {x} (4) {u, v } = {x, y }. (2) , x = y = u. (3), (4) {x, v } = {x}, x = v . , , (2), x = y = u = v , , (x = u y = v ). , (3). , (1) (4). (1) u = x, (4) v = x v = y . u = x v = x, (4) {x} = {x, y }, u = v = x = y , , (x = u y = v ). , . . u = x v = y , (x = u y = v ) . , (n + 1)- (n = 2, 3, . . .) : x1 , . . . , xn , xn+
1

x1 , . . . , xn , xn+1 ,

n- n = 1 x1 x1 . m- (m = 1, 2, 3, . . .) , . 4. (). x u, , x: xuy (y u z (z x y z )). 3.5.3. , u , . u x x. zx z . x, xy (y x z (z x y z )). x1 x2 x1 x2 {x1 , x2 },


3. x1 x2 . (: {{x1 }, {x2 }} = {x1 , x2 } .) x1 , x2 x3 x1 x2 x3 (x1 x2 ) x3 ,

129

x1 , x2 x3 . . {x1 , x2 , x3 } {{x1 , x2 }, {x3 }}, {x1 , x2 , x3 , x4 } {{x1 , x2 , x3 }, {x4 }}

. . 3.5.4. , xy z (z x y z x z y ), xy z ((x y ) z = x (y z )), xy z ({x, y , z } = {z , x, y , y }).

, : xy z (z x z y ).

, x y (x y , x y y x), x y , . . x y . 5. ( ). x y , x : xy z (z y z x). 3.5.5. , y , . y ( ) x 2x . , xz (z 2x z x). 6. . x, , y x y {y }: x I nd(x), I nd(x) ( x y (y x y {y } x)),

, Z F I nd(x) : w(z (z w) w x) y (y x u(v (v u v y v = y ) u x)). / x I nd(x), x .


130 . . 7. . x y , x, (. . ) A: xy z (z y (z x A)), A Z F , x, y , z ( 7 ) , y A. A , z , y . ( z , A.) , y , , , , x!y z (z y (z x A)). y {z x | A}. : xw(w {z x | A} w x [A]z ), w A Z F , w, x, z ( ) , w A. x1 x2 x1 x2 {z x1 | z x2 }, x1 x2 . x1 , x2 x3 x1 x2 x3 (x1 x2 ) x3 ,

x1 , x2 x3 . . , x x {y x | z (z x y z )},

x. zx z . x y x\y {z x | z y }. /

3.5.6. , , xy z ((x y ) z = x (y z )), xy z ((x y ) z = (x z ) (y z )), xy z ((x y ) \ z = (x \ z ) (y \ z )), xy z (x \ (y z ) = (x \ y ) (x \ z )).

7

. 3.2.


3.

131

8. (). u v , A(u, v ) (. . A u v ), x y , v , u x A(u, v ): (u!v A xy v (v y u(u x A))), A Z F , u, v , x, y ( ) , y A, u v A ( , A ). y x , : x A(u, v ) y . A(u, v ) u x v y . , . , y , u!v A, , , (u!v A x!y v (v y u(u x A))). 3.5.7. Z F8 Z F , 3.5.1. Z F8 , Z F8 : , u v A. , Z F8 Z F8 . 9. (). x y , x y (. . x y ): x(x = y (y x x y = )) , Z F : x(z (z x) y (y x wì(w x w y ))). , , x x, x y y x, x y y z z x. , , x y , x y y x. , , x y x y y x. v {x, y }. v x = , y v y x. v y = . , v , , v , . . Z F .
ux v y


132 . . 3.5.8. Z F , . , , . , 8 , , F. , x : y (y x). Z F / , ( ) .

3.5.2. Z F
- . Z F , 3.5.2 3.5.3 . ( ) x½y {z 2
2xy

x y -

| uv (u x v y z = u, v }.

3.5.9. , x ½ y . z 22 x ½ y , . . x y z = u, v 22 , , u x v y u, v 2
2xy x y

.

, , u, v {{u}, {u, v }}. u x v y u x y v x y . {u} x y {u, v } x y, {u} 2xy {u, v } 2xy . {{u}, {u, v }} 2xy , . . u, v 2xy , x y , u, v 22 . , x y u, v , u x v y . n + 1 (n = 2, 3, . . .) : x1 ½ . . . ½ xn ½ xn+
1

(x1 ½ . . . ½ xn ) ½ xn+1 .

3.5.10. , , , xy z ((x y ) ½ z = (x ½ z ) (y ½ z )), xy z ((x \ y ) ½ z = (x ½ z ) \ (y ½ z )).

8 , Z F , .


3. Rel(z ) xy (z x ½ y ).

133

z , Rel(z ). , z , , z . z dom(z ) {u z | v ( u, v z )}.

, , , u z . dom(z ) z . z rng (z ) {v z | u( u, v z )}.

u z , rng (z ) z . ( ) . , . . , , , , . x x. F nc(z ) Rel(z ) uv1 v2 ( u, v1 z u, v2 z v1 = v2 ).

z ( ), F nc(z ). , , . 9 f :X Y F nc(f ) dom(f ) = X rng (f ) Y .

, f X Y ( f X Y ), f : X Y , . . f X , Y . X Y X Y {f 2X ½Y | f : X Y }. , f 2X ½Y . : y = f (x) f :xy F nc(f ) x, y f .

9 3.5 f , X , Y . (. 2.1.1) , .


134 . . , x dom(f ) y , f x ( x, x x) f (x). x dom(f ) : f (x) f x, y f . y f

{y rng (f ) | x, y f };

, x dom(f ) {y rng (f ) | x, y f } . f , f ( ), . f : x, y z f : x, y z , f ( x, y ) f (x, y ). . 3.5.11. ) , ) , , ) , , ) .

3.5.3. Z F
, Z F . x , I nd(x), . . x y (y x y {y } x). S y S (y ) , y {y } S , S S , S S S , ... .

: 0 , 1 {}, 2 {, {}}, 3 {, {}, {, {}}}, ... .

x, x . , , N , . ( ) N 0, 1, 2, 3, . . . . (. . , ) {z x | u(I nd(u) z u)} . N . N ( Z F ) , .


3.

135

3.5.12. Z F , , 2N N. , Z F , 2.6.28 Z F . . , . . , . Z F : u, v x, y , u + y = x + v . x, y [x, y ]. : [u, v ] = [x, y ], u + y = x + v . , [x, y ] x, y (x - y ) (x - y ). , [0, 2], -2, x, x + 2 , x N. , : [u, v ] + [x, y ] = [u + x, v + y ] (: (u - v ) + (x - y ) = (u + x) - (v + y )), [u, v ] § [x, y ] = [u § x + v § y , u § y + v § x] (: (u - v ) § (x - y ) = (u § x + v § y ) - (u § y + v § x)), , . . ( 0) : u, v x, y , u § y = x § v . 3.5.13. . R ( ) . , . (, < > ) (, , , ). , Z F (., , [45]). x ( ) , u(x : N u). x , x(n) xn n- .


136 . . x , x : N R. Z F , , . , , . x z R. , z x, : > 0 k , m > k |xm - z | < . : ( R > 0 k (k N m(m N m > k |xm - z | < ))). : x y A x(x y A) ( x, y , , A ) x y A x(x y A) ( x, y , A ). : R ( > 0 k N m N (m > k |xm - z | < )). 3.5.14. Z F , , ) - , ) , ) , ) . ( , , [45].)

3.5.4. Z F C
Z F , , Z F C - .10 . X f , x X f x x: X f (F nc(f ) dom(f ) = X x(x X x = f (x) x)) . , f x X x. f , X , X .
10 Z F C Z F C axiom of Choice .


3.

137

Z F , ( ), . . , , , . . ( ) . : (a) (b) - . . , (a) (b), (., , [45]): n () n - a xn , xn . : xn . , , 4.1.3. 3.5.15. - . . , Z F C : , . , , Z F C , , . Z F C , Z F C , .

3.5.5. Z F C
Z F C , , . . , , Z F C , . Z F C , . ( ) Z F C , . Z F C .


138 . . - Z F C . (, , , 3.4 , Z F C .) , 3.3.3, , . Z F C . Z F C ( Z F ) , , Z F C ( Z F ) . P A Z F P A Z F . A P A A Z F , P A A Z F A , (ìA) ìA . . , P A Z F . , P A , A , P A A P A ìA; , Z F A Z F ìA , , Z F . Z F Z F C , . , Z F , Z F C . (. 5.5.38 ) , Z F C , Z F C . Z F C . Z F C . Z F C , Z F C . , Z F Z F C . , , , ( ), , . 3.5 , . , : , ( , . ) . , ( ) , .


3.

139

, . . , , -, , . : - , .


4.


, , . , . , () , , . , , , .

4.1.
. . , ( ), , ( ). (), . . : , , . , (. 1.1.35 . 27), . 140


4.

141

, . F S . A . - (, . 2.5) Q1 x1 . . . Qn xn B , n 0, i = 1, . . . , n , B Qi . ( , , ). , B . , x1 , . . . , xn : xi xj i < j , Qi xi ( , , , : ). S k o , F S S k o = m N S k o m- . A , S k o. Q1 x1 . . . Qn xn B x1 Q2 x2 . . . Qn xn B , S k o c, B , A1 Q2 x2 . . . Qn xn [B ]x1 . c

Q1 x1 . . . Qn xn B x1 . . . xk
-1

xk Q

k+1 xk+1

. . . Qn xn B ,

S k o (k - 1)- f , B , A1 x1 . . . xk
-1

Q

k+1 xk+1

. . . Qn xn [B ]x f

k

(x1 ,...,x

k -1

)

.

A1 . . , . ( y1 . . . yl B , l 0, B , ) ‡1 ( ) A. S k o . 4.1.1. A x(y P (y ) (ìz Q(z ) y R(x, y ))).

1 ( Skolem).


142 . . 2.5.6 . 82: A xy z y1 (P (y ) (ìQ(z ) R(x, y1 ))). , : (P (y ) (ìQ(z ) R(x, y1 ))) (ìP (y ) (ìQ(z ) R(x, y1 ))) (ìP (y ) ìQ(z )) (ìP (y ) R(x, y1 )). , xy z y1 ((ìP (y ) ìQ(z )) (ìP (y ) R(x, y1 ))), ()

A. x, cx cx () x: y z y1 ((ìP (y ) ìQ(z )) (ìP (y ) R(cx, y1 ))). ()

, y1 , f y1 f y1 (y , z ) () y1 : y z ((ìP (y ) ìQ(z )) (ìP (y ) R(cx, f y1 (y , z )))). , A. 1 . , A 1 , A , A 1 . , - , , , , . 4.1.2. A , . . , : A , . A Q1 x1 . . . Qn xn B , B , x1 , . . . , xn . , . 4.1.3. A x1 . . . xk-1 xk C (k 1) , x1 , . . . , xk ; f (k - 1)- , C ; f (x1 , . . . , xk-1 ) xk C ; E x1 . . . xk-1 [C ]xkx1 ,...,xk-1 ) . A , f( E .


4.

143

. A . , D, ² , M A. M 1 , . . . , k-1 D k D , M , C , , (x1 ) = 1 , . . . , (xk-1 ) = k-1 , (xk ) = k . (. 3.5.4) f : 1 , . . . , k-1 k . M D, ² : ² (f ) = f ² (s) = ²(s) s, f . 1 , . . . , k-1 D M , [C ]xkx1 ,...,xk-1 ) , , (x1 ) = 1 , . . . , f( (xk-1 ) = k-1 . , M E , E . , E . , M D, ² , M E . 1 , . . . , k-1 D x , M , [C ]f kx1 ,...,xk-1 ) , ( (x1 ) = 1 , . . . , (xk-1 ) = k-1 . 1 , . . . , k-1 D x k = ²(f )(1 , . . . , k-1 ) , M , k C . , k M A, A . 4.1.4. 4.1.3 , f (x1 , . . . , xk-1 ) xk C ? . . 2.4.17. 4.1.5. A , 4.1.2 A . A , , , A. , xP (x) P (c) ( , ). 4.1.6. A A1 . . . An ; i = 1, . . . , n Ai Ai , i j , Ai Aj , . , A , (A1 . . . An ) . A1 . . . An , B ( B , ) , . , , , , . 4.1.7. , . . . A , ) B , B , , ) , A . (, , 2.5.1 . 81.) 4.1.2 , A A ( ), 4.1.6 .


144 . . 4.1.8. , ) A , ì A ; ) A , ìA ; ) , B : B , B .

, A ( ) : A ì A . A ; , A . , ( ) . A , , (A1 . . . An ), Ai (i = 1, . . . , n) , . . . , Ai , . (. 1.5), , , A {A1 , . . . , An }, , . , S {A1 , . . . , An }, S ( ) (A1 . . . An ). , A1 . . . An , Ai (i = 1, . . . , n) S Ai . . , , . , . , , . ( ), .

4.2.
, . , .


4.

145

4.2.1.
, , ( ). 4.2.1. S . i N Hi (S ) . H0 (S ) , S , S ; H0 (S ) {a}, a . Hi+1 (S ) Hi (S ) f (t1 , . . . , tn ), f n- , S , t1 , . . . , tn Hi (S ), n N+ . S iN Hi (S ), H (S ). 4.2.2. S
1

{P (f (x)) ìQ(y ), Q(g (a))};

H0 (S1 ) = {a}, H1 (S1 ) = {a, f (a), g (a)}, H2 (S1 ) = {a, f (a), g (a), f (f (a)), f (g (a)), g (f (a)), g (g (a))}. S i N.
2

{P (x) ìQ(y ), Q(z )}; Hi (S2 ) = {a} = H (S2 )

4.2.3. S H (S ) P (t1 , . . . , tn ), P n- , S , t1 , . . . , tn H (S ), n N ( P () P , n = 0). 4.2.4. C , S , , C C H (S ), C H (S ). 4.2.5. S , H (S ) S , I H (S ). I S , n N, n- f , S , t1 , . . . , tn H (S ) : n > 0 |f (t1 , . . . , tn )|I = f (t1 , . . . , tn ), n = 0 |f |I = f . , S S . {P0 , P1 , . . . , Pn , . . .} S . I S {P 0 , P 1 , . . . , P n , . . .}, P n Pn , I Pn ,


146 . . ìPn . , , S , S . . 4.2.6. S {P (f (x)) ìQ(y ), Q(a)}.

S H (S ) = {a, f (a), f (f (a)), f (f (f (a))), . . .}. S H (S ) = {P (a), Q(a), P (f (a)), Q(f (a)), P (f (f (a))), Q(f (f (a))), . . .}. S , : {P (a), Q(a), P (f (a)), Q(f (a)), P (f (f (a))), Q(f (f (a))), . . .}, {ìP (a), ìQ(a), ìP (f (a)), ìQ(f (a)), ìP (f (f (a))), ìQ(f (f (a))), . . .}, {ìP (a), Q(a), ìP (f (a)), Q(f (a)), ìP (f (f (a))), Q(f (f (a))), . . .}.

4.2.7. S , M , I S . , I M , n N, n- P , S , t1 , . . . , tn H (S ) : n > 0 |P (t1 , . . . , tn )|I = |P (t1 , . . . , tn )|M , n = 0 |P |I = |P |M . S . , S . . 4.2.8. S 4.2.6. M {d, e}, ² , ²(a) = d, ²(P )(d) = 0, ²(f )(d) = d, ²(f )(e) = d, ²(Q)(e) = 0.

²(P )(e) = 1,

²(Q)(d) = 1,

I S , M . H (S ) : |P (a)|I = |P (a)|M = ²(P )(|a|M ) = ²(P )(d) = 0, |Q(a)|I = |Q(a)|M = ²(Q)(d) = 1,


4. |P (f (a))|I = |P (f (a))|M = ²(P )(|f (a)|M ) = ²(P )(d) = 0, |Q(f (a))|I = |Q(f (a))|M = ²(Q)(d) = 1, |P (f (f (a)))|I = |P (f (f (a)))|M = ²(P )(d) = 0, |Q(f (f (a)))|I = |Q(f (f (a)))|M = ²(Q)(d) = 1 . . , I {ìP (a), Q(a), ìP (f (a)), Q(f (a)), ìP (f (f (a))), Q(f (f (a))), . . .}.

147

4.2.9. S , M . S M , S , M . 4.2.10. . 4.2.11. S , S S . . S , S , S . , S S . S , M , S . , M , S , . , S . , , , , .

4.2.2.
. 4.2.12. S , H (S ) ( ) P0 , P1 , P2 , . . . . S , i N , 2 i ( ), 2 , Pi ìPi . S . 4.1.

2

, 0.


148 . .

P0 P1 . . . ìP1 . . . P1 . . .

ìP0 ìP1 . . .

. 4.1. S .

4.2.13. S , P H (S ) 3 , P ìP .

p q ìq q

ìp ìq

. 4.2. S1 .

P (a) Q(a) P (f (a)) ìQ(a) ìP (f (a))

ìP (a) Q(a) ìQ(a)

. 4.3. S2 . 4.2.14. S1 {ìp, p ìq , q }. H (S1 ) = {p, q }. S1 . 4.2. S2 {P (x), ìP (f (y )) Q(a), ìQ(x)}. H (S2 ) = {P (a), Q(a), P (f (a)), Q(f (a)), P (f (f (a))), Q(f (f (a))), . . .}. S2 . 4.3. S2 , H (S2 ) ; , , .
3

. 105.


4.

149

S S , . 4.2.15. S , T S . -

(1) T S ; (2) S , T . 4.2.16. . N S I (N ) , , N . , I (N ) , S . I (N ) S . 4.2.17. N S . , N ( I (N )) C S , C , I (N ) ìC . (. 2.4.2 . 75.) 4.2.18. C P1 . . . Pl ìPl
+1

. . . ìPm

( Pi i = 1, . . . , m) I (N ) . , I (N ) ìC , {ìP1 , . . . , ìPl , Pl
+1

, . . . , Pm } I (N ).

4.2.19. S , T S . N T , N S , N , N , S . 4.2.20. , . 4.2.21. , .


150 . .

p


ìp q


ìq


. 4.4. S1 .

P (a) Q(a)


ìP (a)


ìQ(a) ìP (f (a))


P (f (a))


. 4.5. S2 .

4.2.22. , S1 (, S2 ) 4.2.14 . 4.4 (, . 4.5). , . 4.2.23. , S I , I S . 4.2.24. S , C S I S . , C I , I (N ) I C . , -

4.2.25. S , I (N ) S . , I (N ) C S , S S , I (N ).

4.2.3.
( ) . 4.2.26 ( ( )). S . S , S . . S . T S B .


4.

151

IB S , B . S , S IB . , C C S , C IB . C 4 IB . C , , IB C . B . B T , . S T . , S . S S . , 4.2.11 S . 4.2.27 ( ( )). S , S S . . S . ( ) T S . T , L CL S , I (L) ìCL . S CL L T . , S S . S S , S S . 4.2.11 S . , S S . S , 4.2.11, , S I S . S I , S I . S . S I . 4.2.28. , . . . ( ?)

4.2.4.
( ) , 4 1.5.1 , . 57 , (. 4.1).


152 . . S , . i = 0, 1, 2, . . . Si S Hi (S ) (. 4.2.1 . 145). Si , ; (. 2.4.18 . 80). Si , , . ( ) S , S . S , . Si i, S . , , , . . 4.2.29. , . ( Si , ?)

4.3.
( 1.5) . . , , , . , , ìP (x) Q(x) P (f (y )) R(y ).

ìP (x) P (f (y )) , y a x f (a), . ìP (f (a)) Q(f (a)) P (f (a)) R(a), C1 Q(f (a)) R(a). f (a) y f (f (a)) x, ìP (x) P (f (y )) . ìP (f (f (a))) Q(f (f (a))) P (f (f (a))) R(f (a)) C2 Q(f (f (a))) R(f (a)). -: ìP (x) P (f (y )) x f (y ). ìP (f (y )) Q(f (y ))


4.

153

P (f (y )) R(y ) C3 Q(f (y )) R(y ). C3 , C1 C2 , , C1 , C2 C3 . , , .

4.3.1.
. 4.3 . 4.3.1. I V , Dom() {x I V | (x) = x} ( , , ). Dom() . , Dom() {x1 , . . . , xn } (x1 ) = t1 , . . . , (xn ) = tn , {t1 /x1 , . . . , tn /xn } ( , - / ). , , x/x; . , . ( ) {}. {} . (, {x/x} , {}.) , - (, ), - (, {a/x} {b/x} ). 4.3 , . 4.3.2. {t1 /x1 , . . . , tn /xn } E . E x1 , . . . , xn E t1 , . . . , tn . E E , E . W {E1 , . . . , En }. W {E1 , . . . , En }, W . , , , , ( ) .


154 . . 4.3.3. E = P (v , h(f (z , w), g (b, y , z )), x, g (b, y , z )). , , (x) = ((x)) x; . - , E E ( ), , . , , . {t1 /x1 , . . . , tn /xn } {s1 /y1 , . . . , sm /ym } {t1 /x1 , . . . , tk /xk }: 1. ti .
1

{a/u, f (z , w)/x, x/y , g (b, y , z )/z }, E P (v , h(x, z ), y , z ).

(t1 /x1 , . . . , tn /xn )5 , ,

2. 1 x/x, x 2 .

3. s1 /y1 , . . . , sm /ym sj /yj , yj x1 , . . . , xn , 1 . 4. , , 2 1 . 4.3.4. {f (y )/x, z /y }, {a/x, b/y , y /z }. . 1 (f (y ) /x, z /y ) = (f (b)/x, y /y ); 2 (f (b)/x); 1 (y /z ); = {f (b)/x, y /z }. 4.3.5. , . . , E E = (E ) . . , v v = (v ) . 3 . 1. v Dom(), . . v = xi i. v = ti = (v ) . 2. v Dom( ) \ Dom(). v = yj j , , v = sj = v = (v ) . 3. , , v Dom() Dom( ). v = v = (v ) . / , {} = {} = , (E ) = E ( ) ( ) = ( ) ( ), , , , E .
5

.


4.

155

4.3.6. {E1 , . . . , En } ( E1 , . . . , En ), E1 = E2 = . . . = En . , {E1 , . . . , En } ( E1 , . . . , En ), {E1 , . . . , En }; ( ). 4.3.7. {a/x, f (a)/y }. {P (x, y ), {y /x}, {x/y }, {a/x, a/y }, {f (b)/x, f (b)/y , {P (f (x), z ), P (g (y ), a)} . {P (a, f (x)), P (x, y )} P (y , x)} a/ z } . {P (f (x)), P (x)} -

4.3.8. W ( ) , W , = . 4.3.9. {y /x} {P (x, y ), P (y , x)} . , , , {t/x, t/y , L}, t , L s/z , s , z , x y . = {y /x} {t/y , L} ( = {y /x} ), , {y /x} . 4.3.10. {f (x)/y }, {f (x)/y , a/z }, {f (x)/y , u/v }, {f (z )/y , z /x} {P (y ), P (f (x))}? 4.3.11. . 4.3.12. {t1 /x1 , . . . , tn /xn } Rng () {t1 , . . . , tn }. , Dom() = Rng (). . 1. W . W . 2. 1 2 W . , 1 = 2 .

4.3.2.
. , - . . P (g (x), x, f (g (y ))) P (z , a, f (z )). . 6 ,
6

4.3.13.

. 2.3.6 . 72.


156 . . . , : P (g (x), x, f (g (y ))) P (z , a, f (z )). , ( ) x t, z g (t). , x, , z g (x). z g (x) P (g (x), x, f (g (y ))) P (g (x), a, f (g (x))). ()

1 {g (x)/z }, . (), P (g (x), x, f (g (y ))) P (g (x), a, f (g (x))). , x a. x a , {a/x} . P (g (a), a, f (g (y ))) P (g (a), a, f (g (a))) ()

2 1 {a/x} = {g (a)/z , a/x}. () , , : P (g (a), a, f (g (y))) P (g (a), a, f (g (a))). , y a. : 3 2 {a/y } = {g (a)/z , a/x, a/y }.

{a/y } P (g (a), a, f (g (a))) P (g (a), a, f (g (a))). , 3 . 4.3.14. W , d , - W . W , (. . ) - W d. 4.3.15. W {P (g (x), x, f (g (y )), P (z , a, f (z ))}.

(W 4.3.13.) W {g (x), z }.


4. {P (x, f (x)), P (x, a), P (x, f (g (z , x)))} {f (x), a, f (g (z , x))}.

157

, ( ), , , . W ( , ) : (1) k = 0, W0 = W , 0 = {}. (2) Wk , , k . Dk Wk . (3) vk tk Dk , vk , tk , k+1 = k {tk /vk } Wk+1 = Wk {tk /vk }. , . (4) k = k + 1 (2). , (3) vk tk ( ), . , , 4.3.2. 4.3.16. , Wk k , Wk = W k . k , Wk = W k W . 4.3.13 . . 4.3.17. W {Q(f (x), x), Q(y , g (y ))}. (a1) W0 = W , 0 = {}. (a2) W0 1 , D0 W0 : D0 = {f (x), y }. (a3) D0 f (x) y , . 1 = 0 {f (x)/y } = {f (x)/y } W1 = W0 {f (x)/y } = {Q(f (x), x), Q(f (x), g (f (x)))}. (a4) (2) k = 1. (b2) W1 1 , D1 W1 : D1 = {x, g (f (x))}. (b3) D1 x , x - D1 (x g (f (x))), , W .


158 . . 4.3.18. W . W . . , ( ) W . W0 , W1 , . . . , Wk , Wk+1 , . . . ( ) , k N Wk+1 7 , Wk ( vk Wk , Wk+1 = Wk {tk /vk }). , W0 = W . 4.3.19. W , W . . 4.3.18 . (2) (3). (2), , , W . (2). , (3) , , . 4.3.20. W , W W , W = . . W . , k N S (k ): (3) k , k , = k . 4.3.18 k = m (2) m W , , = m . , S (k ) k N, k . S (0) , (1) 0 = {}. . , S (k ). , S (k + 1). (3) k . (2) k , S (k + 1) . k Wk . Wk , (2) k+1 ; , S (k + 1) . , Wk . Dk Wk .
7 , , , , .


4.

159

= k ( ) W ), W (, Wk = W k = W . , Wk , , , Dk . Dk , Dk ( , ). vk , Dk . tk Dk , vk . Dk , vk = tk . , vk tk , , vk tk . Dk tk vk , tk . , (3) k+1 = k {tk /vk }. S (k + 1) , k+1 = . k
+1

= (k {tk /vk }) = k ({tk /vk }).

{tk /vk }. {t/vk , L}, L s/z , z vk . , vk = tk , {tk /vk } = {tk /vk , L} = {vk /vk , L} = . k
+1

= k ({tk /vk }) = k = ,

. , S (k + 1) . 4.3.21. , = . 4.3.22. , {t1 /x1 , . . . , tn /xn }, i = 1, . . . , n ti xi , Rang e() , t1 , . . . , tn . , , Dom() Rang e() = . 4.3.23. W . , , W = . , . 4.3.24. W , W W , . 4.3.25. , .


160 . .

4.4.
( , ) , .

4.4.1.
4.3 , , . . , , . 4.4.1. C ( ) , C ( ) C . 4.4.2. C ìP (x) ìP (f (y )) Q(x). {f (y )/x}.

ìP (x) ìP (f (y ))

C = ìP (f (y )) Q(f (y )) C . () ( 2.3.2). A, B , x1 , . . . , xn , y1 , . . . , yn . B x1 , . . . , xn A y1 , . . . , yn , , B A. 4 , ; . 4.4.3. C1 C2 . , C1 C2 ( C1 C2 , ). C1 ( ) L1 , C2 L2 . L1 ìL2 ( ìL1 L2 ) , (C1 \{L1 })(C2 \{L2 }) C1 C2 , L1 L2 . 4.4.4. , C , , C (. 4.1).


4.

161

. , , . 4.4.13 . 4.4.5. C1 ìP (f (y )) Q(f (y )) C2 P (y ) R(y ).

y C2 z C2 P (z ) R(z ). L1 ìP (f (y )) C1 L C2 {f (y )/z }.
2

P (z ) -

(C1 \ {L1 }) (C2 \ {L2 }) = ({ìP (f (y )), Q(f (y ))} \ {ìP (f (y ))}) ({P (f (y )), R(f (y ))} \ {P (f (y ))}) = {Q(f (y ))} {R(f (y ))} = {Q(f (y )), R(f (y ))} = Q(f (y )) R(f (y )) C1 C2 . 4.4.6. C1 C2 : C1 C2 , C1 C2 , C2 C1 , C1 C2 . 4.4.7. C1 ìP (x) ìP (f (y )) Q(x) C2 P (y ) R(y ).

, C1 ìP (f (y )) Q(f (y ))

C1 , C Q(f (y )) R(f (y ))

C1 C2 . C C1 C2 . C1 , C1 C2 . y C2 z C2 P (z ) R(z ).

ìP (x) C1 P (z ) C2 {z /x}, ìP (f (y )) Q(z ) R(z ) (, , ) C1 C2 .


162 . . 4.4.8. C1 C2 C1 , C2 C . , C .

4.4.9. 4.4.8. . , 1) C C , C C , 2) C C1 C2 , C1 , C2 C (. 1.5.4). , 1.5. 1.5.6 , 4.4.8. 4.4.10 ( ). S . S , S . 4.4.11. C , S . , ( ) , ( ) C S , C , S , C , C . , . 4.4.12. S , : 1) P (x), 2) ìP (f (y )) Q(a), 3) ìQ(x). S : 4) Q(a) 1 2 ( P (x) 1 ìP (f (y )) 2 {f (y )/x}), 5) 3 4 ( ìQ(x) 3 Q(a) 4 {a/x}). S

, S . : 1 4 5 . 2 3

.


4. 4.4.13. {P (a, x), ìP (x, b)}?

163

, , ? 4.4.14. {P (u) P (v ), ìP (x) ìP (y )}? ( )? 4.4.15. , 2.6.14 . 89, A B y P (x, f (y )) xQ(x, z ) .

4.4.2.
. : . -

4.4.16 ( ). C1 C2 , C1 C2 C1 C2 , C C1 C2 . C C1 C2 , C C . . (. ), C1 C2 . C C1 C2 , C = (C1 \ {L1 }) (C2 \ {L2 }), , L1 L2 , L1 = ìL2 . k = 1, 2 Ck Ck , Ck = Ck k , k . C1 C2 , , Dom(1 ) Dom(2 ) = . 1 2 . Ck = Ck . 1 k = 1, 2 Lk , . . . , Lnk (nk N+ ) k n 1 - Ck , Lk = Lk = . . . = Lk k . ( , L1 , . . . , Lnk Ck Lk Ck k k Ck .) , k = 1, 2 n Wk {L1 , . . . , Lk k }. 4.3.20 k k Wk , = k ; nk = 1, k . Ck k Ck nk > 1, Ck k = Ck nk = 1.


164 . .
1 k = 1, 2 Lk = Lk = L1 k . L1 = ìL2 , k 1 1 L1 1 ìL2 2 . 4.3.20 L1 1 ìL1 2 , = . 1 2 C C1 C2

C

(C1 1 \ {L1 1 }) (C2 2 \ {L1 2 }). 1 2 C . ,

, C

C = (C1 \ {L1 }) (C2 \ {L2 }) = (C1 \ {L1 }) (C2 \ {L1 }) = 1 2 (C1 1 \ {L1 1 }) (C2 2 \ {L1 2 }) = 1 2 (C1 1 \ {L1 1 }) (C2 2 \ {L1 2 }) = C . 1 2

4.4.17 ( ). S , S . T p N
2


a

T N
1

b

T N
1

c



ìp N q N
4


p
3

ìp


N ìq


2



N

3

ìp

ìp N
5

p

p ìq

q

. 4.6. C Ta , Tb , Tc . . S , : 1) ìp, 2) p ìq , 3) q . Ta S , . 4.6. , . L Ta ( ) S , I (L). N3 N4 N5 , Resa p. , Resa I (N3 ). Tb , Ta N3 , S {Resa}.


4.

165

N1 Tb N2 N3 . N2 N3 , Resb , Resb I (N1 ). Tc S {Resa } {Resb }, Resb . , S , , . , S ( , S ): 4) p 5) 2 3, 1 4.

. 4.4.17. ( ) T S . , k N+ : S T S k S . k . . T N0 . S , I (N0 ), . . . T m > 1 , , k < m. T , , . , , T . , T N . N N1 N2 , , N N1 N2 , Pn ìPn (. . 4.7). , : I (N1 ) = I (N ) {Pn } I (N2 ) = I (N ) {ìPn }.

Pn N
1


N ìPn N

2

. 4.7. N , N1 N2 T .


166 . . N1 , C1 C1 S I (N ) {Pn } ìC1 I (N ) ìC1 . , ìPn C1 . N2 , C2 C2 S I (N ) {ìPn } ìC2 I (N ) ìC2 . , Pn C2 . C (C1 \ {ìPn }) (C2 \ {Pn }) C1 C2 , , I (N ) ìC . C C1 C2 , C C . S {C } , S . I (N ) ìC , I (N ) C , , T S {C } T N1 N2 . T S {C }, , S {C }. C1 , C2 C , S . 4.4.18. . 161 4.4.6 . C1 C2 . , C1 C2 ( C1 C2 , ). k = 1, 2 Ck ( ) L1 , . . . , Lnk nk N+ . k k {L1 , . . . , Ln1 , ìL1 , . . . , ìLn2 } ( {ìL1 , . . . , ìLn1 , L1 , . . . , Ln2 }) 1 2 1 2 1 2 1 2 , (C1 \ {L1 }) (C2 \ {L1 }) 2 1 C1 C2 . .

4.4.3.
A ì A S , . A S . : S , S . ? , S . S0 , S1 , S2 , . . ., S0 = S , Si+1 (. ) C C , C S0 . . . Si , C Si . , , , S . 4.4.19. ,


4.

167

. , : , 4.3.2. , 4.3.12 . S , S . S , . , . , , , . - . , . , () . , SLD-, 4.5. 4.4.20. , ( ) , . . , . ? ( ) ?

4.5.
. (, Pascal, C++, Java, C#) , . , . , , (, Lisp, Haskell) (, Prolog, Datalog). 8 ( ) , . , , , , .
8 .


168 . . , . . , . (, , .) , Prolog, , .

4.5.1.
B1 , . . . , Bn A1 , . . . , Am , B1 , . . . , Bn , A1 , . . . , Am , , m, n N. (i = 1, . . . , m) , (j = 1, . . . , n) . B1 , . . . , Bn A1 , . . . , Am m > 0 n > 0 ( ) (B1 . . . Bn ìA1 . . . ìAm ), m = n = 0 . , (A1 . . . Am B1 . . . Bn ), , (, ) T (, F). A (C1 . . . Cl ), i = 1, . . . , l Ci , C C1 . . . Cl A (. 4.1.2). C A. , . 4.5.1. clause . . , , . , . , . B A1 , . . . , Am (m 0); B , A1 , . . . , Am . , . B . . Ai Bj


4.

169

4.5.2. , ( ) . G ( G ), G1 , . . . , Gn , n N i = 1, . . . , n Gi , . Gi (i = 1, . . . , n) G. n > 0 G G1 . . . Gn . n = 0 G . , , , T. () , . E E , 4.3.2 . G P , , P G, , , P G Dom() , G. G; P G, G . . , P G, , P G. , , , P , . , P (a) P (b) xP (x), t , P (a) P (b) P (t). P (a) P (b) xP (x), P (a) P (b) xP (x), , , {P (a) P (b), ìP (x)}. , , x a, b.

4.5.2. SLD-
P {C1 , . . . , Ck }, k 0 ( k = 0 P ) G (G1 , . . . , Gn ), n 0. n = 0 . , , P G, n > 0. 2.4.3 : P G, C1 . . . Ck G. C1 . . . Ck G , C1 . . . Ck (ìG1 . . . ìGn ). , S {C1 , . . . , Ck , (ìG1 . . . ìGn )}, ()


170 . . i = 1, . . . , k Ci Ci (. . Ci Ci ). S . , SLD-. . 4.5.3. ìG1 . . . ìGj C
-1

ìGj ìGj

+1

. . . ìGn (m 0).

(n > 0)

B ìA1 . . . ìAm

, C ( C , ). j {1, 2, . . . , n} Gj B . SLD- C (ìG1 . . . ìGj
-1

ìA1 . . . ìAm ìGj

+1

. . . ìGn ),

n = 1 m = 0 . 4.5.4. l , S , (). SLD- l S , . 4.8, i0 , . . . , il-1 {1, 2, . . . , k }, 0 (ìG1 . . . ìGn ) j = 0, 1, . . . , l - 1 j +1 SLD- j Cij .
0

Ci0
1

Ci1
2 l- 1

Cil

-2



Cil
l

-1

. 4.8. SLD- l S . , SLD- SLD j Cij j +1 j = 0, 1, . . . , l - 1. 1 2 . . . l l > 0 {} l = 0 . , {t1 /x1 , . . . , tj /xj , tj +1 /xj +1 , . . . , tl /xl } , x1 , . . . , xj 0 , xj +1 , . . . , xl 0 . {t1 /x1 , . . . , tj /xj }.


4. ,

171

, SLD- . . , x y , P ar, . : 1) P ar(cAdam, cC ain) , 2) P ar(cE v e, cC ain) , 3) P ar(cAdam, cAbel) , 4) P ar(cE v e, cAbel) , 5) P ar(cC ain, cE noch) . x z . P red , P red(x, z ) ( ). , x z , x z , x z , y , x z , y z . (P ar(x, z ) y (P ar(x, y ) P red(y , z )) P red(x, z )), p q r (p r) (q r) ((P ar(x, z ) P red(x, z )) (y (P ar(x, y ) P red(y , z )) P red(x, z ))). : (P ar(x, z ) P red(x, z )) (P ar(x, y ) P red(y , z ) P red(x, z )). ()

; , {C1 , . . . , Ck } E , C1 . . . Ck E . , () 9 : 6) P red(x, z ) P ar(x, z ), 7) P red(x, z ) P ar(x, y ), P red(y , z ). , 1í7 .
9 , .


172 . . P red(x, cE noch), P ar(x, cAbel) , , , cE noch, , cAbel. , , , 1í7, , : 8) ìP red(x, cE noch) ìP ar(x, cAbel). SLD- . (a) 1í7, . , ; , P red(x, cE noch) . 6 ) P red(x1 , z1 ) P ar(x1 , z1 ), 6. SLD- 10 6 1 8. 1 {x/x1 , cE noch/z1 } 6 P red(x, cE noch); : 1.9) ìP ar(x, cE noch) ìP ar(x, cAbel). 1.9 P ar(x, cE noch), P ar(x, cAbel). (b) 1í7, , , ( ) P ar(x, cE noch) 1.9. 1 {cC ain/x}. SLD- 5, 2 5 1.9 1.10) ìP ar(cC ain, cAbel), P ar(cC ain, cAbel). (c) 1í7 , , P ar(cC ain, cAbel). , . (b) ( ), P ar(x, cE noch) 1.9: (b) 5, . , 5, , ( ) P ar(x, cE noch).
10 , , .


4.

173

(a) ( ), P red(x, cE noch) 8: (a) 6, . , 6, , ( ) P red(x, cE noch). 7 ) P red(x2 , z2 ) P ar(x2 , y2 ), P red(y2 , z2 ), 7. SLD- 7 8. 2 1 {x/x2 , cE noch/z2 } 7 P red(x, cE noch); : 2.9) ìP ar(x, y2 ) ìP red(y2 , cE noch) ìP ar(x, cAbel). 2.9 P ar(x, y2 ), P red(y2 , cE noch), P ar(x, cAbel). (d) 1í7 , ( ), P ar(x, y1 ) 2.9. 1, 2 {cAdam/x, cC ain/y2 }. SLD- 1 2.9 2 2.10) ìP red(cC ain, cE noch) ìP ar(cAdam, cAbel). (e) , , , 6 ( 6, ): 6 ) P red(x3 , z3 ) P ar(x3 , z3 ), P red(cC ain, cE noch) 2 {cC ain/x3 , cE noch/z3 }. . 3 SLD- 6 2.10: 2.11) ìP ar(cC ain, cE noch) ìP ar(cAdam, cAbel). (f ) , , SLD- 5 2.11, 2 4 {}: 2.12) ìP ar(cAdam, cAbel). (g) , , SLD- 3 2.12, 2 5 {}: 2.13) .


174 . . , SLD- (1, . . . , 8, 2.9, . . . , 2.13) 1í8. 22222 1 2 3 4 5 , {cAdam/x}, , , . , SLD- , (. 4.5.6 4.5.7). , , ( SLD- ), ( ) , ) , ) G G , G G , C , G C G G, , .

, , . 4.9.

P red(x, cE noch), P ar(x, cAbel) {x/x1 , cE noch/z1 } {cC ain/x} 5 P ar(cC ain, cAbel) 6 7 {x/x2 , cE noch/z2 } 1 {cAdam/x, cC ain/y2 } P red(cC ain, cE noch), P ar(cAdam, cAbel) 6 {cC ain/x3 , cE noch/z3 } P ar(cC ain, cE noch), P ar(cAdam, cAbel) 5 {} P ar(cAdam, cAbel) 3 {} . 4.9. SLD-. , , ( , (c)) , - {cE v e/x}. 4.5.5. . P ar(x, cE noch), P ar(x, cAbel) P ar(x, y2 ), P red(y2 , cE noch), P ar(x, cAbel)

4.5.3.
,


4.

175

. search, . , - , . ( ), , . Prolog se a r ch. P {C1 , . . . , Ck },

1, 2, . . . , k . search search(G), G (G1 , . . . , Gn ): (1) n = 0, . (2) i = 1, . . . , k . (2.1) Ci . Ci B A1 , . . . , Am (m 0), G. (2.2) B G1 , . (2.2.1) B G1 . (2.2.2) search(A1 , . . . , Am , G2 , . . . , Gn ) , . (3) . search SLD- S (. () 4.5.2). , . SLD- , . , search. B A1 , . . . , Am (m 0) B , A1 , . . . , Am . G1 , . . . , Gn G1 , . . . , Gn . G1 ( ) B A1 , . . . , Am , B G1 , A1 , . . . , Am , G2 , . . . , Gn . , SLD-. 4.5.6 ( ). P G (G1 , . . . , Gn ). search(G) , P G .


176 . . . l search(G). (l = 1) . . search(G), l > 1 . . B ìA1 . . . ìAm , ( ) B A1 , . . . , Am P , ìG1 . . . ìGn , G1 , . . . , Gn , SLD (ìA1 . . . ìAm ìG2 . . . ìGn ), B G1 . G search(G), . = . (A1 , . . . , Am , G2 , . . . Gn ).

search(G) , l, , search(G) P G , . . P (A1 . . . Am G2 . . . Gn ) . ()

, m > 0 ( , m = 0, ). B A1 , . . . , Am P , , P (A1 . . . Am ) B .

B G1 , P ( ) P . . P G . (G1 G2 . . . Gn ) , (A1 . . . Am ) G1 ,

4.5.7. , SLD- S (. () 4.5.2) , search. SLD- S P . , search , , search(G) , P G. 4.5.6 , . . , . . .


4.

177

4.5.8. P G , P G, ( ) . , ? , , search , , P G : P G, search (G) , P G; search (G) . , , search, . Prolog, - . search (. . ) ( ). Prolog ( ) , . 4.5.9. search , . . , P add P mult , P add(x, y , z ) x y z , P mult(x, y , z ) x y z . , 0 , S , 0 0, S . , , : 1) P add(x, 0, x), 2) P add(x, S (y ), S (z )) P add(x, y , z ), 3) P mult(x, 0, 0), 4) P mult(x, S (y ), z ) P mult(x, y , u), P add(u, x, z ). 1 2 , : 1 , x + 0 = x,


178 . . 2 x + S (y ) = S (x + y ). 3 4 , : 3 , x § 0 = 0, 4 x § S (y ) = x § y + x. P mult(S (S (0)), S (S (0)), x), 2 § 2, {S (S (S (S (0))))/x}, P mult(x, S (0), S (S (0))), x § 1 = 2, {S (S (0))/x}. 4.5.10. . 4.5.11. , , , , , , () .


5.


( ) , , - , . , , , , , . , , .1 , , , , .

5.1.
(), . , , . , , . . . , , . , , , . , , . ‡ , ,
1 , 3.5.5.

179


180 . . . . ) , ( ) () , ) , , , . , ( ) . : 1) , 2) (2 ) , 3) - ( -), 4) . ( ) , 5.1.5. , : , , . ( - ); - . - . (, ), .

5.1.1.
. , . , .
2 .

. . -


5.

181

, . () . , , . . X , Y , X , X X . f X Y X Y . X = , f . , f X Y , p f :X Y. 5.1.1. , , , S, q0 , F, P , 1) , ( ) , _, ( ), ; 2) , ( ) , \ {_}; 3) , , \ {_};

4) S , ( ), S , S = ; 5) q0 S 6) F S , ; ;

7) P (S \ F ) ½ S ½ ½ {L, C, R}, . M , , , S, q0 , F, P

5.1.1. q , r S , a, b . P (q , a) = r, b, L q a rbL, P (q , a) = r, b, C q a rb, P (q , a) = r, b, R q a rbR; . P , . ( ) U q aV , q S , a , U, V . , a ( ) q . , q U . , q F .


182 . . 5.1.2. X U q aV . X , Y , : 1) P , q a, Y ; 2) P q a rb, Y = U rbV ; 3) P q a rbR, ) V , Y = U brV ; ) V , Y = U br_;3 4) P q a rbL, ) U ( U = U c U c ), Y = U r cb V ; ) U , Y = r_bV .3 , 2í4 X , Y X M . , Y X , X Y . 5.1.3. , . , M ( M ) M () = , Z0 , . . . , Zn (n 0), : 1) , Z0 = q0 , Z0 = q0 _; 2) i = 1, . . . , n Z
i-1

Zi ;

3) Zn = U q W q F U, W ; 4) , W . , M (M , M , M ) !M (), M . ½ . . . ½ , 1 , . . . , n , 0 , n N+ . 1 n 0 5.1.4. # , 1 , . . . , n \ {#}, 0 p f : ½ . . . ½ . , M n 1 0 f , :
3 , .


5.

183

1) 1 , . . . , n : f (1 , . . . , n ) 1 n , !M (1 #2 # . . . #n ); 2) 1 , . . . , n : f (1 , . . . , n ) , 1 n f (1 , . . . , n ) = M (1 #2 # . . . #n ). , , . 5.1.5. n N+ M , n- 1 , . . . , n M (1 # . . . #n ), !M (1 # . . . #n ), n- . , . , . n N+ Nn N . n- f , dom(f ) = Nn . x x x || . . . | ( {|}), x |; 0 . p f : Nn N p f : ({|} )n {|} , x1 , . . . , xn , x N f (x1 , . . . , xn ) = x f (x1 , . . . , xn ) = x

( , f (x1 , . . . , xn ) f (x1 , . . . , xn ) ). , M f , M f . , , . 5.1.6. , , . M , {|, #}, {|}. 5.1.7. ( 5.1.5.) n N+ M , n- x1 , . . . , xn M (x1 # . . . #xn ) ( | ), !M (x1 # . . . #xn ), n- . x1 , . . . , xn , y M (x1 , . . . , xn ) M (x1 # . . . #xn ) M (x1 , . . . , xn ) = y M (x1 # . . . #xn ) = y . 5.1.8. M+ , f (x, y ) = x + y . {|, #} {|} . , {_, #, |}


184 . . M+ , {q0 , q1 , q2 , q3 , qf } , q0 . , {qf } M+ : 1) q0 | q0 |R, 2) q0 # q1 |R, 3) q1 | q1 |R, 4) q1 _ q2 _L, 5) q2 | q3 _L, 6) q3 | q3 |L, 7) q3 _ qf _R. . || . . . |#|| . . . |. , # |, | _. . q0 || . . . |#|| . . . |. q0 ( 1) | #. , 2, # | q1 . ( 3) _, |, ( 4) , q2 . ( 5) | _ ( , | #) q3 . ( 6) _, |. , ( 7), qf . |, qf , M . , , M+ : q0 ||#| ||q3 |__
1

|q0 |#| 1 ||q0 #| 2 |||q1 | 3 ||||q1 _ 6 |q3 ||__ 6 q3 |||__ 6 q3 _|||__

4 7

|||q2 |_ 5 _qf |||__ .

, , . , M+ f , f ; . , M+ . , M+ q1 # q2 #L, g (x, y , z ) = x + y . 5.1.9. 5.1.8, , M+ f . 5.1.10. , ( ) . 5.1.11. , () , , , ;


5.

185

, 1, {a, b} ( . 1.2.2 . 32), 0 . 5.1.12. , .

5.1.2.
. . 5.5.1, . , § . ( ) § , , . , . . , . A 1) 1 1 1 , ... n) n n n , i = 1, . . . , n i , i , i § . , A , A() A . i, i , A() ; i , i . i i ; . i = § (. . i- ), A() ; (. . i- ) A() A( ), . . , . , A . , A (A ) !A(), A . , . ( , \ , .) A , # , 1 , . . . , n \ {#}, p f : ½ . . . ½ . , A 1 n f , :


186 . . 1) 1 , . . . , n : f (1 , . . . , n ) 1 n , !A(1 #2 # . . . #n ); 2) 1 , . . . , n : f (1 , . . . , n ) , 1 n f (1 , . . . , n ) = A(1 #2 # . . . #n ). , , . (. 5.1.1) ( ). 5.1.13. 1. A {a, b, c, d} ab § bac, ( ) . A ab bac, , . 2. ( ). 3. § ( ). 4. , a, § a a . 5. {|, #} # , , f (x, y ) = x + y g (x, y , z ) = x + y + z . 5.1.14. A, ba {a, b}. q , q , q ba. A {a, b, q } ( {a, b}) : 1 ) q a aq , 2 ) q b bq , 3 ) q § ba , 4) q . A: ab b
4

q ab b

1

aq b b

2

ab q b

2

ab b q

3

ab b b a .

, . , - (. 5.5.7 . 231). 5.1.15. f . f , f .


5.

187

5.1.16. , , 5.1.11. 5.1.17. , 1, (. 1.1.3 . 13), 0 .

5.1.3. - -
. , (, ) , (. 4.5). -. - (. 1.2). . , , , . - , , . () , -. , . -, , . , , f , , f (x) = x + 2. f . , f x.(x + 2), , x x + 2. , : y .(y + 2). f , f (x): x.f (x), , a (x.f (x))(a) = f (a). , f , f (x, y ), x y . x fx , y


188 . . fx (y ) = f (x, y ). , fx y .f (x, y ). f x.fx (y ) = x.(y .f (x, y )), xy .f (x, y ). . . . 5.1.3 , , , 5.1.3. - - -. V ars, 1.1.3. f , v , w, x, y , z , , . - (-, - ) : 1) ; 2) M , x , (xM ) , , M (- ); 3) M N , (M N ) , M N . . , . -, (x1 (x2 . . . (xn M ) . . .)) x1 x2 . . . xn .M , , M (M ), x1 x2 . . . xn .M . -, (((M1 M2 )M3 ) . . . Mn ) M1 M2 . . . Mn . , , , . 5.1.18. : x, xx (xx), yx (y x), x.y x (x(y x)), xy .y xz .z xy .y x (x(y (y x))), (xy .y x)z .z ((x(y (y x)))(z z )), (x(y ((y x)(z z )))).

, - , (. 2.1.2), . , x y , z , (x.xy )(z .(y .x)z x), , . - .


5.

189

, (. - N 2.3.1), [M ]x N x - M , , - N x M ( N x M ). - . x - x.y , x y . S ub(M ) - M : 1) M x, S ub(M ) = {x}, 2) M x.N , S ub(M ) = S ub(N ) {x.N }, 3) M N1 N2 , S ub(M ) = S ub(N1 ) S ub(N2 ) {N1 N2 }. - N - M , N S ub(M ). M = N , M N . - , - ( - ). - . ; L, M N -, x y . - , : 1) x.M = y .[M ]x , y M ( y - );
x 2) (x.M )N = [M ]N , N x M ( - );

3) M = M . - : M =N , N =M M =N , LM = LN M =N , ML = NL M =N . x.M = x.N

L = M; M = N , L=N

M = N - M = N . L = M M = N , L = M = N . ( 5.1.3) ‡ =. , - M N ( M N ), M = N . , -.


190 . . , - , . , 2.6.37 . 5.1.19. M , N N -, M N M N , . N = N , M = M . 5.1.20. 5.1.19. - , -. - ( 5.1.19 , ). - , . , , . , - -, ( , 2.3.2). 5.1.3 , . 5.1.21. : (x.(y .xy ))(z .y z ) = (x.(v .xv ))(z .y z ) = v .(z .y z )v = v .y v . , , - (x.(y .xy ))(z .y z ) = v .y v . (x.xy )(z .z ) = (z .z )y = y , (x.x)(x.x)y = (x.x)y = y . , = ( -: , ). - (x.xy )(z .z ) = (x.x)(x.x)y . 5.1.22. ( -) () 5.1.21. ( , - , . . . () () , 3.1.6), () :


5. -

191

(x.M )N 4 . , , . N M , N M . M , , M . , , . 5.1.23. v .y v . (x.(y .xy ))(z .y z ) , v .y v (. 5.1.21), w.y w x.y x, . (x.xy )(z .z ), (x.x)(x.x)y y (. 5.1.21). - (x.xx)(x.xx), . , . , . , -, . . . - , - . T F xy .x, xy .y .

-, T F, . , T F . B , M N , B , M , N B M N . , TM N = M , FM N = N . X Y , - X Y X . X Y X , T, Y , , Or
4

xy .xTy ,

red ucible ex pression .


192 . . Or F F = F, Or F T = T, Or T F = T, Or T T = T. , Not x.xFT Not F = T, Not T = F. 5.1.24. -. M N [M , N ] x.xM N ,

x M , N . [M , N ]T = M , [M , N ]F = N , [M , N ] M N . n n : 0 n+1 x.x, [F, n].

, . Succ Pred IsZero x.[F, x], x.xF, x.xT,

, n Succ n = n + 1, Pred n + 1 = n, IsZero 0 = T, IsZero n + 1 = F. , , , .


5.

193

. , . - , . , . -. 5.1.25 ( ). (a) F X , X = F X . (b) Y f .(x.f (xx))(x.f (xx)). () F YF = F (YF ). . (a) W W W . F , X y .F (y y ), y

X = W W = (y .F (y y ))W = F (W W ) = F X. (b) (a) X , X = YF , 5.1.19 YF = F (YF ). X = F X;

F ; X , X = F X , F . Y , : Y F = F (Y F ) F . , Y (. ( ) 5.1.25) . -. c , M , M f , . F f .M , f , F . YF . , F (YF ), (f .M )(YF ). M f YF , , . , , . 5.1.26. Add , m n Add m n = m + n. , Add(x, y ) x y ( ) : I sZ ero(y ), x, S ucc(Add(x, P red(y ))),


194 . . I sZ ero , , S ucc P red . Add , Add x y = (IsZero y ) x Succ(Add x (Pred y )). , Add , Add = xy .(IsZero y ) x Succ(Add x (Pred y )), Add , Add = (f xy .(IsZero y ) x Succ(f x (Pred y )))Add. Add Y(f xy .(IsZero y ) x Succ(f x (Pred y ))). 5.1.27. Add 2 1, Add 2 1 = 3, Add , . 5.1.28. Mult, Exp Tsub , m n Mult m n = m § n, Exp m n = mn ( 00 = 1, [7]), Tsub m n = m - n, m - n, m n, m-n= 0, m < n. 5.1.29. Sub , m n Sub m n = m - n, m n, Sub m n .

- f : Nk N - (- ), F , n1 , . . . , nk N F n1 . . . nk = f (n1 , . . . , nk ), f (n1 , . . . , nk ) , F n1 . . . nk , f (n1 , . . . , nk ) . 5.1.30. f . f , f . , . , - , , , .
p


5.

195

5.1.4.
5 , . , , . : 1) - o, o(x) = 0 x N; 2) s, s(x) = x + 1 x N;
n 3) n N+ m = 1, . . . , n Im , n Im (x1 , . . . , xn ) = xm x1 , . . . , xn N.

5.1.4 m, n N+ , . () n- f g x1 , . . . , xn N f (x1 , . . . , xn ) = g (x1 , . . . , xn ), , . , . : m- f n- f1 , . . . , fm . n- g , x1 , . . . , xn N g (x1 , . . . , xn ) = f (f1 (x1 , . . . , xn ), . . . , fm (x1 , . . . , xn )), f1 (x1 , . . . , xn ), . . . , fm (x1 , . . . , xn ) , g (x1 , . . . , xn ) . , g ( ) f , f1 , . . . , fm . : n- f (n + 2)- g . (n + 1)- h , x1 , . . . , xn N h(x1 , . . . , xn , 0) = f (x1 , . . . , xn ), x1 , . . . , xn , y N h(x1 , . . . , xn , y + 1) = g (x1 , . . . , xn , y , h(x1 , . . . , xn , y )), h(x1 , . . . , xn , y ) , h(x1 , . . . , xn , y + 1) . , g f g . n = 0. a , g . , h , a, g , h(0) = a,
5

.


196 . . y N h(y + 1) = g (y , h(y )), h(y ) , h(y + 1) . , . 5.1.31. ( ), . , . . 5.1.32. on : Nn N, 0, . , x1 , . . . , xn N
n on (x1 , . . . , xn ) = o(I1 (x1 , . . . , xn )). n , on o, I1 . 5.1.33. a . g n : Nn N, a, . , x1 , . . . , xn N

g n (x1 , . . . , xn ) = s(s(. . . s(on (x1 , . . . , xn )) . . .)), a s. , g n () s on . 5.1.34. add(x, y ) = x + y . , x, y N
1 add(x, 0) = x = I1 (x), 3 add(x, y + 1) = add(x, y ) + 1 = s(add(x, y )) = s(I3 (x, y , add(x, y ))). 1 , add I1 g , g 3 3 s, I3 : g (x, y , z ) = s(I3 (x, y , z )). 5.1.35. , x - y (. 5.1.28 . 194) . , x - 1 . x N

0 - 1 = 0 = o(x), 2 (x + 1) - 1 = x = I1 (x, x - 1).
2 , x - 1 o I1 . , x, y N 1 x - 0 = x = I1 (x), x - (y + 1) = (x - y ) - 1. 1 x - y I1 g (x, y , z ) = z - 1, g , , .


5.

197

5.1.36. |x - y | ( x y ) , x, y N |x - y | = (x - y ) + (y - x), , u + v , u - v . (n + 1)- f . n- g , x1 , . . . , xn N : y N , f (x1 , . . . , xn , y ) 0, y < y f (x1 , . . . , xn , y ) 0, g (x1 , . . . , xn ) = y ; y , g (x1 , . . . , xn ) . , g f g (x1 , . . . , xn ) = ²y (f (x1 , . . . , xn , y ) = 0). , , . , ( ). , , . , . 5.1.37. ( ) f (x, y ) = s(x) + y . , g (x) = ²y (f (x, y ) = 0) . 5.1.38. , sub(x, y ) = x - y, x y, , x < y,

. g (x, y , z ) = |x - (y + z )|, . sub(x, y ) = ²z (g (x, y , z ) = 0). - , , Pascal ( , ), . . - , , , , . : . , . 5.1.39. f . f , f . . ( ) , , .


198 . . 5.1.40. , : sg (x) = 0, x = 0, 1, x = 0; b(x) = 0, b(x) = 0,

mult(x, y ) = x § y ; h(x) = b, f , g f (x), g (x),

; x y, y = 0, x, y = 0; x y , y = 0, x, y = 0;

mod(x, y ) = div (x, y ) =

p(x) = x- (p(0) = 2, p(1) = 3, p(2) = 5, . . .).

5.1.41. , : x/y , y = 0 y x, f (x, y ) = . 5.1.42. , , , .

5.1.5.
(. 5.1.15, 5.1.30, 5.1.39). . 1936 . . , : -, . (. . ) . 5.1.30 : . ( ): . , (, , ). , , . , -, , . ,


5.

199

, , , . , , (), . , ( ). , , . , . , , , . 5.1.43. , ( ), . , , . 5.2.4. : ? , , . ( , ) . . , , 2, . f : N N , x N f (x) = 1, , 0 .

, . f 0 1, f0 f1 , x N f0 (x) = 0 f1 (x) = 1, , , f . f , , ; , f : , 1, , 0. , f , , , ( ; . 2.6.23).


200 . . , , , . . (. 2.5.7), (, ) .

5.2.
, , .

5.2.1.
5.2.1. A N A : N N, A (x) = 1, x A, 0, x A. /

5.2.2. A N ( ), A . , A N , , x , x A . 5.2.3. , N, , , . , , , . , , . , A B . , MA MB , A B . A\B A \ B : x MA (x), MB (x); MA (x) 1, MB (x) 0, 1, 0. . 5.2.4. p A N : N N, A (x) = A 1, x A, , x A. /


5.

201

5.2.5. A N ( , ), . A , A N , , x 1, x A, . , A . , M , A , M , , A : x M (x), M (x) 1, 1, . , 5.4.5. 5.2.6. . . A B . MA MB , A B . B : x A MA (x) MB (x), , MA (x) MB (x) , 1. B : x A MA (x) MB (x), , MA (x) MB (x) , ; , 1. (. 5.4.5 5.4.6), A , N \ A . 5.2.7 ( ‡). A N. A , A N \ A . . A , N \ A, , . , A N \ A . M M , \A . A N M , x N M (x) M (x), , M , M 1, M , M 0. x N M M x , M A . , A . 5.2.8. A N. : (a) A ; (b) A = dom() : N N;
p


202 . . (c) A = A = rng (f ) f : N N; (d) A = rng () : N N. . (a) (b). A , dom( ) = A, A A (b). A , A = dom() p : N N. M , . M , : x M (x) ( ) 1. , M , A . A (a) (c). A . j0 A. f , A x N: 1. A x B ( B ): i = 0, 1, 2, . . . i + 1 (0), (1), . . . , (i). A A A 2. x- B (j ) A j ( j ), A j , j0 . A, f , x N f (x) dom( ) = A, j A x N, A f (x) = j . rng (f ) = A f (c). , (c). A , A . A = rng (f ) f : N N. (x) A : x i = 0, 1, 2, . . . f (i) , x, 1. , A . (c) (d). (c). A = , A , . A = , A = rng (f ) f : N N, (d). , (d). , (d) (c), , (a) (c), , f , . A (c) 5.2.8 () . , (, ) f (0), f (1), f (2), . . . , f ( ). 5.2.9. A , B , f : N N . A B f ?
p


5.

203

5.2.2.
N. . n- . . N2 0, 0 , 0, 1 , 0, 2 , 0, 3 , . . . 1, 0 , 1, 1 , 1, 2 , . . . 2, 0 , 2, 1 , . . . 3, 0 , . . . ... , : 0, 0 , 0, 1 , 1, 0 , 0, 2 , 1, 1 , 2, 0 , 0, 3 , 1, 2 , . . . . ()

x, y ( 0) c(x, y ) ( ) . c : N2 N, , . , . c N2 N. c . , c. x, y (x + y )- x- ( 0). 1 + 2 + . . . + (x + y ) . , c(x, y ) = 1 + 2 + . . . + (x + y ) + x = (x + y )(x + y + 1)/2 + x. l r N N, z , , z . , l : z i = 0, 1, 2, . . . i- x, y () , c(x, y ) = z , x. r . l r , x, y , z N l(c(x, y )) = x, r (c(x, y )) = y c(l(z ), r(z )) = z .

c, l, r . 5.2.10. l r . n- , n N+ c(n) : Nn N , c(1) (x1 ) = x1 , c
(n+1) (n)

(x1 , . . . , xn , xn+1 ) = c(c

(x1 , . . . , xn ), xn+1 ).


204 . . , c(n) . c(n) (x1 , . . . , xn ) ( ) n- x1 , . . . , xn . , c(2) = c. n N+ m = 1, . . . , n (n) cm : N N, z (2) (2) m- n- z . , c1 = l c2 = r. 5.2.11. c
n (n) m

l r .

R N (, ), c(n) (R) ( R c(n) ) (, ) . (, ) , , . (, ) (, ). . : R Nn , R Nn \ R . R Nn R R , 5.2.1 5.2.4, n- . 5.2.12. R Nn . , R c(n) (R) . 5.2.13. , R Nn (, ) , R (, ) . R 5.2.14. , n- , , (n + 1)- , ? 5.2.15. , n- , , (n + 1)- , . Nn . (, ), (, ) N, (. 2.2.2). (, ) (, ) , .

5.2.3.
( 5.2.8) : .


5. 5.2.16. X , R X , n 2. { x1 , . . . , xj
-1

205 n-

, xj

+1

, . . . , xn X n-1 | xj ( x1 , . . . , xj

-1

, xj , xj

+1

, . . . , xn R)}

R j - . 5.2.17. R Nn , R Nn+1 , R R (n + 1)- . . R , R c(n) (R). , R M . x1 , . . . , xn Nn : x1 , . . . , xn R, c(n) (x1 , . . . , xn ) R , !M (c(n) (x1 , . . . , xn )). R Nn+1 , x1 , . . . , xn , xn+1 R, M c(n) (x1 , . . . , xn ) xn+1 . , R , !M (c(n) (x1 , . . . , xn )) xn+1 , x1 , . . . , xn , xn+1 R. R R (n + 1)- . 5.2.18. R Nn , n R . 2,

. Q R n- , . (d) 5.2.8. c(n) (R) = rng () p : N N. c(n-1) (Q) = l(c(n) (R)) = rng (l ), l l , , c(n-1) (Q) Q . 5.2.19. . 5.2.20. , . .

5.2.4.
. .


206 . . . 0. , k (k 1). 1, 2, . . . , k i ai . aij . . . ai1 ai0 () = i0 + i1 § k + . . . + ij § k j . k N+ n N+ n = i0 + i1 § k + . . . + ij § k j , il {1, 2, . . . , k } l = 0, 1, . . . , j . , : N, , . , , . , , . L (, ), (L) (, ) . R ½ . . . ½ , 1 n 1 , . . . , n , n 1. 1 , . . . , n , n 1. R ½ . . . ½ (, 1 n ), { (1 ), . . . , (n ) Nn | 1 , . . . , n R} (, ) N. 5.2.2, . , . 5.2.21. , , . R R R , 5.2.1 5.2.4, n- . 5.2.22. , R (, ) , R (, ) . R
1 ½ . . .½ n . (, ), (, ) , (. 2.2.2). (, ) (, ) , .

5.3.
, , -


5.

207

. (, ) . -, , . , , . . , . . , .

5.3.1.









f : N . x N f (x) = , x ( f ). , . n N+ n- () . () . , , , _, # |, . , , , . , , , , {b0 , b1 , . . .}. 0 , bi i, -. , , , 0 , . . ( , 5.1.1, , .) M , (M 0 ), , . , M , M 0


208 . . , 6 . x 0. 0 . , , M , , , x; , , , x 1; . ( , , .) , , . p 0 : N M. , 0 : M N 0 M. M (M ). -1 : N M, , . x M , (M ) = x. , , , x- , . , -1 , M. , N M. M, ( , ). -1 . M (M ) ( ) . x N Mx , x. (n) x n- () , Mx . x ( (n) ) x . , n N+ n- : (n) x Mx x . , . (1) x x . 5.3.1. , . n- , n- , n N+ n- . . , , .
6 M , .


5.

209

. , , f . , x N f (x) = x (x) + 1, x (x) , 0, x (x) .

f (x) x (x) x, , f , f . . x ( x (y ) , x (y ) ): 0 (0), 0 (1), 0 (2), . . . 1 (0), 1 (1), 1 (2), . . . 2 (0), 2 (1), 2 (2), . . . ... x f (x) , f (x) x (x), .

5.3.2.
U , () , . . , . U x y1 , . . . , yn (n 1). x U Mx ; Mx (y1 , . . . , yn ), Mx y1 , . . . , yn ; Mx ( ), Mx (y1 , . . . , yn ). , U , : n N+ x, y1 , . . . , yn N U (x, y1 , . . . , yn ) = Mx (y1 , . . . , yn ). ( = , , .) U ( ). - . -, 5.1.3, -.


210 . . . , u0 , v0 g xy .g (u0 , v0 , x, y ). g uv xy .g (u, v , x, y ). . n N+ U (n) (n + 1)- U , : x N
( y1 . . . yn .U (x, y1 , . . . , yn ) = xn) . (n) (n)

()

, , U . 5.3.2. C n- . (n + 1)- C , : 1) x N y1 . . . yn . (x, y1 , . . . , yn ) C ; 2) C x N , y1 . . . yn . (x, y1 , . . . , yn ) = . , () , U () n- . . 5.3.3. . n N+ , n- . U U . , , . () , n- . , . : , n- , ? . 5.3.4. , n- , . . , , n- , . y1 . . . yn .( (y1 , y1 , y2 , . . . , yn ) + 1) . x0 N, y1 . . . yn . (x0 , y1 , . . . , yn ) = y1 . . . yn .( (y1 , y1 , y2 , . . . , yn ) + 1). , y1 . . . yn . (x0 , y1 , . . . , yn ) . y1 , . . . , yn x0 , (x0 , . . . , x0 ) = (x0 , . . . , x0 ) + 1,
(1) (n)


5.

211

, , (x0 , . . . , x0 ) = (x0 , . . . , x0 ) + 1. , . 5.3.5. , n N+ , () n- .

5.3.3.
f , xy .f (x, y ). a y .f (a, y ) . , b y y .f (a, y ), f (a, b). , , f a, y .f (a, y ). , , f a y .f (a, y ). . 5.3.6 ( , s-m-n-). m, n N+ sm : Nm+1 N , n x, y1 , . . . , ym N
( z1 . . . zn .xm +n)

(y1 , . . . , ym , z1 , . . . , zn ) = sm

(n) n (x,y1 ,...,ym )

.

. , sm . x, y1 , . . . , yn n : 1) M , z1 , . . . , zn (m+n) x (y1 , . . . , ym , z1 , . . . , zn ), Mx y1 , . . . , ym , z1 , . . . , zn ; 2) M . , x, y1 , . . . , y (m+n) z1 . . . zn .x (y1 , . . . , ym , z1 , . . . , zn ).
n

5.3.7. m, n N+ p g : Nm+n N s : Nm N , y1 , . . . , ym N z1 . . . zn .g (y1 , . . . , ym , z1 , . . . , zn ) = s(
(n) y1 ,...,ym )

.

. . x0 N g = x0 s y1 . . . ym .sm (x0 , y1 , . . . , ym ). n

(m+n)


212 . .

5.4. .
, ()7 , .

5.4.1.
, . ( ) , , . , x y ? x y . . , 2 3 ? 2 4 ? . (x1 , . . . , xn ) x1 , . . . , xn , , , x1 = k1 , . . . , xn = kn 1, (k1 , . . . , kn ) , 0, . , , () ; , () . . ( ), . , , , . (. 5.2.2 5.2.4, 2.2.2), n- X1 ½ . . . ½ Xn S


{ x1 , . . . , xn X1 ½ . . . ½ Xn | (x1 , . . . , xn ) },

. , , S , . , ) , , ) M , M . 5.4.1. : 1) 2) x x N ( {x N | x } ); x y x, y N ( { x, y N2 | x y } );

7 , , . , , .


5. 3) 4) 5) x x , { a, b } ( {x | x } );

213

x 5 x N; x y , t x, y , t N.

5.4.2. 1í3, . , 4 5.

5.4.2. ,
, ( ). x y , Mx y . : x (y ) x, y N. , ; , , x y , Mx y . . x , Mx x . : x (x) x N. 5.4.3 ( ). x (x) x N . . , . , . , x N (x) = 1, x (x) , 0, x (x) .

, . f , x N f (x) = , (x) = 1, 0, (x) = 0.

f , , , , , f , : x, (x) = 0, 0, .


214 . . f x0 : f = x0 . x f x0 , x0 (x0 ) = f (x0 ) = , x0 (x0 ) , 0, x0 (x0 ) .

, : x0 (x0 ) , x0 (x0 ) . , . 5.4.4 ( ). x (y ) x, y N . . , . . , x, y N (x, y ) = 1, x (y ) , 0, x (y ) .

, x.(x, x), N, . , 5.4.3. . , , , , M x , M x . , 5.1.8 ||#| || . . . |#|| . . . | . K {x N | x (x) }. 5.4.1, , , . , 5.4.3 : K . K 5.4.5. K . 5.4.3. , . K 5.2.8 K , x.U (x, x), U ( . 5.3.2) , x (x) = U (x, x) x N.

, .


5. 5.4.6. {x N | x (x) } = N \ K .

215

. N \ K , , K , (. 5.2.7) , K , . , , x , x . 5.4.7 ( ). x x N . . , , . . , x N (x) = 1, x , 0, x .

. f , , , . f , x N f (x) = x (x) + 1, (x) = 1, 0, (x) = 0.

f : x, (x) = 1, U (x, x) + 1 , 0. , f , . x , f x , f (x) = x (x). , : f , .

5.4.3.
5.4.4 , . 5.4.3. . . , , ,


216 . . . , , . ‡ . . , ( , ) . : , , , ? . 5.4.8. x = 0 (. . x , 0 ) x N . . . , , . . , x N (x) = 1, x = 0, 0, x = 0.

f , x, y N f (x, y ) = 0, x (x) , , x (x) .

f : x y U (x, x) 0. 5.3.7 s : N N , x N y .f (x, y ) = s(x) . x, y N s(x) (y ) = 0, x (x) , , x (x) .

, x N : s(x) = 0 , x (x) . s , x.(s(x)), x N (s(x)) = 1, x (x) , 0, x (x) .

, x.(s(x)) , 5.4.3 . , , .


5.

217

, , . , , x = 0 x. h x: 1) s(x) , y : U (x, x) 0 ; 2) s
(x )

.

x : s(x) y 0, U (x, x) = x (x) . , h , .

5.4.9. . ,

x = y

x, y N -

. , x = 0 , 5.4.8, . . , , x, y N (x, y ) = 1, x = y , 0, x = y .

y .0 y0 . x.(x, y0 ) x = 0 , 5.4.8. 5.4.10. , a N x (a) x N . 5.4.11. , a N a rng (x ) x N . 5.4.12. , x x N . 5.4.13. , dom(x ) = x N . , . C (1) () . 5.4.14 ( , -). C C (1) . C = C = C (1) , x C x N .


218 . . . x C x C (1) \ C , , , , C ( x C x C (1) \ C ). C = , C . 5.4.8. , , . . , x N (x) = 1, x C , 0, x C . /

f , x, y N f (x, y ) = (y ), x (x) , , x (x) .

f : x y U (x, x), (y ). 5.3.7 s : N N , x N y .f (x, y ) = s(x) . x N : 1) x (x) , s(
x)

= , , s(
x)

x)

C;

2) x (x) , s( , s(x) C . /

,

, x.(s(x)) , 5.4.3 . . . , C , . , , x C x. h x: 1) s(x) , y : U (x, x), (y ) ; 2) s
(x )

.

x , s(x) , C , U (x, x) = x (x) . , h , . C , C (1) ,


5.

219

C (. 2.2.2). , C = C = C (1) , , , , , . : . , 5.4.8 x = 0 . , y .0, : y .0 , y .1 . . : ( , - ) . : , , , , . , ( ) . : , , , . : . , 0 . 5 , ( , 5.4.1 5.4.2). 5.4.15. , 5 , , : 5 , , 5. 5.4.16. , rng (x ) y x, y N . . , y , .

5.4.4. m- m-
(. 5.4.3). , , . , .


220 . . . . , x N {x N | (x) }. . 5.4.17. , A N m - ) B N, A m B , f : N x N : x A , f , m- A B . ( N , f (x) B .

5.4.18. m- ( ) many-one reducibility , , f . , m- f . : K {x N | x (x) }. 5.4.19. 1. 5.4.8 s, m- K {x N | x = 0}. 2. (. 5.4.14) s, m- K {x N | x C }, C , . 3. x.c(x, x) m- N {y N | x(y = c(x, x))}, c , 5.2.2. 4. K
(2)

{ x, y N2 | x (y ) }

. 5.4.4 . K , , m-, K (2) m- K , K (2) . K (2) c, K
h

{c(x, y ) | x (y ) },

{z N | xy (z = c(x, y ) x (y ) )}. x.c(x, x) m- K Kh . 5. 5.4.9 x = 0 x = y . y0 y .0. x.c(x, y0 ) m {x N | x = 0} {c(x, y ) | x = y }, {z N | xy (z = c(x, y ) x = y )}.


5. m-. 5.4.20. A, B , C

221

N.
m

(a) A m A (. . m ); A A m C (. . m ); (b) A (c) A (d) A
m m m

BB

m

C,

B , N \ A

m

N \ B;

B B , A ; B B , A ;
m

(e) A , B = B = N, A (f ) A (g) A (h) N (i)
m m m m

B;

N , A = N; , A = ; A , A = ; A , A = N.

. (a) x.x m- A A. f m- A B g m- B C , x.g (f (x)) m- A C . (b) , m- A B , m- N \ A N \ B . (c) f m- A B B B . x.B (f (x)) A. (d) f m- A B B B . x. (f (x)) B A. (e) b B c N \ B f , x N b, x A, f (x) = c, x A. / A , f . , x N : x A, f (x) B . , f m- A B . (f )í(i) . 5.4.21. (f )í(i) 5.4.20. m-, 5.4.20, , m- . 5.4.22. , N \ K
m

K , , K

m

N \ K.

. 5.4.5 K , 5.4.6 N \ K . , (d) 5.4.20 , N \ K m K . (b) 5.4.20 , K m N \ K .


222 . . 5.4.23. , K m- , 5.4.10í5.4.13. , N , m- N. , : (c) 5.4.20, , N . , Kh , 5.4.19. 5.4.24. Kh A A N.
m

Kh -

. K (2) ( 5.4.19), , , K (2) U ( , . 5.3.2). Kh = c(K (2) ) . 5.2.8 A N a ( a), A. y : y A, a (y ) , c(a, y ) Kh . , y .c(a, y ) m- A Kh . 5.4.25. B N m- ( m- m ), B A m B A N. 5.4.24 Kh m-. , m- , m- . 5.4.26. A m- , B N A m B , B m-. -

. A N. m- A A m A. m (. (a) 5.4.20) A m A A m B A m B . , m- m . m- : (c) 5.4.20 , . 5.4.26 m B : , ) B , ) m- m- B . , K m-. 5.4.27. K m-.


5.

223

. K 5.4.5. 5.4.24 Kh m-. , m- Kh K . l r (. 5.2.2) Kh : Kh = {x N | l
(x )

(r (x)) }.

x N : x Kh , l(x) (r (x)) . x N M (x) , y l(x) (r (x)) 0. x N : x Kh , M (x) y , , , M (x ) . s : N N, : x s M (x) . x N M (x) s(x) , M (x) s(x), s(x) (s(x)) . , x N : x Kh , s(x) (s(x)) , . . s(x) K . , s m- Kh K . , Kh m K , , Kh . g , x, y N g (x, y ) = 0, x Kh , , x Kh . /

g , Kh . 5.3.7 s : N N , x N y .g (x, y ) = s(x) . , x N : x Kh , g (x, s(x)) = s(x) (s(x)) , . . s(x) K . , s m- Kh K . 5.4.28. Kh . , Kh A N, , A m K . 5.4.29. 1. {x N | x C }, C , , m, m- K (. 5.4.19). 2. {x N | x } m-, . 3. {x N | x (x) } m-, 5.4.6 . 5.4.30. 1 5.4.29, m- .


224 . . 5.4.31. , m: 1) {x N | x }, 2) {x N | x }, 3) {x N | x = 0}, 4) {z N | xy (z = c(x, y ) x = y )}, 5) {x N | x (a) } a N.

5.4.5.
, , . , , , . 5.4.32 ( n = f (n) (. . n f (n) (b) n = y .g (n, y ). , ). (a) f : N N n N, ). p g : N2 N n N,

. (a) xy .f (x (x)) (y ). , x, y N: Mx (x); ( ) , f ; w Mw , Mw (y ) , , Mw (y ). 5.3.7 s : N N , x N y .f (x (x)) (y ) = s(x) . s m: s = m . x N f (x (x)) = m (x) . m x, f (m (m)) = m (m) , m (m) , s = m s . n = m (m), f (n) = n , . (b) 5.3.7 , s : N N , x N y .g (x, y ) = s(x) . (a) n N, n = s(n) . x = n n = y .g (n, y ). f , . n N, n = f (n) , f . ( f , x , x = f (x).)


5.

225

5.4.33. f : N N . , f . 5.4.34. , (k ) x m- f . . , , . 5.4.35. p N , p = p. . M , x M (x) , x. M f : N N , f (x) = x x N. p N, p = f (p) . x = p p = p. 5.4.36. - , . . , , . : , , : ' , , :' . (. 5.4.14) . 5.4.37 ( , -). C C (1) . C = C = C (1) , x C x N . . . A= . , , A {x N | x C }. C = (. . ) C = C (1) (. . A = N), a A b N \ A. f , x N f (x) = a, x A, / b, x A,
(n)

. n N, n = f n A, f (n) A.

. ()

f x N : x A, f (x) A. n x, : / n A, f (n) A, / () .


226 . .

5.5.
, , , . , , , , ; . , , .

5.5.1.
{a1 , . . . , am } Ai , Bi , i = 1, . . . , n. 2n : U Ai V , U Bi V U Bi V , U Ai V

U , V , i = 1, . . . , n. C . D E U DV , U EV U , V , D E , , ( ). , C Ai Bi , Bi Ai (i = 1, . . . , n).

, D E E D. X Y C , X C Y (. 1.2.2 ). ( ) C : X Y , C X Y . . i = 1, . . . , n Ai Bi Bi Ai , C : Ai Bi (i = 1, . . . , n). ()

, X Y , X C Y . X Y :


5.

227

Z1 , . . . , Zk (k 1), X = Z1 , Zk = Y l = 2, . . . , k Zl Ai Zl-1 Bi Bi Zl-1 Ai i = 1, . . . , n. , . S , Z [Z ]. S §, [U ] § [V ] = [U V ]. S § , a1 , . . . , am (). , C a1 , . . . , am (): X Y , [X ] = [Y ] . 5.5.1. , a1 , . . . , am ai aj aj ai ( i < j ). 5.5.2. , . 5.5.3. . . A B . ; , . . . C0 X Y ( C0 ), X C0 Y . , , . , , . M , , , S, q0 , F, P .

ZM M Z0 , , S , Z0 ZM ZM . , q2 S , a3 , a5 \ {_}, __a3 __q2 a5 _ a3 __q2 a5 , _a3 __q2 __ a3 __q2 _ , __q2 __ q2 _ . C S { , }. .


228 . . C , , Ai Bi , Z , ZM , , : ) Z , (. . Z Ai ), ) Z , ZM . ( M ) q a rb C q a rb. q a rbL C : 1) b = _, c cq a r cb q a r_b ; 2) b = _, c d cq a d r c_ d ; d q ad r _ _ d ; c cq a r c ; , , q a r_ . C q a rbR. X X _, X , X .8 , X , Y : M (X ) = Y q0 X
C

Y.

()

, M U q Y V , (q F ), Y Y V , . ( ) , C , , , Y , Y M .
8 (. 1 5.1.3 . 182), , ( ).


5. C 3 C : q a dd b a . q F , a , , d , b b ( \ ) { }, a , ,,

229

, , , , , . C ( ) . M , x N ( x) x (x) ( U (x, x)) 0 ( ). , x N : M (x) = 0 , x (x) . C , M , . ( ) x N : x (x) , q0 x C . C , . , , . C . C , C § § . , C , ( ): X , Y : M (X ) = Y q0 X
C

Y §.

C , C . C , C , . , C . : X , Y : q0 X
C

Y § q0 X

C

Y §.

(

)

, C C , , C , ( ). ( ) , q0 X C Y § C , .


230 . . ( ) Y § . Z1 , . . . , Zk . k = 1 q0 X C . k > 1. Zk-1 Zk , § , . , R1 , Zl-1 Zl l < k . Zl-1 Zl R1 . R2 , Zl Zl+1 . Zl+1 . , Zl : Zl-1 Zl , ( , , , C ). R1 R2 , Zl-1 Zl+1 . , Z1 , . . . , Zl-1 , Zl , Zl+1 , . . . Zk Zl , Zl+1 , R1 , C . 5.5.4. , , q a rbR . 5.5.3 , : X Y , X Y . . 5.5.5. , A B A, B . 5.5.3 ( ) . (, , ) . , . . 1947 . . . ( . ) , . . - (. [27, 29]). (. [30]). 5.5.6. 5.5.3, .
R1 R2


5.

231

5.5.7. , . . 5.5.3 , . . , 5.5.3, , , . , . (. [47, 48]), {a, b, c, d, e} : a c ca , ad da, b c cb , bd db,

e ca ce ,

edb de,

cca cca e .

5.5.2.
5.5.8. , . A , A . . , ( ) , , . S , S . ( . 3.2.4 . 115.) 5.5.9. .
S

. 5.5.5 C Ai Bi (i = 1, . . . , n), () i = 1, . . . , n Ai , Bi . { a 1 , . . . , am } C , x1 , . . . , xm . ai (i = 1, . . . , m) xi . A aj1 aj2 aj3 . . . ajk t S .
A

(. . . ((xj1 § xj2 ) § xj3 ) § . . . § xjk )


232 . . , A B : A B ( C ) ,
A, B

((t

A

1

=t

B1

... t

A

n

=t

Bn

) tA = tB )

S. A B . Z1 , . . . , Zk (k 1), A = Z1 , Zk = B l = 2, . . . , k Zl Ai Zl-1 Bi Bi Zl-1 Ai i = 1, . . . , n. M S , M , (tA1 = tB1 . . . tAn = tBn ). , Z1 , . . . , Zk , tA = tZ1 = tZ2 = . . . = tZk = tB , M . M , A,B . , A,B S ( ). , A,B S, A,B M , a1 , . . . , am (), , (xi ) = ai (i = 1, . . . , m). M , (tA1 = tB1 . . . tAn = tBn ) (). M , (tA = tB ), , A B . , , . A B A,B . S A, B ( A,B ). 2.4.3 A,B S, A,B . , A B , A,B . , S , C . 5.5.10. C . C , C . C , , . H() . 5.5.9 5.5.11. H(S ), .
S

-

5.5.12. 5.5.11 . , , 5.5.9, A,B


5.

233

A,B S. , , , . 5.5.13. , A B , A,B S (. 5.5.9). , B A A,B S. A , A , H() . , , , .

5.5.14. n , . , . . , , 2n . 5.5.15. T , , T , ; T . 5.5.16. , , , T , . 5.5.9 : . 5.5.17. .

5.5.3.
T , , . T . , H(). , T , . , () T . , . , , , ; . . . , ( ) , . , , H().


234 . . , . , ( 1) T ? , T . , , : . T , , , . , ; , {; }. , , M P Gen H() , , {; } , T . 5.5.18. . . 5.5.19. T , , , T , , T T , ( , ). 5.5.20. , -, , , . 5.5.21. T . T . . T , ; . P roof {; }, T . , P roof (, ) , T . , , , P roof . ( , . 5.2.21 . 206) P roof (, ) . , T . , T . 5.5.22. , , , . 5.5.23. , .

5.5.4.
M . M


5.

235

T , M . T T (. 3.1, , 3.1.6). T , , M T . 3.1.8 . 112 ,9 , T . P A , P A ; P A. , , . Wx dom(x ). 5.2.8 , W0 , W1 , . . . . 5.5.24. A N B N , f : N2 N , u, v N A Wu , B Wv Wu Wv = , f (u, v ) f (u, v ) Wu Wv . / 5.5.25. , . 5.5.26. K
0

{x N | x (x) = 0}



K

1

{x N | x (x) = 1}

. . , K0 K1 . . , K0 K1 . g , u, v , x N: Wu Wv ,10 Wu , x, 1, , Wv , x, 0. 5.3.7 f : N2 N , u, v N x.g (u, v , x) = f (u,v) . u v , K0 Wu , K1 Wv
. 2.6.32 . 94. 5.2.8.
10 9


236 . . Wu Wv = . , / f (u, v ) Wu Wv . u, v x x Wu , 1, 0, x Wv , g (u, v , x) = f (u,v) (x) = . f (u, v ) Wu , f (u,v) (f (u, v )) = 1, f (u, v ) K1 Wv , Wu Wv = . f (u, v ) Wv . f (u, v ) Wu Wv . /

m N m S S . . . S 0 Ar P A, S m . x1 , . . . , xn , A , t1 , . . . , tn . [A]x11,,......,,txn t n x1 , . . . , xn A t1 , . . . , tn .11 5.5.27. n- x1 , . . . ,xn Ar P A, . , A (x1 , . . . , xn ), m1 , . . . , mn N 1) (m1 , . . . , mn ) , P A 2) (m1 , . . . , mn ) , P A
x1 , [A]m1 , ì[A]x11 m

; ; A A P A , .

...,xn ,...,m

n

...,xn ,...,m

n

(x1 , . . . , xn ) P A, , P A (x1 , . . . , xn ). 5.5.28. , E q (x, y ) N, x y , P A x = y . ‡ 1) E q (m, n) , E 1 x(x = x) P A P A m = n. 2) n ( ): E q (m, n) P A m = n. . n 12 0. ( ) P 1 x(S x = 0) P A. . , ( ) n, k . ( ) n, k + 1. m, 0, ( )
11 , 2.3.1, 4.3.2, . 12 , =, = Ar .


5.

237

P 1. m j + 1 j . E q (m, k + 1) , E q (j, k ) , P A j = k. P 2 xy (S x = S y x = y ) P A S j = S k, . . P A m = k + 1. 5.5.29. , x y P A z (y = x + S z ). ‡ 5.5.30. ‡ P A. 5.5.30. , . 5.5.31. , P A , P A . K0 K1 , 5.5.26, , , 5.2.17 K0 K1 N2 . i = 0, 1 i , m N mK
i



n, i (m, n).

()

K0 K1 = , (0) m K0 n, 0 (m, n) l n 1 (m, l), (1) m K1 n, 1 (m, n) l n 0 (m, l). 5.5.30 i = 0, 1 i (x, y ) P A ‡ Ai . (, Ai x, y .) B0 B1 y (A0 w(w y (A1 w(w y ì[A1 ]y )), w y ì[A0 ]y )), w

w y z (y = w + z ). B0 B1 (0) (1) , , i = 0, 1, Ar : , Bi , (x) Ki . 5.5.32. m N (a) m K0 , P A (b) m K1 , P A (c) P A [B0 ]x ; m
x [B1 ]m ;

x [B1 ]m , P A

ì[B0 ]x . m

5.5.32. P A. 5.5.33. 5.5.32.


238 . . 5.5.34. () P A i (x, y ) Ai x, (i = 0, 1) , m Ki , n, P A [Ai ]myn . , x - P A y [Ai ]m . (a) 5.5.32 B0 y A0 ; (b). Bi (i = 0, 1) , (c) . 5.5.35 (() ( )). P A , P A . . Pr {m N | P A [B0 ]x }, m R ef {m N | P A ì[B0 ]x }. m

P r Ref = P A. 5.5.32 K0 P r K 1 R ef . 5.5.21 , P r Ref , u, v N, P r = Wu Ref = Wv . K0 K1 x f k = f (u, v ) Wu Wv , P A [B0 ]k / x P A ì[B0 ]k . , P A . 5.5.35 ì[B0 ]x , k P A ( P A ). x P A. , ì[B0 ]k , ) 5.5.35, k K0 , / ) , B0 , , (x) K0 .

5.5.36. P A , P A . . 5.5.35 P r Ref , K0 P r , K1 Ref ( P A) P r Ref = . , K1 Ref N \ P r . , P A . P r . , P r N \ P r , u, v N, P r = Wu N \ P r = Wv . K0 K1 f k = f (u, v ) Wu Wv = N. ( / k N) P A. /

P A P A. S Ar N -1 S; , 5.3.1. S S (S ) ( ) . m, (. .


5.

239

), m . , m, n N : (m, n) , m m , n [m ]x . , , , m 5.5.30 A, P A (x, y ). (, A x, y .) k ìy A. ìy [A]x , k [k ]x ( ) , k P A. 5.5.37. P A , P A .

. , P A . l . (x, y ) (k , l). A (x, y ), P A [A]x,y . - P A y [A]x , k k ,l P A P A. P A . , 5.5.37, P A , P A, , , P A. 3.1.6 P A P A Ar. P A S 0 = 0 (. 3.3.3 . 122), P A P A S 0 = 0. m S 0 = 0. P A C onsis
x ìy [A]m .

, P A . 5.5.37 , P A P A . P A, C onsis P A ( ). P A C onsis, P A C onsis P A , 5.5.37 , P A . , 5.5.38 ( ). P A , P A C onsis. , P A , P A , P A. P A , , Z F C , Z F C . ,


240 . . P A 2.6.20, . Z F C P A Z F C . Z F C (. 3.5.5). ( 3.5.5 P A Z F C .) 5.5.35, 5.5.36, 5.5.38 P A, T , P A. , T P A. , T , , , P A , . T Z F Z F C .


6.


, , .

6.1.
. , . . (). , . . . , 32- , . , : . , (232 )3 > 1028 . , , 1015 , 1013 , 3000 . , . , . , , , , , . ( , 241


242 . . .) , , , , . . . , . , , , (. 4.5.3). . , , .

6.2.
- () , . , , . , . ::= | | | | . ::= ':=' . ::= ';' . ::= 'if' 'then' 'fi'. ::= 'if' 'then' 'else' 'fi'. ::= 'while' 'do' 'od'. ::= . ::= , | . , . , , . , (. 2.2.2) ^. t1 ^t2 t1 t2 . , , , .


6.

243

, S while B do S od. , , , { }, . . S . M , N, , ^ , ( [7]) 00 = 1. , S , . , , , M , . . N. (x) x. ( , , , , .) , . , : . , . . S , S , ( S ), S (), . 1. x := t x |t| |t|M , t |t| (. 2.2.7 2.2.8 . 67). 2. S1 ; S2 . S1 . S1 , , S1 S1 (). S1 () S2 , S2 . ( 6.2 , S S , , S , S , S , S .) 3. if B then S fi |B | |B |M ,


244 . . B (. 2.2.9 . 67). , |B | , S , . 4. if B then S1 else S2 fi |B | |B |M , B . , |B | , S1 , S2 . 5. while B do S od |B | |B |M , B . , |B | , , S . S , , S S (). S () ( , S , B ). . , , . S 0, S S 0, S S S 0, . . . 1, 2, 3, . . . ( , ). , x := S 0 x := 1, . 6.2.1. E xp x, n, k , exp. ( ) . {1} k := 0; {2} exp := 1; {3} while k = n do {4} exp := exp § x; {5} k := k + 1 od x1 , . . . , xn , , (x1 ) = t1 , . . . , (xn ) = tn , {t1 /x1 , . . . , tn /xn }. ( , .) , , {3/x, 2/n, 594/k , 47/exp}. 1 {3/x, 2/n, 0/k , 47/exp}, 2 {3/x, 2/n, 0/k , 1/exp}. 3 4 {3/x, 2/n, 0/k , 3/exp}, 5 {3/x, 2/n, 1/k , 3/exp}. 3 : 4 {3/x, 2/n, 1/k , 9/exp}, 5 f {3/x, 2/n, 2/k , 9/exp}. ,


6.

245

k = n f , 3 , f . 6.2.2. {0/x, 3/n, 0/k , 0/exp} , ?

6.3.
, . S P rog . , , S P rog . S P re P ost, P rog S . ( ) , S , , P re, S ( ) P ost. ‡, . , ( ) . . , M 6.2. 6.3.1. {P re} S {P ost}, S , P re P ost , S . 6.3.2. P re P ost . , () S P re P ost, : M , P re S , M , P ost. , {P re} S {P ost} . 6.3.3. , . , while x = x do x := x od , ( ) . .


246 . . , M ( ), {[[A]]x } x := t {A}, t x , t , A , [[A]]x t t x A (. 2.3.15 . 74). . ; 6.3.7, . ( A, B , C , I ; B ; S , S1 , S2 ): A B ; {B } S {C } (S P RE ), {A} S {C } {A} S {B }; B C (W P OS T ), {A} S {C }

{A} S1 {B }; {B } S2 {C } (C OM P ), {A} S1 ; S2 {C } {A B } S {C }; A ìB C (I F ), {A} if B then S fi {C } {A B } S1 {C }; {A ìB } S2 {C } (I F E LS E ), {A} if B then S1 else S2 fi {C } {I B } S {I } (W H I LE ). {I } while B do S od {I ìB } , ; 6.3.7, M -. . S P RE W P OS T . W H I LE I ( , I , S while B do S od). 6.3.4. E xp 6.2.1 , {x = 0} E xp {exp = xn } . 1, 2, 3, 4 5 E xp S1 , S2 , S3 , S4 S5 . S1 ; S2 ; S3 E xp, S4 ; S5 S3 . ( ) , ( , ) , . , , .


6.

247

S3 E xp , exp = xn . W H I LE I . I exp = xk . {exp = xk k = n} S4 ; S5 {exp = xk }, ()

W H I LE {exp = xk } S3 {exp = xk ì(k = n)}. , M (exp = xk ì(k = n)) exp = xn , W P OS T {exp = xk } S3 {exp = xn }. (), . S5 exp = xk exp = xk+1 . , S4 exp = xk+1 exp § x = xk+1 . M (exp = xk k = n) exp § x = xk+1 , S P RE S4 exp = xk k = n. , (). , , {exp = xk } S3 {exp = xn }. S2 . S3 , . . exp = xk . S2 exp = xk 1 = xk . , S1 1 = xk 1 = x0 . M x = 0 1 = x0 , S P RE 1 = x0 , x = 0 S1 . , {x = 0} E xp {exp = xn } . , M T 1 = x0 , S1 S P RE T, {T} E xp {exp = xn }. ( T .) , C OM P : . : { { { { { { x = 0}{}{1 = x0 } 1} k := 0; {1 = xk } 2} exp := 1; {exp = xk } 3} while k = n do {exp = xk k = n}{}{exp § x = xk 4} exp := exp § x; {exp = xk+1 } 5} k := k + 1 {exp = xk } od {exp = xk ì(k = n)}{}{exp = xn }

+1

}

{x = 0} {T}, T exp = xn . {x = 0} E xp {exp = xn }: 1) {exp = xk
+1

} S5 {exp = xk }

;


248 . . 2) {exp § x = xk
+1

} S4 {exp = xk

+1

}
+1

; ( M -

3) (exp = xk k = n) exp § x = xk ); 4) {exp = xk k = n} S4 {exp = xk

+1

} 3, 2 S P RE ;

5) {exp = xk k = n} S4 ; S5 {exp = xk } 4, 1 C OM P ; 6) {exp = xk } S3 {exp = xk ì(k = n)} 5 W H I LE ; 7) (exp = xk ì(k = n)) exp = xn ( M );

8) {exp = xk } S3 {exp = xn } 6, 7 W P OS T ; 9) {1 = xk } S2 {exp = xk } ;

10) {1 = xk } S2 ; S3 {exp = xn } 9, 8 C OM P ; 11) {1 = x0 } S1 {1 = xk } 12) x = 0 1 = x0 ;

( M );

13) {x = 0} S1 {1 = xk } 12, 11 S P RE ; 14) {x = 0} S1 ; S2 ; S3 {exp = xn } 13, 10 C OM P . {T} E xp {exp = xn } , 12, 13 14 12 , 13 14 : 12 ) T 1 = x0 ( M );

13 ) {T} S1 {1 = xk } 12 , 11 S P RE ; 14 ) {T} S1 ; S2 ; S3 {exp = xn } 13 , 10 C OM P . 6.3.5. , , M , H(), ^: x(x0 = S 0), xy (xS y = xy § x). , , . 6.3.6. ? , , . 6.3.7 ( ). , , .


6.

249

. , {[[A]]x } S {A}, S t x := t. , , M , [[A]]x S t . , M , A. = |x| , |t| |t|M , . 2.4.17 M , [[A]]x M , |x| A. t t t , M , |x| A, , = |x| . t t , , M , . , , I F , . {A B } S {C } M A ìB C . , {A} if S {C }, if S if B then S fi. , M , A if S . , M , C . M , B , ( if S ) S . M , A, M , B {A B } S {C } M, C. M , B , if S , = . M , A, M , B M A ìB C M , C . 6.3.8. , . 6.3.9. , , , case, for, repeat until Pascal switch, for, do while C. , . , . 6.3.10. div 2 mod2. M , div 2 mod2 , , , () 2. ( x, n, p, q , exp) T exp = xn . exp := 1; p := x; q := n; while q = 0 do if mod2(q ) = 1 then exp := exp § p fi; p := p § p;


250 . . q := div 2(q ) od 6.3.11. , . . . . I. , , . T , , . . I I. , M , . , , . 6.3.12. , . ( , .) I I I. , , , , , . , , , 6.2. 6.3.13. P re P ost . () S ( ) P re P ost, , : M , P r e, S M , P ost. , {P re} S {P ost} ( ) . 6.3.14. , .


6.

251

, . , , , . F I N W H I LE :
n [I ]n+1 B ; {[I ]n+1 } S {I }; [I ]n ìB n 0 , {nI } while B do S od {[I ]n } 0

n , S . W H I LE F I N W H I LE , . 6.3.15. , , , . 6.3.16. ( , ) . .


.


, . , , . , .

.1.
. ( , ) . , , . , .1. 252


.

253

, G (), G , 1.4.4.

.1.1.
: , , , A , A , , A . .1.1. G (). . . ( .) . , , A . . . , A . . , 0 0 , , n, 0 , A0 0 . , n R. R ( ), , 1 , B C , R 1 , B , C . 1 , B , C, A , R , A . R ( ), , 1 , xB , R 1 , [B ]x , y () ()

y () x B . z , (), A. y z 1 , [B ]x z ( ). , A 1 , [B ]x , z R , A . , R, . .1.2. , . .1.3. .


254 . .

.1.2.
, n- S1 ; . . . ; Sn , S S , S1 ..., S . Sn

, (. . , , ). G () (, ), , , (, ). , : , ìA , , A , A B , , A, B , A B , A B , , , A , B , A B , A B , , , A , B , ìA , , A , A B , A B , , , A , B , A B , , A, B , A B , , A , B

, , A, B . . .1.4. G () . . . , , (), . , A B . , , A , B . . , A B . , A B , , A , B . 1 , A B . , A , B ( 1 , A B , A , B ) , () 1 , B , A , B 1 , A , B , A.


.

255

. , 0 0 , A0 B0 , , n, 0 , A0 0 , B0 . , A B , n R. , A B R, , A , B . R. , , R ( ), , A B , 1 , xC , A B , R 1 , [C ]x , A B . y 1 , [C ]x , A , B , R y , A , B . .1.5. . .1.6. , .

.1.3. ,
. . , . ( 1.3.3 2.6.2 .) , ( ) : ì - , A B , AB , A B ; , A ìB , ìA A; B , AB A , AB B , AB - A; AB , B

ììA , A AB , A AB , B

, A C ; , B C , , A B C

, , A, B , C . , , . .


256 . . . . - , G () (). -. () A () A B .

() () , A B . () , A B , , B . ì- , A B , A ìB () ( )AB ( ) A ìB .

- ( ) (A B ) ((A ìB ) ìA) ( ) (A ìB ) ìA. ( ) - ìA, . , ì- : ììA ììA A - A. - : A, B A (B (A B )), -, A B . , -, : A B (A B ) A - A; , A B (A B ) B B . , -, : A A A B - A B ; , B B A B - A B . , - , G () ( ). .1.7. , . (. 1.4.2), A1 , . . . , Am B A1 . . . Am B . , , .1.3, . , - , A B : , A, B . .


.

257

- : A , A B , B . - . ì- , ( , ): ìA, A , . . B B ìB . - : , A B C , , A C , B C . .1.8. , , -, : A B; , A C ; C , B C .

, G () , : [A]x y (-), xA [A]x t (-), xA xA (-), [A]x t , [A]x B y (-), , xA B

1) - - y ( ) x A , 2) - - t x A. , - : xA y , [A]x . - y ( C Choice ): , xA B , y x x, A xA, , [A]y B . x - : [A]y ( ) xA. - : xA xA [A]x - [A]x . t t .1.9. - -. .1.10. , , -, : xA; , [A]x B y , B y x A .


258 . .

.2.
, , , . 3, . , , 1.3 2.6 . 3. G (Ar) Ar , . , (. . Ar)? , S (0) + 0 = S (0) Ar , 1 0 1. G (Ar), . x(x + 0 = x), . x(x + 0 = x) S (0) + 0 = S (0) G (Ar) , , . , x(x + 0 = x), S (0) + 0 = S (0). , G (Ar) , S (0) + 0 = S (0) , . . . . . , , . A , , G () G1 . . . Gn A, G1 , . . . , Gn , .

.2.1.
. G () ( ()) S1 (), S2 S1 S
2

( -


.

259

. . 103). , S , S . , G () ( ), . .2 ( ) G () (). : . , , 2.7.10 , , S S0 , , 2.7.10, S0 () S . , (. 2.7.4). , (, ). 3.1.1 ( ) , 3, . .2.1. T , , A . A T ( T ), {G1 , . . . , Gn } , G () G1 . . . Gn A ( , T). , A T , T A. T A. G1 . . . Gn A, {G1 , . . . , Gn } T , , , A T . .2.2. , G1 . . . Gn A G1 , . . . , Gn A. .2.3. T , A , T A T ìA. T . .2.4. T , A T A T ìA. T .


260 . . .2.5. T . T . T , .

.2.2.
, . , .2.15 , , . .2.6 ( G () , G ()). T , , A . T A, A T . . .2.1, T A , {G1 , . . . , Gn } , G1 . . . Gn A. 2.7.7 G1 . . . Gn A. , {G1 , . . . , Gn } , ( ) : G1 , . . . , Gn , A . T G1 , . . . , Gn , T A . .2.7. , , . . T M . T , A T A T ìA. .2.6 M A M ìA, . .2.8. T . T , T . . , T , T . , , : T , T . T , . . A , T A T ìA. (. .2.1 .2.2) A A ìA ìA A ìA T . A ,
ìA

A



A ,

ìA

ìA.

B A ,
ìA

ìA (A B ).


.

261

- A , ìA B . , T B . , T . .2.9 ( ). . .2.9. 2.6.21 (. 2.6.28), . .2.10. .2.9. .2.11 ( -). - , . . .2.7 , , . .2.9 . .2.12 ( ( )). T , . , , , , T . . , T . .2.9 T , . . A , T A T ìA. (, ) 0 T0 , 0 , T0 A T0 ìA. , T0 . .2.7 T0 , . , T . , ( 2.6.32). .2.13. T , A . , ) A T , A T ; ) T A T A. .2.14 ( G () , G ()). T , , A . T A , T A. . A . T A . T , {ìA} . .2.9 T , . . B , T B


262 . . T ìB . c ì- ( , ) T ììA, ì- T A. .2.6 .2.14 3.1.5. .2.15. T , , A . T A, A T . , , 3, 3.1.6. .2.3 , .

.2.3.
I. , P A S S 0 + S 0 = S S S 0, 3.3.3. , S S 0 + S 0 = S S S 0 P A ( G (Ar)). , . P A, . G (Ar) , S S 0 + S 0 = S S S 0, ()

E 3, E 4, A1, A2 P A. , .2.2, E 3 E 4 A1 A2 S S 0 + S 0 = S S S 0 G (Ar), S S 0 + S 0 = S S S 0 P A. () 1í7. 1. G (Ar) A2, A2 P A xy (x + S y = S (x + y )), -, , S S 0 + S 0 = S (S S 0 + 0). (1)

2. A1, A1 x(x + 0 = x), - S S 0 + 0 = S S 0. (2)

3. E 4, E 4 xy (x = y S x = S y ), -, S S 0 + 0 = S S 0 S (S S 0 + 0) = S S S 0. (3)


. 4. (2) (3) - S (S S 0 + 0) = S S S 0. 5. (1) (4) - S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0.

263

(4)

(5)

6. E 3, E 3 xy z (x = y y = z x = z ), -, S S 0 + S 0 = S (S S 0 + 0) S (S S 0 + 0) = S S S 0 S S 0 + S 0 = S S S 0. (6) 7. (5) (6) - S S 0 + S 0 = S S S 0. , , , , . I I. . S 0 = 0 P A. P 1 S 0 = 0 G (Ar), P 1 x(S x = 0) P A: 1) x(S x = 0) S 0 = 0 2 (); 2) x(S x = 0) S 0 = 0 3 ( ); 3) x(S x = 0), S 0 = 0 S 0 = 0 G (Ar).

I I I. , 3.3.2 5.5.2í5.5.4 .



[1] . -. . .: , 1985. [2] . PROLOG. .: , 2004. [3] . ., . . 2. . .: , 2002. [4] . ., . . 3. . .: , 2002. [5] ., . . . .: , 1979. [6] ., . . . .: , 1982. [7] ., ., . . . .: , 1998. [8] ., . . .: , 1982. [9] . ., . . : . .: , 2004. [10] . . .: , 1973. [11] . . . .: , 1983. [12] ., . . . .: , 1977. [13] . . . .: , 1957. [14] . . . .: , 1973. [15] . . .: , 1990. [16] ., . . . // , , . 9. .: , 1972, . 66í83. 264




265

[17] . ., . . . .: , 2004. [18] . . : . . .: - . -, 1981. [19] . . -. .: , 1969. [20] . ., - . . . .: , 1988. [21] ., . . .: , 1970. [22] . ., . . , . .: , 2003. [23] . . . , , . .: -, 2001. [24] . . : . .: . . . , 2007. [25] . .: , 1988. [26] . . . .: , 1965. [27] . . . // , . 55, N 7, 1947, . 5 8 7 í 5 9 0 . [28] . . . . I. , , . .: - , 2002. [29] . . . . II. , , . .: - , 2003. [30] . ., . . . .: , 1996. [31] . . : . . .: .- , 2002. [32] . . . .: , 1 9 8 6 . [33] . . . , . . . .: , 1967. [34] . . .: , 1984. [35] . . . : - , 2000. [36] . . . .: , 1973.


266 . . [37] ., ., . - ; . .: . .: , 1967, . 113í144. [38] . . - , . // , , . 7. .: , 1970, . 194í218. [39] . . .: , 1972. [40] . . .: , 1981. [41] . . IíIV. .: , 1982, 1983. [42] . . .: , 1978. [43] . ., . ., . . . .: , 2004. [44] ., . . .: , 1993. [45] . . . . . I. .: , 1997. [46] ., - . . .: , 1966. [47] . . . // , . 107, N 3, 1956, . 370í371. [48] . . . // . . - . . . , . 52, 1958, . 172í189. [49] ., . . .: , 1983. [50] . . .: , 1960. [51] . . .: , 1975. [52] . . . .: , 1979. [53] Apt K. R. Ten Years of Hoare's Logic: A Survey Part I. // ACM Transactions on Programming Languages and Systems, Vol. 3, No. 4, October 1981, P. 431í483. [54] Barendregt H., Barendsen E. Introduction to Lambda Calculus. 1994. [55] Church A. An Unsolvable Problem of Elementary Number Theory. // American Journal of Mathematics, Vol. 58, No. 2, April 1936, Pp. 345í363.




267

[56] Deransart P., Ed-Dbali A., Cervoni L., Biro C., Scowen R. S. Prolog: The Standard: Reference Manual. Springer, 1996. [57] Fitting M. First-Order Logic and Automated Theorem Proving. Springer, 1996. [58] Gallier J. Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers, 1986. [59] Hoare C. A. R. An Axiomatic Basis for Computer Programming. // Communications of the ACM, Vol. 12, No. 10, October 1969, Pp. 576í580, 583. [60] Lassez J.-L., Maher M., Marriott K. Unification Revisited. // Lecture Notes in Computer Science, Vol. 306, 1988, Pp. 67í113. [61] Nilsson U., Maluszynski J. Logic, Programming and Prolog. John Wiley & Sons, 1995. [62] Sipser M. Introduction to the Theory of Computation, Second Edition. Course Technology, 2006. [63] Tro elstra A. S., Schwichtenberg H. Basic Proof Theory, Second Edition. Cambridge University Press, 2000.



9 9, 69, 124, 126 9, 126 / 9, 127 {x1 , . . . , xn } 9, 129 {x1 , . . . , xn , . . .} 9 {x X | (x)} 9, 130 9, 128 9, 130 \ 9, 130 9, 129 f : X Y 9, 133 dom(f ) 9, 133 rng (f ) 9, 133 X1 ½ . . . ½ Xn 9 , 1 3 2 x1 , . . . , xn 9, 127, 128 Xn 9 N 9, 134 N+ 9 9 9 = 12, 113, 236 1 2 V ar s 1 3 F 13 T 13 P L 13 ì 14 14 14 14 15, 75 16 1 ( ) 17 0 ( ) 17 B 17 Fì 17 F 17 F 17 F 17 |A|M 18, 68 |A| 18 M A 19, 68 M A 19, 68 A 19, 74 A 19, 75 A 22, 75 A 22, 75 G1 , . . . , Gn A 22, 75 G1 , . . . , Gn A 22, 75 A B 22, 75 | 28 28 C 32 C 32 32 32 C 35, 85 C 35, 85 35, 85 35, 85 , 3 5 1 , . . . , n 35 H 36 M P 36, 83 ì-, -, -, - 41, 255 G 49 (S ) 50 (ì ), ( ì), ( ), ( ) 50 ( ), ( ), (), () 50 57 60, 62 60, 62 F OL(P S, F S, #) 62 B V (A) 64 F V (A) 64 65 65 |t|M , 67 268


|t|M 67 x 67 |A|M , 67 M , A 68 M , A 68 Ar 68 68 [A]x 72 t A B 72 [[A]]x 74 t H() 83 Gen 83 -, - 87, 257 A B 95 G () 101, 259 ( ), ( ), ( ), ( ) 101 T A 111, 259 T A 111, 259 !xA 117 P A 118 m 119, 236 Z F 126 2x 129 I nd(x) 129 Rel(z ) 133 F nc(z ) 133 X Y 133 y = f (x) 133 f : x y 133 f (x) 134 f : x, y z 134 f (x, y ) 134 R 135 x y A 136 x y A 136 Z F C 136 Hi (S ) 145 H (S ) 145 H (S ) 145 I (N ) 149 Dom() 153 {t1 /x1 , . . . , tn /xn } 153 {} 153 E 153, 169 , 154 169 p f : X Y 181 _ 181 X Y 182 M () = 182 !M () 182 # 182 x 183, 192 M (x1 , . . . , xn ) = y 183 xy .f (x, y ) 188, 210 [M ]x 189 N o(x) 195 s(x) 195 n Im (x1 , . . . , xn ) 195 A 2 0 0 2 0 0 A c(x, y ) 203 l(z ) 203 r (z ) 203 c(n) (x1 , . . . , xn ) 204 (n) cm (z ) 204 Mx 208 (n) x 208 x 208 (n) U 210 U 210 K 214 A m B 220 K (2) 220 Kh 220 X 228 Wx 235 K0 , K1 235 x [A]t11,,......,,txn 236 n - 189 Ar 68 - 189 C+ + 1 6 7 C# 1 6 7 Datalog 167 G 49 G () 101, 259 Gen 83 H 36 H() 83 Haskell 167 Java 167

269


270 . . 114 131 124, 126 m- 222 245 m- 222 m- 220 G 51 Mo dus ponens . G () 101 M P 36, 83 H 36 H() 83 P A 118 246 Pascal 167 - 189 P L 13 124 Prolog 167, 168, 175, 177 118 114 s-m-n- 211 114 SLD- 174 P A 118 SLD- 170 Z F 126, 132 SLD- 170 Z F C 136 SLD- 167, 170 115 Z F 126 115 Z F C 136 66 179, 198, 199 47, 97, 166 - 188 166 180 154 129 . 136 130 47 131 SLD- 118 175 31 G 55 G () 106 129 H 47 111 H() 97 128 124, 126 166 127 47 131 H 47 246 127, 132 , 131 114 151 124 212 114 157 111 180, . 129 12 128 - . - Lisp 167


31 181 181 181 181 181 181 181 32 () 49 187, 188 118 110, 118, 234 226 62 145 177 65 . - 12 26

271 95 35 32 149 19, 75 153 155 155 11 180, 199 186 183, 199 . 180 35 199 62 101 168 115 31 9 9, 132 169 167 SLD- 174 52, 53 52, 53 162 147 149 148 24 245 208, 209 27, 140 57, 160

241 242 105 175, 242, 243 183 167 12 64, 101, 188 64, 65, 101, 188 32 SLD- 170 111, 121, 234, 259, 263 35 H() 85 58, 162 34, . 51 . 51 111, 113, 259 H() 85


272 . . 168 27 14 27 32, 35 12 . 32 137 199 82, 90, 199, 200 . 34, 120, 122, 138, 262 34, . 95 G 56 G () 107, 253í 255, 257 H 41 H() 86í88 212 14 168 () 32 21 76 21 21, 90, 199 21 . 77 21 149 65 65 65 65 65 65 65 167, 169 169 . ( ) 243 67 . 134 119 167, 242 14 246, 250 208 208 61 129 33 33, 123 28, 118 63 15, 63 15 () 242 242, 244 250 242, 243 242, 243 242, 243 250 242, . 245 175, 207, 209 119 119 17, 66, 111, 260 66


114 17 Ar 68, 118 66 111, 260 . 66 13, 17 17 18 67 31 G 49 G () 101, 259 H 36 H() 83 226 49 36 49 - . 232 101, 259 83 1 1 7 101, 259 232 58, 162 245, 248

273



168 168 168 . 71 181 182 188 193 154 103 72, 97 66 66 12 61 13 61 138 82, 90, 199, 200 57, 151 52 50, 101 48, 97 ( ) 181 181 181 182 125 27 203 203 27, 140 60, 62 14 62 27 62 64 175 G 53 195 110, 123, G () 103 H 38 137, 138 H() 86 . 37


274 . . 248 58, 162 176 241 250 250 245 - . - 72 44, 91 73 163 27, 140 57, 151 160 59 11, 59 7 60 60 60 11 167, 168 14, 15, 28 14, 15, 28 14 22, 75 19, 20, 60, 74, . 62 62 167 13, 17 - 188 - 180, 187í189, 230 - 209 - 180, 194 - 188 191 188 - 189 189 212 212 212 7 81 175, 242, 243 180, 181, 198, 207, 227, 230 182, 183 183 182 225 209 183 138 108 34 33, 123 208, 209 63 15, 63 15 28, 118 140, 144, 160, 166 166 140, 144 140, 144 56 216, 219 120, 137 120, 138 197 235 9, 124, 126 m- 222 m- 220


() 135 () 17 9, 134 129 135 135 153 155 155 . 57, 144 57, 144 129 57, 144 - 2 2 0 220 215 214 220 127 201, 202, 204, 206 . . 9, 127 125 200, 204, 206 156 . . 43, 90 43, 90 43, 89 43, 90 43, 89 43, 90 91 43, 90, 111, 260 66 43, 90 P A 120 114 17 66 111, 260 66 36, 83, 257

275



155 124, 125 12 35 32 19, 75 57, 144 208, 209 111 19, 75 215 224 - 193 111, 259 43, 90 111, 112, 235, 259, 260 19, 75 43, 89 G 54 G () 103 H 38 H() 86 - 190 233 232 214 P A 120 155 155 127 . , 181 .


276 . . 207 n- 204 204 G () 101 208 220 208 127 203 175 203 175, 242, 243 238 238 149 208 208 145 114 65 114 169 - 177 66, 133 191 204, 206 180, 185, 230 204, 206 185 185 206 185 203 9, 133 66 160 153 14 - 195 67 183, 192 32 207 127 127 133 125 9, 133 125 135 64 133 9, 133 101 64 64 160 160 71, 73, 97 226 13, 63 - 188 G () 254 61 179 64 . c 50, 101 19, 74 13, 61 197 64 64 101 9, 129 128


9, 130 130 201, 202, 204, 206 201, 202 206 206 204 206 204 2 0 6 . 9, 129 12 12, 72, 153 170 170 159 74 72, 189 153 63 - 189 16, 64 169 46, 47 SLD- 175 G 52, 55 G () 106, 108 H 47 H() 97 166 47, 52, 55, 108 29 111, 112, 235, 259 112 43, 90 148 G 54 G () 103, 259 H 43, 46 H() 89, 94 116 164

277 . 115 227 . 135 136 ( ) 245 14 168 52 () 32 31 G 50 G () 101 101 101 H 36 H() 83 246 - 189 C 87, 257 84 G 56 G () 253 168 31 Gen 83 M P 36, 83 n- 32 254 253 253 . 87, 257 88 36, 83, 257 83














278 . . 226 G () 254 246 36, 257 58 42, 107 246 74 81 136 66 P A 236 70 P A 236 204, 206 68, 69, 113 204, 206 206 204 62 61 113 65 61 64 64 64 101 34 50, 101 ( ) 245 81 133 42, 257 42, 257 42, 257 153 145 195 196 181 212 215 232 212 212 212 231 213í215, 220 213 227 213í216, 218, 220, 227, 229 216, 219 2 2 6 226, 227, 231 230, 231 167, 168 181 242 138 210 ( ) 185 185 185 205 9, 132 . 11 13, 61 13 61 1 3 195 111, 112, 259 19, 75 43, 89 42, 125, 257 175
























. , 9, 127 12 57, 160 169 69, 113 12 22, 75 42, 257 9, 130 233 232 200, 204, 206 200 206 206 204 206 204 2 0 6 191 57, 152, 153, 161, 166 SLD- 170 160 58, 162 59 58, 162 SLD- 167, 170 167 12 - 189 12 72 74 153, 169 182

279 185 197, 202 ( ) 193 234 . . 180 216, 219 124 () 64 72, 189 64, 101, 188 () 64 64, 65, 101, 188 . 49 49 101, 259 101, 259 103 49, 101 50, 101 103 245 169 245 175 175, 242, 243 175 17, 37 65


280 . . 22, 75 147 149 148 126 61 12 62 62 181 61, 62 113 61 181 61, 62 141 95 24 66 31 160 141, 143 141 22, 75 22, 75 12 12 12 12 226 182 183 186 206 206 206 206 206 206 12 144 12 32 35 181 12 32 35 12 111 () 101 120, 137 . , 181 181 181 243 241, 242, 245 . Ar 68, 118 129 9 167 SLD- 167, 170 167 28 () 49 195 ( ) 185 66 66





18, 20 19, 74 198 168 243 s-m-n- 211




281

() 238 138, 239 90, 94, 111, 261 115 H() 94 32 G () 260 - 94, 261 H 37 38, 86, 256 H() 85, 111 45 G () 261 94, 261 H 45 116 H() 94, 111 201, 204 175 217, 219, 225 G 53 111, 259 G () 103 - 217, 225 G () 150, 151 260 110, 111, 258 H 38 P A 118 H() 86 Z F 126 Z F C 136 248 - 110, 126, 58, 162 234 22, 75 - 224 136, 137 ( 111, 259 ) 193 111, 112, 235, 211 259, 260 233 111, 112, 235, 259 77 112 111, 112, 259 233 24 234 G 54 113 G () 103, 259 G () 110, 111, 261 258 H 46 H() 94 110, 118, 234 H() 115 116 115, 231, 233, 234 164 205, 206 179 224 179 138, 252 25, 78 125 95 124, 125


282 . . 62 65 - . - 65 72 62 241 39, 86 153 19, 74 19, 75 245 250 250 245 149 149 149 209 210 65 145 155 155 155 155 n- 9, 128 127 168 - 242 110, 111, 258 242 120, 138 34, . 34, . 1 3 13, 62 62 65 . 19, 75 26 70 P A 236 65 19, 68 13 19, 68 - 189 19, 75 19, 75 19, 75 73 19, 74 62 ( ) 185 62 13 19, 75 19, 74 19, 75 103 62 95 95 72, 97 22, 75 22, 75 22, 75 95 50 61 141 167, 187, 191 9, 133, 134, 187, 207 m- 220 26


183 136 180, 199 186 183, 199 183 17 203 203 - 209 - 180, 194 208, 209 181 - 195 197 196 195 195 197, 202 ( ) 193 212 182 210 . 181 . 180, 197 183

283 181 2 0 0 206 206 204 204 149 149 180, 197 77 183 183 183 - 194 186 197 203 204 204 204 204 204 103 103 50 27 27 135 50 101 101 50 127







200 206 206 . - ( ) 182 28 204 204 15, 75 . 95 243, 244, 251 95 22, 75


284 . . 22, 75 95 65 9, 124 110, 118, 234 115 115, 231, 233, 234 145 146 149 149 145 145 2 3 5







1 3 31 13 167 124 62 206 167, 180 167 167, 242 167 167, 187, 191 13 206 69, 126 13 68 69 69, 231, 232 34 34 - 34