. 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`