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

lilianjie

哪位能给理解下：

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'.
# c1 ^8 A  q: w) J
The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.

0 R# {" `* w! {

S := { 1 .. 5};
; \2 }7 Q$ N2 ~4 W/ ]> P := PowerSet(S);
9 E" ^- [- B6 H0 C/ KP;
+ {6 R8 Q5 j$ l, i4 F- |PFS:=PowerFormalSet(S);
, R( u% \2 d2 [- {4 n- h. fPFS;
F := { 2, 4 };
FF := { 2/3, 4 };

6 n) L/ ^1 S' Y( L9 G& D F in P;
FF in P;
# Z, }3 X; ?8 b  v- e F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
Set of formal subsets of { 1 .. 5 }
true
. J, D2 @  Z, ]. }3 ^false
; v5 a% J( r& w. e; a
>>  F in PFS;
      ^
Runtime error in 'in': Bad argument types


6 h2 f8 K! y4 x8 a$ W>> FF in PFS;
; ~. |' F) ]# c9 g0 L6 n      ^
7 h- h2 P8 w, Z% n. sRuntime error in 'in': Bad argument types