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

lilianjie

哪位能给理解下：
. D3 V, e7 H/ G" J
2 ~& @! H6 ~3 v3 C& ^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'.

The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
# d' ^$ Z+ \# A/ C2 o

; q( d* f8 t5 G$ d
' X2 y" d) o' V2 _$ E4 vS := { 1 .. 5};
4 {6 g1 Y# ]1 t3 I: B$ A> P := PowerSet(S);
P;
7 Y  J$ k( d+ yPFS:=PowerFormalSet(S);
PFS;
) \% e5 e' w: u% eF := { 2, 4 };
6 R1 A& K8 k0 W4 B* X- o; yFF := { 2/3, 4 };
0 G. |& O) r& y$ \- O) H% w; t
F in P;
FF in P;
1 d: E# \% y. o% g2 }: V- c F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
  C) _' D$ H& u* U+ d& z# Y) E, JSet of formal subsets of { 1 .. 5 }
! e0 P3 u9 B2 U( C% z- r7 Ctrue
false
7 ], S' v& j" v: j) h
>>  F in PFS;
9 c$ u. R; }4 g* Z/ p" d      ^
. S7 p; b) ^- ARuntime error in 'in': Bad argument types
% g7 g  W8 L! \4 E
% `8 F5 H( {  ~- G# z. k
>> FF in PFS;
      ^
( k1 w) W8 d, v' ]# M9 jRuntime error in 'in': Bad argument types