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

lilianjie

哪位能给理解下：

Formal Sets
' v' m5 g/ d- i  `& h$ hA formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.

% [: e* [2 _1 C7 {4 M+ a/ W  m) d2 RThe only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
9 p! B: I8 H: ^. O- B3 \
( m; Y( V4 e2 Z( F" [# F3 ~9 T: E1 E+ {
* T! u, m8 T( ]% I, E8 j* H% k8 c3 P
S := { 1 .. 5};
> P := PowerSet(S);
7 J# I0 r( S# Z9 _2 uP;
6 z5 |0 K! @2 A1 V2 R! QPFS:=PowerFormalSet(S);
# z( u8 Z; |/ ?. K- s9 }, Q' Q0 aPFS;
F := { 2, 4 };
FF := { 2/3, 4 };
; W, B$ i% I5 P* v, z
5 p/ e: q! R" a! W F in P;
  Z$ g: u8 y8 q6 TFF in P;
2 ^. W: A* f$ U: i$ `3 r. T F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
6 ]( a% S9 ~; o, N7 o0 |, n9 {. D2 OSet of formal subsets of { 1 .. 5 }
' K& L* C9 e( S3 N: ztrue
' u9 |7 u! `( o3 m7 K" Efalse
1 D$ N" a8 l7 E! c& c* i1 W( a4 V& }' F
2 x: n5 \  k! t9 W# _! H- ~/ c3 J>>  F in PFS;
- z: [* I. Z/ m: s' r      ^
" \! B( i) W' B1 h- j0 dRuntime error in 'in': Bad argument types

+ |2 h7 n, f+ i! P1 Y7 O0 r
>> FF in PFS;
      ^
8 H3 ~' q0 g+ }) i2 f) W8 N- DRuntime error in 'in': Bad argument types