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

lilianjie

哪位能给理解下：

Formal Sets
9 i" j3 C$ u9 Q, u2 E& LA 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.

- T" ^! N! z! G& t5 q7 A
7 e6 e$ W2 B8 N, p* Z0 K' c0 F( A
S := { 1 .. 5};
/ U  H* u$ `- E, T> P := PowerSet(S);
- J' g0 f+ b5 t, c% [+ }5 WP;
PFS:=PowerFormalSet(S);
' D3 H, _. _1 R. u5 B4 pPFS;
" J2 @) z" ^( I/ NF := { 2, 4 };
FF := { 2/3, 4 };
6 B4 T5 V/ f6 ]3 Y9 \6 q
F in P;
FF in P;
F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
) Q- b, v# _1 zSet of formal subsets of { 1 .. 5 }
true
2 m' r3 f; ^3 u; d  y# T1 Ifalse
: f- f  t0 h! R; `4 N& T
* {" j4 S4 D+ m" r8 o% C>>  F in PFS;
      ^
Runtime error in 'in': Bad argument types

, q/ z* I3 B* O% ]
+ l& b+ T7 n) @! B3 E6 Y>> FF in PFS;
/ k# L% Z5 _8 H      ^
0 m, a5 Q8 g- ~5 w% b/ k* K' d9 MRuntime error in 'in': Bad argument types