.Open 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 There is a less formal introduction to this theory in .See http://www.csci.csusb.edu/dick/maths/intro_sets.html . Rapid History Sets are implicit in much of Aristotlean logic (Ancient Greece... Medieval). George Cantor (1800's) developed the theory as part of his research into the mathematics of infinity. Sets rapidly became the language of modern mathematics. Russell (1990's) uncovered paradoxes in the Cantor theory. This lead to the Zermelo-Frankel axiomatic theory($THEORY below), Halmos's Naive set theory, and Whitehead and Russell's Theory of Types. . Introduction These notes are about a language that lets talk both naturally and rigorously at the same time. Everyday language is full of references to sets of objects, classes, types of things, and on. The simple notation proposed here makes much of this rigorous. Sets also form a foundation for several more complex ideas which together form a simple yet effective way of talking about complex pieces of software - such IBM's CICS(Customer Information C?? Systems), elevators, or Hotel Bookings for example. For example, using the language of sets we can say: birds ==> fly, all birds fly. penguins ==> birds, penguins are birds. And so conclude (in the face of the evidence): penguins ==> fly. So we might rethink our assumptions: birds = flightless | flying. Birds are flying or flightless. This might lead us to think about how big the various sets are and conclude that most birds are not flightless... . Types Every object belongs to a type T -- where the type describes the kind of things that can be done to the object or could produce objects of the type. For any type T there is an another type symbolized by @T with objects that are sets of objects of type T. .Note THEORY::=Net{ The use of sets is only distantly related to the theories of sets developed my mathematicians and logicians between 1850 through about 1940: .See http://www/dick/maths/logic_32_Set_Theory.html }=::THEORY. A key point is that in theory one can re-express statements in MATHS that use sets into expressions that use predicates instead. Some sets are not types - A type by definition is a universal set or domain of discourse, but a set is determined by the type of element plus some rule(predicate) indicating what is in the set. We assume that whenever we have a set of some kind or other than it is a set of objects of the same type. However a subset (or a `set` for short) does belong to a type and so determines the types of the elements in it. It is therefore safe to use a subset of a type in a declaration of a variable of the right type, and with values/properties limited to those of the set(compare type and subtype in Ada). The restriction that each set has elements all of the same type is not a particularly restrictive rule given the freedom with which we can construct types as we need them. The main expressions involving sets in MATHS are: .Open Set Expressions . Constructors .Table Form Meaning Type (Notes) .Row {} $() null set Ambiguous type. .Row T universal set @T .Row {e1} $(e1) set(e1) singleton @T (e1:T) .Row e1 {e1} @type(e1) (only if context requires a set) .Row {e1,e2,e3,...} set(e1,e2,e3,...) $(e1,e2,e3,...) set of enumerated items @T (extension) .Row {x:T || W(x)} {x:T. W(x)} $[x:T](W(x)) set(x:T WHERE W(x)) set of things satisfying a property W @T (intension) .Row $ Net{...} structured set type(Net{...}) .Row $ Name set of elements with structure Name type(Name) .Close.Table There is also a more readable format that is suitable for large sets made up of complex objects -- .See Long Format below. . Long Format Representation For example my_pets::@Animals=following, .Set stranger, AKA "Megan" shadow ginger .Close.Set The raw source code is: .As_is .Set .As_is element .As_is element, comment. .As_is ... .As_is .Close.Set An element in a long set can be several lines long. It starts with an indentation. Each element is an expression and may be terminated by a comma and a comment. Comments are ignored. Long sets are normally used with a definition like this: .As_is Name::@Type = following, When rendered for display or printing a long set should shown as an unordered list with each element marked with a bullet or similar marker. . Enumerating Finite Sets In computing and software engineering we often need to introduce and then describe a finite set of distinct named elements. One way to this is: .Box Instead of .As_is T::Sets, .As_is e1::T, .As_is e2::T, .As_is ... .As_is e[n]::T, .As_is |- T = {e1,e2,...e[n]}. .Close.Box If the elements e1,e2,...,e[n] are distinct and free identifiers then the following syntax is natural short hand: .As_is T::={e1,e2,...,e[n]} It defines T and declares the elements in T. For example: .As_is Direction::={down, up}. means .Box .As_is Direction::Sets. .As_is down::Direction. .As_is up::Direction. .As_is |- Direction={down, up}. .Close.Box Note, that the above does not guarantee that the elements have to be different -- even if we use different identifiers for the elements. As written, it is possible for some else to take our document and reuse it with a substitution which makes two variables the same. To stop this, and to be very clear about what we want we must add extra assumptions like this: .As_is Direction::={down, up}. .As_is |- down <> up. or .As_is Lights::={Green, Amber, Red}. .As_is |- 3 Lights. See $Cardinality below. This is a little clumsy and counter-intuitive, and so I may add a new notation that handles this. If you want the elements to be in order then see .See http://www/dick/maths/math_77_Enumerations.html . Summary of Set Operators .Table Symbols Example Meaning Type .Row & \cap AND S1 & S2 Intersection @T><@T->@T .Row & \cap AND & \beta Intersection @@T->@T .Row | \cup OR S1|S2 union @T><@T->@T .Row | \cup OR |\beta union @@T->@T .Row ~ NOT S1 ~ S2 Complement @T><@T->@T .Row @ \powset SetOf @S1 powerset,set_of_subsets @T->@@T .Row >< Product S1><@T->@(T><@T->@ .Row <> S1 <> S2 inequality @T><@T->@ .Row != S1 != S2 inequality @T><@T->@ .Row == S1 == S2 equality @T><@T->@ .Row ==> ARE S1 ==> S2 subset or equal @T><@T->@ .Row =>> S1 =>> S2 proper subset @T><@T->@ .Row some some S1 S1<>{} @T->@ .Row - S1 some S1 @T->@ .Row no no S1 S1={} @T->@ .Row all all S1 S1=T @T->@ .Row and S1 and S2 some(S1&S2) @T->@ .Close.Table .Close . Syntax of Set Expressions propositional_expression::= set_theoretical_proposition |..., set_theoretical_proposition::= |[T:Types] (expression(T) "in" expression(@T) | expression(@T) "=" expression(@T) | expression(@T)), For T:Types, expression(@T) ::= simple_set_expression | union | intersection, union::= SERIAL($intersection,"|"), .As_is Dog | Cat intersection::= SERIAL($complementary_set_expression,"&"), .As_is Shot_haired & Barkless & Dog complementary_set_expression::= $Cartesian_product #($complement $Cartesian_product) complement::="but_not" | "~", The text form is used in EBCDIC. .As_is Animal~Dog Cartesian_product::= SERIAL($possible_prefix_set_expression, "><"). Note: Cartesian products are sets of pairs of elements and are actually a subset of a different type. .As_is Point = Real >< Real. possible_prefixed_set_expression::= #( "|" | "&") $simple_set_expression. Note: in fact the simple expression must return a set of sets for a prefix to be OK. If there are 2 prefixes then it must be a set of set of sets. .As_is |{ {1,2}, {2,3} } = {1, 2, 3}. .As_is &{ {1,2}, {2,3} } = {2}. simple_set_expression::=set_name | elementary_set |"("$set_expression")" | set_of_sets | set_of_maps | set_of_relations | simple_set_expression"."relational_expression | relational_expression "("set_expression")". .As_is Animal .As_is { shadow, ginger } .As_is ( A \cup B ~ C ) .As_is @Animal .As_is A<>->B .As_is shadow.breeds .As_is breeds(shadow) set_of_sets::= "@" simple_set_expression | simple_set_expression "@" expression(Nat0). .As_is @Animals .As_is Animals@2 @A = { B | B==>A }. A@n = { B:@A | Card(B) = n }. .Box A@n was new and tentative on Thu Aug 19 at 11:20:05 PDT 1999 but became standard notation 2008-06-27 Fri Jun 27 08:06 . .Close.Box elementary_set::= intention | extension | singleton | empty_set |type_name | "$"structure_description, empty_set::="{}"|"$()", intention::= "{" loose_binding #(","loose_binding ) "||" proposition "}" | "$" loose_bindings "(" proposition ")", extension::= finite_extension |informal_extension, finite_extension::="{" list_of_elements "}"| "$(" list_of_elements ")" informal_extension::= "{" list_of_elements "..." "}"|"$(" list_of_elements "..." ")", An informal extension will stop most automatic proof checkers from validating results. list_of_elements ::= element #(punctuation element), singleton::= "{"element"}" | "$(" element ")". For Type T, e:T, e::@T={e}. element::= expression, MATHS has a special way to define a set - by describing it as a collection of tuples under some constraint. Any piece of documentation contains declarations and axioms that can be interpreted this way. Examples might be: my_circle::=$ Net{x,y:Real, x^2+y^2=y^2 }, CIRCLE::=Net{x,y:Real, r:Real, x0,y0:Real, (x-x0)^2+(y-y0)^2=r^2 }, (CIRCLE)|- my_circle=$ $CIRCLE(r=>1, (x0,y0)=>(0,0)} structure_description::= "$" documentation, .See http://www/dick/maths/notn_13_Docn_Syntax.html and .See http://www/dick/maths/notn_14_Docn_Semantics.html structure_expression::=R(expression), .See http://www/dick/maths/notn_12_Expressions.html |- structure_expression= "(" identifier "=>" expression #( (|",") identifier "=>" expression) ")", .Open Semantics of Set Expressions . Definitions (intension_semantics): For Type T, W:predicate, x:variable(T), {x:T||W(x)}::@T= `set of all x in T that satisfy W(x)`. (in): For Type T, A:@T, t:T, t in A ::@=`it is true that t is a member of set A`. |- (set0): t in {x:T||W(x)} iff W(t). {}::@T= {x:T||false}, T::@T= {x:T||true}, (singleton_semantics): For a,b,c,...: T, {a}::@T={x:T||x=a}. (coerced_singleton): For a,b,c,...: T, a::@T={a}. (extension_semantics): For a,b,c,...: T, {a,b,c,...} ::@T= {a} | {b} | {c}|... . (projection_semantics): For f,x,W, {f(x) || for some x:T (W)}::= {y || for some x:T(y=f(x) and (W))}. For f,x,X,W, {f(x) || x:X}::= {y || for some x:X(y=f(x))}. (Set Operators)|- (union_semantics): For A,B: @T, A | B = {x:T || x in A or x in B }. (Set Operators)|- (intersection_semantics): For A,B: @T, A & B = {x:T || x in A and x in B }. . Equality of sets |-(eqsets):for A,B:@T, if for all x:T(x in A iff x in B) then A=B. An object is a set when and only when membership solely determines equality. "Bags" have the same abstract operators as "Sets" but two bags are equal only when their members occur the same number of times in both Bags. Formally a "Bag of X's" is an object of type Nat^X. The most general form of this model will be found under .See http://www/dick/maths/math_41_Two_Operators.html#semiring For A,B:@T, A<>B iff not(A=B). . Conveniences For x,y:T1, x is y::=(x = y), For x:T1,X:@T1, x is_a X::=(x in X). . Cardinality `How many elements are in this set?` For X:@T, n:Nat0, |X| = n iff for n x:T (x:X). For Type T, Card[T]::@T->Nat0= map[X:@T](|X|). For Type T, X:@T, Card(X) ::Nat0= Card[T](X). For Type T, A:@T, n:Nat0, A@n = { X:@T || Card[T](X) = n }. Note: avoid using /Card(n) or /|_|(n) as it does not define the types of objects being counted. |-(cardinality_of_union): for Type T, \alpha, \beta:FiniteSet(T) ( Card(\alpha | \beta ) = | \alpha | + | \beta | - |\alpha & \beta| ). . Quantifiers expressed using sets For all X:@T, X=T iff for all x:T(x in X), A set in a context that demands a proposition is true iff there exists at least one member. For X:@T, X::@= for some x:T(x in X), For X:@T, for some x:T(x in X) = Card(X)>0. For X:@T, if |X|=1 then the(A) ::= the(x:T||x in A). There are short hand ways of stating properties of sets so that they can be used easily: some(X)::= (X<>{}). no(X)::= (X={}). all(X)::= (X=T). A and B::= some (A & B). Here is a readable distfix expression: no A and B::= no (A & B). . Set Operators For T:Types, A,B:@T, A & B::= {x:T || x in A and x in B} , \cap::= "&". & :: @@T -> @T, |- For \beta:@@T, &\beta={x:T || for all B:\beta(x in B)}. (above)|- A & B = &{A,B}. For T:Types, A,B:@T,A | B::= {x:T || x in A or x in B}, \cup::= "|". | :: @@T -> @T, |- For \beta:@@T, |\beta={x:T || for some B:\beta (x in B)}, (above)|- A | B = |{A,B}. For T:Types, A,B:@T,A ~ B::= {x:T || x in A and not x in B}, "but_not"::="~". (above)|- (@T,|,{},&,T,~) in Boolean_algebra. .Box A&B = B&A. A|B = B|A. A&(B&C) = (A&B)&C. A|(B|C) = (A|B)|C. A | A = A. A & A = A. A~A={}. ... .Close.Box (Cartesian products): these look like set expressions but are really part of the MATHS theory of types. For T:Types, A,B:@T, A>B::= for all a in A(a in B), \subseteq::= "==>". A<==B ::= B==>A. all A are B::= (A==>B). For T:Types, A,B:@T,A=>>B::= A ==>B and A<>B, \subset::= "=>>". A<<=B ::= B=>>A. . The Axiom of Choice $MATHS assumes that given a collection of disjoint sets, then we can choose one member of each to be a representative of that set. Formally: Choice::@=For all A:Sets, \pi:partitions(A), some choice:\pi-->A, all B:\pi ( choice(B) in B). Notice that this assumption is `obviously` true for finite cases.... it is some the weirder infinite sets that make it doubtful. The following formally asserts that the axiom of choice is part of the $MATHS system: |- (axiom_of_choice): $Choice. This appears in other forms as part of the theory of relations and functions, .See http://www/dick/maths/logic_5_Maps.html#Choice The axiom of choice was used long before Zermelo made it an explicit axiom in 1904. It appears as the .Key axiom of selection in `Principia Mathematica`. It was discussed for a long time but is used by praticing mathematicians without qualams. For more history, see .See http://http://en.wikipedia.org/wiki/Axiom_of_Choice in the Wikipedia. Also see Skolem functions in .See http://www/dick/maths/logic_5_Maps.html .Close .Open Proofs involving Sets The following proof patterns are common: .Table To prove Assume Derive Notes .Row A==>B a:A b:B .Row no(A) a:A $RAA .Row A=B a:A a:B And also .Row - b:B b:A .Close.Table There are a large number of provable facts about sets ()|-(glb): A<==A&B==>B. ()|-(lub): A==>B|A<==B. There are also some easily proved derivation rules ()|-(seteq): A=B iff A==>B and B==>A. ()|-(converse): A==>B iff T~B==>T~A. ()|-(barbara): If A==>B==>C then A==>C. ()|-(celarent): If no A are B and all C are B then no C is B. ()|-(darii): If all M is P and some S are M then some S are P. ()|-(ferio): If no M is P and some S are M then some S are T~P. And so on thru most of the medieval catagorical syllogisms .See http://ftp.csci.csusb.edu/dick/samples/syllogisms.html .Close . Families of sets .See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html . Chapter 42 -- Partly Baked Idea This comes from rereading section 42 of Principia Mathematica and noticing a couple of odd theorems about the union and intersection of sets of sets of set. I doubt if they will be useful. They force the use of a nonstandard notation for the set extension of a function, so I'm enclosing them in a Net. Chapter_14::PBI=following .Net |- NONSTANDARD. T::Types. |- Set Operators // :: infix( T^T, @T, @T). For all f:T->T, A:@T, f//A = { f(x) || x:A }. For A,B,C:@T. (-1)|- | //{ {A,B}, {C} } = { |{A,B}, |{C} } = {A|B, C}. (-1)|- | | //{ {A,B}, {C} } = | {A|B, C } = A | B | C. (Set Operators)|- |{{A,B}, {C}} = {A,B,C }. (Set Operators)|- ||{{A,B}, {C}} = |{A,B,C } = A | B | C. (above)|- | | //{ {A,B}, {C} } = ||{{A,B}, {C}} . Whiehead and Russell (PM *42) prove that (above)|- (infinite_union_associative): For all \kappa: @@@T, | |// \kappa = | | \kappa. (above)|- (infinite_intersection_associative):For all \kappa: @@@T, & &// \kappa = & | \kappa. .Close.Net . MinTerms MINTERM::={ A:Sets, B:@A, p::=map[ a:A] (map b:B(a in b)). For each a in A there is an array of true/false values, one for each set in B, named p(a). We can partition A into cells of elements with the same array of values: P::=A/p Thus, given for a1,a2:A, a1 =/p a2, for all b:B, a1 in b iff a2 in b. }=::MINTERM. .Open Tree by Knuth .Source [Knuth 69, Vol 1, Section 2.3 Trees p305] A typical tree is `T` where .Box T::=(nodes=>{1,1.1,1.2,1.2.3}, root=>1, m=>2, subtree=>(T1,T2)), T1:=(nodes=>{1.1}, root=>1.1, m=>0, subtree=>()), T2:=(nodes=>{1.2,1.2.3}, root=>1.2, m=>1, subtree=>(T3)), T3:=(nodes=>{1.2.3}, root=>1.2.3, m=>0, subtree=>()). .Close.Box . Definition of a tree TREE::=Net{ |-numbers. nodes::Finite(Sets), root::nodes, fan_out::Nat0, subtree::1..fan_out->@nodes, -- These are ordered trees |-nodes~{root}>== {subtree(i) || i:1..m}, |-For all i:1..m, subtree(i) in $ $TREE. }=::TREE. |-For T:$ $TREE, i:Nat0, T[i]::=T.subtree[i]. ??{convergence because lim |nodes|=0}?? forest::={F:@TREES||for T1,T2:F(no T1&T2)} ()|- if T:$ $TREE then T~{root} in forest. .Close . Idea This is a new idea designed to handle natural expressions like `flightless bird`. An `epithet` is a word or phrase written in front of the name of a set (not an expression). It is always a subset of the named set. constrained_set_name ::= #epithet set_name. Like this perhaps flightless bird There is a risk of confusion when talking about sets of strings. A formal justification for the syntax is by defining a prefix operator on sets of the correct type: flightless::prefix(@animal) = S+>{b:S. `b can not fly`}. For A:@Animal, flightless A::@Animal = {b:A. `b can not fly`}. Should this be abbreviated to .As_is flightless::epithet(Animal) = `_ can not fly'. .Close Sets