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

lilianjie

哪位能给理解下：

* X" D; ~5 U3 Z- _3 M1 D- ^Formal Sets
A formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.
) O1 C' c+ i4 N/ h) G
" e! e0 j% l+ h6 y$ T' G8 fThe only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
8 b+ B* z& P$ }% I

% L- H3 [: U; P0 v8 s! C" [; v
8 a: c9 Y" p* Z/ cS := { 1 .. 5};
- s1 G9 K7 k3 r  T6 L> P := PowerSet(S);
- k2 r5 E$ W4 h8 U: Z; Q  k" O5 CP;
' s8 I: J+ H( K7 Q: z7 [PFS:=PowerFormalSet(S);
PFS;
1 }3 p" [, ?* k; w0 W5 lF := { 2, 4 };
FF := { 2/3, 4 };

: {7 q! ^, O) g" K6 W F in P;
FF in P;
# G+ U# U! o' G4 Y7 c7 f, \) w F in PFS;
9 g# i& B' \" C9 b3 y, z7 u6 {FF in PFS;
# T9 x& L6 R2 B8 [3 z) @* j  X* T- i0 u" A% uSet of subsets of { 1 .. 5 }
Set of formal subsets of { 1 .. 5 }
$ w) J7 V1 v2 C# d6 P1 qtrue
false

>>  F in PFS;
5 N" s+ b6 J: C) F9 d* [& O; z1 c      ^
/ P! q1 f6 c% d" D: ARuntime error in 'in': Bad argument types
+ ]* Y) E3 T5 X3 T9 t3 G! \: T

>> FF in PFS;
( D! b& d- v* \      ^
Runtime error in 'in': Bad argument types