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

lilianjie

哪位能给理解下：
9 g9 I3 f) s- X. e$ y9 j
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.



4 [' A3 L% \" U2 A; m; {/ }8 BS := { 1 .. 5};
6 S/ D, Z: u9 L1 I> P := PowerSet(S);
P;
PFS:=PowerFormalSet(S);
9 N4 i! I: B/ o5 aPFS;
F := { 2, 4 };
FF := { 2/3, 4 };

F in P;
FF in P;
F in PFS;
FF in PFS;
* q( J; ^4 p5 d# k8 h9 tSet of subsets of { 1 .. 5 }
  X! ^3 _: R8 p. eSet of formal subsets of { 1 .. 5 }
: _/ e: s% ]! q: v" d* s  |5 |7 {true
false

>>  F in PFS;
! P4 e9 P) A. h3 D$ J      ^
Runtime error in 'in': Bad argument types
1 L8 ~6 D$ ?) a6 \1 m

>> FF in PFS;
      ^
Runtime error in 'in': Bad argument types