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

lilianjie

哪位能给理解下：
8 A$ e. o4 L+ c$ `2 e
6 \, \7 p+ ?+ dFormal Sets
A formal set consists of the subset of elements of some carrier set (structure) on which a certain predicate assumes the value `true'.
: k3 d0 \7 b# f4 c5 g. ^/ L% j! i
6 O8 x! [1 o6 PThe only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
' ^0 P: a) k- Z# G! m" F


S := { 1 .. 5};
' i+ m! `' g( i" m# o  {> P := PowerSet(S);
8 e4 [& x2 m7 n( MP;
PFS:=PowerFormalSet(S);
PFS;
2 ?" O( q( J$ ~( B1 g" I- Q* R8 e5 wF := { 2, 4 };
9 s# J( l& K) d% Z- X  x# u. M( `FF := { 2/3, 4 };

5 m! p7 x4 x" w4 } F in P;
: X5 G+ h1 O0 n# X. O* f- |FF in P;
/ [9 h4 @- X( I+ b" o F in PFS;
FF in PFS;
1 v( ]( A0 i0 Q* `; L' i/ ^( B# QSet of subsets of { 1 .. 5 }
7 |- l7 b+ o. M8 O% ^Set of formal subsets of { 1 .. 5 }
" g; b2 ^+ B- o0 Q; Z, }true
- ]& p9 H1 E% T$ @false

>>  F in PFS;
      ^
; E& J; _  @- v" wRuntime error in 'in': Bad argument types

6 R8 H  \& w* S* d3 z+ ]( a
>> FF in PFS;
8 }. _" @* S  O3 O# j% t% k$ y      ^
Runtime error in 'in': Bad argument types