什麽是形式集合Formal Sets/PowerFormalSet？

lilianjie

哪位能给理解下：
& A8 O' n# J0 U' F  ~  B* I' n
Formal Sets
; r5 L' R, ^5 z8 t; C+ l9 O( dA formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.

; r& T, m" h" }, j) i) [The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.

) k4 U6 @, O" b% o8 |1 W1 N
' G1 B& `- i8 W1 A
5 E) S7 K! P* y$ a4 CS := { 1 .. 5};
* E: O, ^, Z1 ?7 ]# H6 X, R7 }> P := PowerSet(S);
P;
- J1 D: m; r# e3 G* SPFS:=PowerFormalSet(S);
& s5 Q+ }. ?! ~- e2 _, O& D/ yPFS;
5 g0 p: s3 }6 Y8 a$ d/ Z/ xF := { 2, 4 };
FF := { 2/3, 4 };
% l4 E9 u) D! r7 Z$ m9 }+ }
F in P;
0 g+ d6 e7 j5 I9 T  ?2 o% UFF in P;
F in PFS;
& g# F7 h/ a- oFF in PFS;
+ }  Y1 p" e) B, xSet of subsets of { 1 .. 5 }
Set of formal subsets of { 1 .. 5 }
+ d7 z  r7 R0 H6 V1 T5 v- {- n$ S& `8 xtrue
false
" Q$ n  f* p$ R" x9 p
>>  F in PFS;
      ^
' L- q9 q4 T" _: B: o& DRuntime error in 'in': Bad argument types


>> FF in PFS;
      ^
Runtime error in 'in': Bad argument types