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

lilianjie

哪位能给理解下：
! [* E& A( e$ u1 ~) ]
+ a) b+ H" n" U" j! D( 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'.
$ b% ^" Z  V- G  O8 {3 F8 Q
The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
( l7 k/ x+ _# w6 j


( A+ i8 m5 [" n( Z/ ?+ W8 k* }S := { 1 .. 5};
> P := PowerSet(S);
2 ]! v4 P  ^, v. ?- G0 Y1 t7 yP;
( h) W2 X6 M3 F% f# Q& w; G- C6 cPFS:=PowerFormalSet(S);
3 `9 i* I1 N# Q# N7 yPFS;
F := { 2, 4 };
FF := { 2/3, 4 };
: J  z/ \* y& V. `/ }- `6 o( t- J
F in P;
" s9 K! n7 {& X- D; F" M) lFF in P;
F in PFS;
FF in PFS;
Set of subsets of { 1 .. 5 }
Set of formal subsets of { 1 .. 5 }
true
' V; a- a- X1 k/ H) m4 ~false

>>  F in PFS;
; {( d. C# W# T      ^
, e& j# B0 \% C5 t" m. fRuntime error in 'in': Bad argument types
( _  k* W$ ?# O* Y/ p

- V3 L3 @8 S0 N/ c' r>> FF in PFS;
      ^
9 K' }5 L8 p1 f2 ?Runtime error in 'in': Bad argument types