Kt .
1) D(B1, Bn), D(p1, , pn) .
2) [F](A B) ([F]A [F]B); [P](A B) ([P]A [P]B) ().
3) [F]A [F][F]A ().
4) A [F]<P>A; A [P]<F>A ().
; .
, , 1, , n , , [F] [P].
, A [F]<P>A A [P]<F>A , :
1. Kt A , (W, R), R. Kt ,, Kt.
.
(W, <) ,
1) "x Î W (Ø(x < x)),
2) "x, y, z Î W (x < y & y < z x < z).
t < v, v t, t v.
2. Kt A , .
, Kt . <F>1 <P>1 t Î W.
[F][F]A [F]A :
"t"u (t < u $v(t < v <u)).
, Q R , Z .
, .. :
"t"u (t < u Ú t = u Ú u < t),
<F>A&<F>B <F>(A&B)Ú<F>(A&<F>B)Ú(B&<F>A)
( ).
(Z, <) :
[F]([F]A A) (<F>[F]A [F]A),
[P]([P]A A) (<P>[P]A [P]A).
(N, <) :
[F]([F]A A) (<F>[F]A [F]A),
[P]([P]A A) [P]A.
(R, <) , . :
<F>[F] <F>ØA <F>)[F]A& Ø<P>[F]A).
:
1) *();
2) 1* = 1, 0* = 0;
3) (Ø)* = Ø(*);
4) ( & )* = * & *, ( Ú )* = * Ú *;
5) ([F]A)* = "y(x < y A*(y)), y ;
6) ([P]A)* = "y(x < y A*(y)), y ;
7) (<F>A)* = $y(x < y & A*(y));
|
|
8) (<P>A)* = $y(y < x & A*(y)).
, .
T() Y(), :
, TA YA . M = (Z, <, h):
M, t |= TA, M, t+1 |= A;
M, t |= YA, M, t-1 |= A.
TA Next A, 0A, XA.
Since, Until
ASB AUB. M = (W, <, h):
M, t |= AUB, u > t M, u |= B v, t < v < u, M, v |= A ( , , );
M, t |= ASB, u > t M, u |= B, v, u < v < t, M, v |= A ( , , ).
, . &, Ø 1 .
FT , 1 &, Ø, <F> . [F], [F] = Ø<F>Ø.
FPTY , 1 &, Ø, <F>, <P>, T Y.
US , 1 &, Ø, U, S.
<F> <P> T Y. , T Y . US FPTY:
<F>A = 1UA, <P>A = 1SA, TA = 0UA, YA = 0SA.
US :
(B U A)*(x) = $y(y > x & A*(y)) & "z(x < z < y B*(x)).
S .
. (, FP US) , q(, 1, , n) (1, , n) , *(, 1*, , n*) q(, 1*, , n*) . , :
M |= "x (A*(x) q(x)).
3 (). US .
(T, <) , X,YÍT, ,
1) X È Y = T;
2) x < y x Î X y Î Y;
3) X , Y .