i. i
i, i i () i.
1. i i, i i (ii) i x1,x2,..., (ii) a1,a2,..., P11, P21,...,Pkj,... i i f11,f21,...,fkj,..., i i i (, (, (, (, i (, (i i i (,),, ().
i i i i i (i), i i .
2. .
.
). i ii i i .
). f n - i , t1,t2,...,tn - , f n(t1,t2,...,tn) - .
). I i, i ) i ), .
i, .
). Pn , t1,t2,...,tn - , Pn(t1,t2,...,tn) - , . i i Pn(t1,t2,...,tn) i.
). F1, F2 - , ((F1), (F1(F2), (F1(F2), (F1(F2) . i i, ii F1 i F2, i i .
). F(x) - , i ii i x, (xF(x) i (xF(x) - .
i i x . i F i.
). I , i ), ) i ), .
. ii i i ii i. M , , i , i i i i i, M. i i i; i i i (i) i , ii i .
3. i i i i.
). i i (, - A1-A10 S1-S3). , i i i.
). i i i:
P1. (xF(x)(F(y),
P2. F(y)((xF(x).
i F(x) - - , i ii x, i i y. F(y) F(x) i i i i x y.
, F(x) , , (yA(x,y) (y(A(x)(B(y)) .
4. i i i .
). (modus ponens) - , i .
). ( (): A(B(x) A((xB(x).
|
|
|
). (: B(x)(A (xB(x)(A.
i B(x) i ii x, A i.
i i i. , i i i. i i , i i ii i i ii i i i. i ii ii i i.
() , , , . , 5.5 5.6 .
5.7. - () ( ) .
5.5. , . ³, , .
5.8. - () .
.
, 5.1.
5.9. A B , ((AB) Ù (BA)) , .
, ((AB) Ù (BA)) ~ (A~B). , : A B (A = B) , (A~B) .
, , , , , .
, . , , , .
, , , , "P (P (x)). , .
:
.
T,
A^2(t,s), t=s, A^2(t,s)
t≠s.
17.3. T ,
T:
6. ∀x (x=x) ;
7.(x=y) → (A(x) → A(x){y/x}) ,
x y , A(x) , A(x){y/x} -
|
|
|
( ) x y, y x, .
T.
17.6. ├ t=t t.
. A6: ├∀x (x=x) A4: ├∀x (x=x) → (t=t) t=t. ►
17.7. ├ x=y → y=x.
. A(x) x=x, A(x){y/x} y=x. :
1) ├ (x=y) → ((x=x) → (y=x)) 7;
2) ├ x=x 17.6;
3) ├ (x=y) → (y=x) 2 L. ►
17.8. ├ x=y → (y=z → x=z).
. A(y) y=z, A(y){x/y} x=z. :
1) ├ (y=x) → ((y=z) → (x=z)) 7;
2) ├ (x=y) → (y=x) 17.7;
3) ├ x=y → (y=z → x=z) 1 L. ►
A, .
17.4. A , :
1. 0.
2. + ×, ´. :: 107
3. = (= ≠).
4. :
1. (P(0) ∧ ∀x(P(x) → P(x´))) → ∀xP(x)
2. t1´ = t2´ → t1 = t2
3. t´ ≠ 0
4. t1 = t2 → (t1 = t3 → t2 = t3)
5. t1 = t2 → t1´ = t2´
6. t + 0 = t
7. t1 + t2´ = (t1 + t2) ´
8. t×0 = 0
9. t1×t2´ = t1×t2 + t1
P , t, t1, t2 A. 1
.
27. . Ҳ. .
(㳺).
. ( ).
³, , .
A (p1, p2,..., pn) - , a1, a2,..., an A (a1, a2,..., an) . , - A, A p1, p2,..., pn B1, B2,....., Bn, 0 1.
, A AB , B, , . : B , , 0. AB, A 㳺, 10, 0. AB.
, , , ( ) . , () .
, .
. - . , ├F ( F ), Gen , ├ →F.
. F.
U1, U2,..., US 
F- F ,A.
: s = 1. U1 F :
|
|
|
) F 
;
) F- ;
) F .
) : 1)F();2)F->(A->F)(A1, A=G);3)A->F(MP 1,2).
) , ) F->F. .
, F, , s.
, , : 1 < < s, : ->Uk, US :
) F
)F-
)F =
) i,j: 1 < i,j < s , Uj= Ui ->Us, Us modus ponens;
)F= 
Gen.
, , . ), , ->Ui, ->(Ui->US). 2, (A->(Ui->US))->((A->Ui)->(A->US)
modus ponens -> US, US=F.
) ->Ui.
. 5 
.
A-> Ui, Gen: 
x (A-> Ui) .. .
