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

lilianjie

哪位能给理解下：
- o+ j/ `: M. x. ~$ P
Formal Sets
! B- z: x; f) d, Y& vA formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.
/ T5 V& C8 j, d! d/ o* p6 z
The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.

* I7 p3 m7 @2 u, ]% V- A6 u
' h) J" z. @( f- I- }
S := { 1 .. 5};
> P := PowerSet(S);
P;
PFS:=PowerFormalSet(S);
PFS;
& o7 G3 Z6 ]' Q+ O9 L# vF := { 2, 4 };
1 O& w4 k  j6 G; o: x* QFF := { 2/3, 4 };
. n, x8 F! m8 R* V4 k' B* i; O
: ]8 H  j# S* V! j$ H" z F in P;
$ }0 f( b8 t& t: o3 w  ~7 w9 N) d  BFF in P;
: G6 h& Y8 N) W' y: J+ t. Z# {( f1 a F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
, e4 J7 q- \3 D- E" L: nSet of formal subsets of { 1 .. 5 }
3 j4 `$ E- \7 M  Y3 b$ Utrue
7 f; N7 H) L, v4 H- C% O2 X# Kfalse

: I/ u6 {5 m& g, y3 }% Z>>  F in PFS;
      ^
3 O# M3 B: y9 D! h* kRuntime error in 'in': Bad argument types

( ?0 i' Q% V0 m3 }( D3 g8 M9 X
>> FF in PFS;
* d' _) O) n/ }- F) q2 J, S      ^
Runtime error in 'in': Bad argument types