.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 Aristotelian 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 systems and so software - such IBM's CICS(Customer Information C?? Systems), elevators, or Hotel Bookings for example. The classic argument looks like this in the language of sets: .Let Socrates is_a Human, Human are Mortal. ()|- Socrates is_a Mortal. .Close.Let Here is another 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 {e(x) || x:S, W(x)} {e(x). x:S, W(x)} set of vales of e(x) for som x satisfying W(x) @T (comprehension) .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, \subseteq @T><@T->@ .Row =>> S1 =>> S2 proper subset, \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 | complementary_set_expression$complement $Cartesian_product. complement::="but_not" | "~", The text form is used in EBCDIC. .As_is Animal~Dog .As_is Animal~Dog~Cat Note. The above definition is expressed recursively to express the associativity of complements: A~B~C = (A~B)~C.$complementary_set_expression = $Cartesian_Product #($complement $Cartesian_product). 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 |comprehension | singleton | empty_set |type_name | "$"structure_description, empty_set::="{}"|"$()", Note "{}" is ambiguous as to type.... is a setof no animals, or a set of no real numbers. The type of "{}" needs to be worked out from the context. To remove the ambiguity use .As_is {}.@Animal intention::= "{" loose_binding #(","loose_binding ) "||" proposition "}" | "$" loose_bindings "(" proposition ")", comprehension::= "{" expression$where_lexeme loose_binding #(","loose_binding ) "." proposition "}", where_lexeme::="||" | "." . 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). .Key null set or empty set {}::@T= {x:T||false}, Note "{}" the type of "{}" above is @T and not determined by the symbol itself. It is determined by the context of the symbol. To remove all ambiguity use the standard MATHS technique of using ".type" to define the type. |- (unambiguous_null_set): {}.@T = {x:T||false}. .Key Universal set 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))}. (Comprehension semantics): an expression like {e || x:X, y:Y, ..., W} should be interpreted as a generalisation of the above whenever e is an expression and W a proposition: {z || for some x:X, y:Y, ... (z=e and (W))} If the W is missing it should be taken to be true. For example even = { 2*n || n:Nat0 }. Note. This is one place where variables are declared after they are used. (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 }. (Set Operators)|- (complement_semantics): For A,B: @T, A ~ B = {x:T || x in A and not x in B }. . Unary Complement Operator Expression like this ~Cat are best thought of as abbreviations when the type of the set is known. If for example Cat is a subset of a type called Animal then ~Cat = Animal ~ Cat. However, the null set symbol {} has no defined type and so it's complement is undefined. Here is an attempt to catch this For Type T, A:@T, ~A::= T~A. . 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). For Type T, A:@T, ~A ::= T~A. Note, if the type of the elements of a set A is undefined then the complement of A is also undefined. . 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. Instead the expression T@n defines the type and the number of elements. . Finite Sets A finite set can be formally defined as a set that can not be put into a one-one correspondence to a proper subset of itself. We can describe: For Type T, Finite_sets(T)::@T=the subsets S of T that are finite. .See ./types.html#Finite_sets For Type T, S:@T. Finite_sets(S)::@T={F:@S. F in Finite_sets(T) }. Notice that |-(fin1):For Type T, A,B:@T, if A==>B in Finite_sets(T) then A in Finite_sets(T). |-(fin2):For Type T, A,B:@T, if A in Finite_sets(T) then A&B in Finite_sets(T). |-(fin3):For Type T, A,B:@T, if A,B in Finite_sets(T) then A|B in Finite_sets(T). |-(fin4):For Type T, A,B:@T, if A in Finite_sets(T) then A~B in Finite_sets(T). |-(cardinality_of_union): for Type T, \alpha, \beta:Finite_sets(T) ( Card(\alpha | \beta ) = | \alpha | + | \beta | - |\alpha & \beta| ). We can define a property of sets: For Type T, S:@T, finite(S)::bool= (S in Finite_sets(T)). However me must avoid expressions that contain "/finite(P)". . 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={}. ... Note. ~A is a well defined set expression as long as A is a subset of a known type T. Instead in MATHS if A is a subset of a Type T then ~A= T~A. A~B = A & (T~B). ~(A&B) = T~(A&B) = (T~A)|(T~B) = ~A | ~B. ... .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::= "==>". .As_is \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::= "=>>". .As_is \subset::="=>>" A<<=B ::= B=>>A. There are many useful theorems for subsets: .Box ()|- (subseteq_reflexive): For all Types T, A:@T, A ==> A. ()|- (subset_irreflexive): For all Types T, A:@T, not (A =>> A). ()|-(subseteq_transitive): For all Types T, A,B,C:@T, if A ==> B ==> C then A ==> C. ()|-(subset_transitive): For all Types T, A,B,C:@T, if A =>> B =>> C then A =>> C. ()|-(subset_subseteq): For all Types T, A,B,C:@T, if A =>> B ==> C then A =>> C. ()|-(subseteq_subset): For all Types T, A,B,C:@T, if A ==> B =>> C then A =>> C. Note: these are easier to write using the relational product: (subseteq_transitive)|- (==>; ==>) = ==>. (subset_transitive)|- (=>>; ==>>) = =>>. (subset_subseteq)|- (=>>; ==>) = =>>. (subseteq_subset)|- (==>; =>>) = =>>. ()|- (subset_complement): For all Types T, A,B:@T, if A ==> B then T~B ==> T~A. ()|-(intersection_is_subset): for all Types T, A,B:@T, A & B ==> B and A & B ==>A. ()|-(union_is_superset): for all Types T, A,B:@T, A ==> A | B and B ==> A | B. ()|-(subset_union_form): for all Types T, A,B:@T, A==>B iff A | B = B. ()|-(subset_intersection): for all Types T, A,B:@T, A==>B iff A = A&B. We could use the above two eqivalences to reason algebraically about subsets. They are both inspired by lattice theory. Some of these theorems are also stated below...$TBA? ()|-(Product_of_subsets): for all Types T, A,B,C,D:@T, if A==>C and B==>D then A> C>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 practicing mathematicians without qulams. 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 ~B==>~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 ~P. And so on thru most of the medieval catagorical syllogisms .See http://ftp.csci.csusb.edu/dick/samples/syllogisms.html .Close . Epithets and term logic -- Use Sets instead This is a the 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. There is a risk of confusion when talking about sets of strings. What would be very handy would be able to have positive and negative epithets. The effect would be like including term logic into MATHS. Use '&' and '~' to construct terms penguin \subset aquatic & flightless & bird. ostriche \subset bird & flightless ~ aquatic. Representing complex families of sets -- ontologies or domains of discourse -- in this form make many consequence transparent. For example No penguin and ostriche, one is aquatic and the other is not. penguin | ostriche \subset flightless & bird \subset bird. For more on this see .See ./logic_8_Natural_Language.html (Semantics) and .See ./notn_16_Classification.html (Notation). Caveats when .Key translating natural language into sets. First, these classifications in natural language are often based on defining arbitrary boundaries. Sometimes you need to attach attributes to the elements of a set to get a consistent and realistic logic. The classic example would be the adjective bearded when applied to the set of men. Here is the .Key argument of the beard. Where do you draw the boundary between bearded and beardless? What happens when you take a bearded person and start removing hairs from the face... when do they become beardless. If we reverse the process and let one hair grow at a time... when has the person become bearded. Second, one needs to be careful of adjectives that define subsets relative to the superset. For example: large and small are not absolutes. A 'small elephant is larger (I guess) than a large dog. So large & dog does not encode the semantics of large correctly. It can not be a separate set. Instead it should be defined as a map from a set into a subset: large::@object->@object. Possibly with this definition in terms of an attribute size:object->Real&Positive. For S:@object, large(S) = {x:S. size(x) > 75 * mean(size o S)}, perhaps, or large(S) = top_quartile[size](S), (if you define top_quartile)... By the way, as a final warning -- what about bearded dog? One must be careful to defines sets as subsets and not translate the terms that move the subsets outside of their sets -- except for humorous, poetic, or other creative processes. Perhaps a traditional Philosophy 101 course would be wise... . Families of sets .See http://www.csci.csusb.edu/dick/maths/logic_31_Families_of_Sets.html . Principia Mathematica 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 .Close Sets