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

lilianjie

哪位能给理解下：
# C1 Q2 u% p9 W) C9 c  ~7 p$ q4 s
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'.
: S" }6 j1 T/ @7 n; w) J% y
The only set-theoretic operations that can be performed on formal sets are union, intersection, difference and symmetric difference, and element membership testing.
! T) z- O* m. E0 T# N. A

* F0 d& Y' n6 q8 K: g
S := { 1 .. 5};
" n- H: g. ~7 l# \5 E4 N+ ]: }> P := PowerSet(S);
' L! r3 Y2 R  ^* P: ^0 BP;
3 L1 g/ _1 ^8 M* cPFS:=PowerFormalSet(S);
PFS;
F := { 2, 4 };
FF := { 2/3, 4 };
% x: V: A& J+ p$ w/ J
2 u+ n$ {9 Q' B6 {* O" p5 f) G& w- `& y F in P;
FF in P;
F in PFS;
. ]) a* d  B4 c6 U$ nFF in PFS;
Set of subsets of { 1 .. 5 }
' V4 Z3 p8 [6 L* ^Set of formal subsets of { 1 .. 5 }
5 V6 g# [! j, E# H/ m& mtrue
false
$ F) P/ p  k* _8 ]( D, _2 b
$ a8 J0 A- s! m( _0 V+ M) Q' c& e>>  F in PFS;
, M; C  S' v% u' [. y      ^
# w. a0 A! g, Z; ARuntime error in 'in': Bad argument types
; d  x" g+ C/ R/ A# `" U

' z* s1 A$ E+ F0 O$ e>> FF in PFS;
8 ?+ N$ y. F/ o2 E8 O      ^
0 V! D& v. k+ V( `1 BRuntime error in 'in': Bad argument types