. Sets This introduces set theory from the point of view of a computer professional using ASCII. For the traditional notation see .See http://www.math.csusb.edu/notes/sets/sets.html For any type T there is an another type (symbolized by @T) of objects that are sets of objects of type T. For example {1,2,3} is a set of type @Nat because 1, 2 and 3 are of type Nat. The subsets of a given type are not (in MATHS) a type. However a set does belong to a particular type: a set A is of type @T if and only if A's elements must be of type T. It is therefore unambiguous to use the symbol/name for the type to be the universal set of that type. The main expressions involving sets in MATHS are: .As_is Expression Meaning Type. .As_is ------------------------------------------------------------------ .As_is {},\$() null set Overloaded .As_is T universal set @T .As_is @T Sets of elements of type T @@T .As_is {e1},\$(e1) singleton @T .As_is where e1 is of type T .As_is {e1,e2,e3,...} extension @T .As_is \$(e1,e2,...) extension @T .As_is where e1,e2 ,e3,... are all of type T .As_is {x:T || W(x) } intension @T .As_is \$[x:T](W(x)) intension @T There is a newer form: .As_is set{x:T. W(x)} intension @T .As_is e1 in S1 membership T><@T -> @ .As_is S1 & S2 intersection @T><@T -> @T(serial) .As_is S1 | S2 union @T><@T -> @T(serial) .As_is S1 ~ S2 complement @T><@T -> @T .As_is S1<> S2 inequality @T><@T -> @(parallel operator) .As_is S1 = S2 equality @T><@T -> @(parallel operator) .As_is S1==>S2 subset or equal @T><@T -> @(parallel operator) .As_is S1=>>S2 subset @T><@T -> @(parallel operator) .As_is S1>==S2 Partition @T><@@T ->@(parallel operator) .As_is S1 non-empty set @ (overloaded) .As_is SetOf(S) @S @@T .As_is Finite_sets(S) finite subsets of S @@T .As_is S@n Subsets of size n @@T .As_is ------------------------------------------------------------------ The '\$' (currency symbol) is a theoretical notation, the braces are a traditional shorthand. SetOf spells out the meaning of "@". Finite_sets a very common in computerized systems and computer science. Sample of Assumed Properties |- For x:T, x in T and not x in {} |- For e:T, e in {e} and e in {...,e,...} and e in {x:T||W(x)} iff W(e). Note. The .As_is |- symbol marks a statement that is asserted as being true - either as an axiom, or because it can be proved from other assertions. Definitions of Set Operations A & B::={c || c in A and c in B}, A | B::={c || c in A or c in B}, A ~ B::={c || c in A and not( c in B) }, Definitions of relationships |- For A,B, A = B iff A==>B and B==>A, For A,B, A==>B::= for all a:A(a in B), For A,B, A=>>B::= A==>B and not A=B. For A,B, A>==B::=( |B=A and for all X,Y:B(X=Y or X&Y={}) ), For A,B, A>==B iff for all a:A, one X in B(a in X). Useful abbreviations For A:Sets, a:Elements, A|a::=A|{a}, a|A::={a}|A, etc. Cardinallity -- size of a set |A| ::Nat0= `the number of elements in A`. A@n ::@A=`subsets of n elements taken from set A`