: . , .
4.2.1. () , () () (), () ( ), ( ) = 1, , , , . () , . , (), , .
4.2.1. - F, G, H :
) F(x) ( F (x));
) F(x) ( F(x));
) F(x) G (F(x) G);
F(x) G (F(x) G);
) F(x) G (F(x) G);
F(x) G (F(x) G);
) F(x) () (F(x) ());
) F(x) () (F(x) ());
) F(x) () (F(x) ());
) F(x) () (F(x) ()).
. .
) F(x) ( F(x)). r - R. ( F(x)) r, F(x) r. , k(x) R, F (k (x)) , , F (k (x)) r. , ( F(x)) r.
( F(x)) r, F(x) r. , F(x) R F(x) R. , ( F(x)) r. ,
( F(x)) ( F(x)).
) ).
) F(x) G
Û (F(x) G). F(x) G ( F(x))→ →G ( F(x)) → G.
,
1) ( F(x)) → G ;
2) F(x) → ( F(x)) 7;
3) F(x) → G 1) 2);
4) x ( F(x) → G) x (F(x) G) 3).
:
1) x (F(x) G) x ( F(x) → G) ;
2) F(x) → G 6 1;
3) ( F(x) → G) → ( G → F(x)) ‒ ;
4) G → F(x) 2) 3);
5) x ( G → F(x)) 4;
6) ( G → F(x)) → ( G → F(x)) 5;
7) G → x F(x) 5 6;
8) ( G → xF(x)) → ( x F(x) → G) ;
9) x F(x) → G x F(x) G 7) 8).
).
1) F(x) G ( F(x)) → G ;
2) ( F(x)) → G 6;
3) ( F(x)) → G) → ( F(x) → G) 7;
4) ( F(x) G) (F(x) G) 2) 3).
:
1) ( F(x) → G) ;
2) ( F(x) → G) → ( F(x) → G) 7;
3) F(x) → G 1) 2);
4) x ( F(x)) → F(x) 6;
|
|
5) x ( F(x)) → G x ( F(x)) G (F(x)) G 3) 4).
) ) .
x F(x) G ( x F(x) G)
Û (( F(x)) G ( ( F(x) G)
Û ( (F(x) G) x (F(x)) G).
x F(x) G ( x F(x) G)
Û( ( F(x)) G) ( ( F(x) G) Û ( (F(x) G) x (F(x) G).
).
.
.
4.2.1 . 䳿:
) → :
= ( → ) ( → ); → = ;
) :
( x F(x)) = ( F(x)); ( F(x)) =
= x ( F(x)); F = F;
) :
Q x () G = Q x (F(x) G);
Q x () G = Q x (F(x) G);
F(x) () = (F(x) ());
F(x) () = (F(x) ());
Q1 F(x) () = (F(x) ());
Q1 F(x) () = (F(x) ()).
, .
1. → ).
2. , : (F G) =
F G; (F G) = F G, ).
3. , .
4. , ).
, 4.2.1.
4.2.2. - , , ├ L.
4.2.1. F(x) → () .
. 1, 2, 4 ,
F(x) → () = ( F(x)) () =
= ( F(x)) () = ( F(x) ()).
4.2.2.
z ( (, ) (, z)) → z R(x, y, z).
. 1, 2, 3, 4 ,
z ( (, ) (, z)) → z R(x, y, z) =
=( z y ( z ((, ) (, z)) z R(, , z) =
= x y z ( (, ) (, z)) u R(, , ) =
= x y z u ( (, ) (, z) R(, , )).
, (). , = ,
= , ‒ .