[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / logic_30_Sets
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Tue Aug 14 19:38:25 PDT 2012



      This introduces set theory from the point of view of a computer professional using ASCII. For the traditional notation see [ sets.html ]

      There is a less formal introduction to this theory in [ 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.


      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:

      1. Socrates is_a Human,
      2. Human are Mortal.
      3. (above)|-Socrates is_a Mortal.

      (Close Let )

      Here is another example, using the language of sets we can say:

    1. birds ==> fly, all birds fly.
    2. penguins ==> birds, penguins are birds.

      And so conclude (in the face of the evidence):

    3. penguins ==> fly.

      So we might rethink our assumptions:

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


      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.


    5. THEORY::=
        The use of sets is only distantly related to the theories of sets developed my mathematicians and logicians between 1850 through about 1940: [ logic_32_Set_Theory.html ]

      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:

      Set Expressions


        {} $() null set Ambiguous type.
        Tuniversal set @T
        {e1} $(e1) set(e1) singleton @T(e1:T)
        e1 {e1}@type(e1)(only if context requires a set)
        {e1,e2,e3,...} set(e1,e2,e3,...) $(e1,e2,e3,...) set of enumerated items@T(extension)
        {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)
        {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)
        $ Net{...}structured settype(Net{...})
        $ Nameset of elements with structure Nametype(Name)

        (Close Table)

        There is also a more readable format that is suitable for large sets made up of complex objects -- [ Long Format ] below.

        Long Format Representation

        For example
      1. my_pets::@Animals=following,
        • stranger, AKA "Megan"
        • shadow
        • ginger

        The raw source code is:

         	element, comment.
        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:

         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:
          Instead of
           	|- T = {e1,e2,...e[n]}.

        If the elements e1,e2,...,e[n] are distinct and free identifiers then the following syntax is natural short hand:
        It defines T and declares the elements in T. For example:
         	Direction::={down, up}.
           	|- Direction={down, up}.

        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:

         	Direction::={down, up}.
         	|- down <> up.
         	Lights::={Green, Amber, Red}.
         	|- 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 [ math_77_Enumerations.html ]

        Summary of Set Operators

        & ∩ ANDS1 & S2Intersection@T><@T->@T
        & ∩ AND& βIntersection@@T->@T
        | ∪ ORS1|S2union@T><@T->@T
        | ∪ ORunion@@T->@T
        ~ NOTS1 ~ S2Complement@T><@T->@T
        @ \powset SetOf@S1powerset,set_of_subsets@T->@@T
        >< ProductS1><S2Cartesian product@T><@T->@(T><T)

        (Close Table)

        Summary of Predicates

        in ∈e1 in S1membershipT><@T->@
        <>S1 <> S2inequality@T><@T->@
        !=S1 != S2inequality@T><@T->@
        ==S1 == S2equality@T><@T->@
        ==> ARES1 ==> S2subset or equal, ⊆@T><@T->@
        =>>S1 =>> S2proper subset, ⊂@T><@T->@
        somesome S1S1<>{}@T->@
        -S1some S1@T->@
        nono S1S1={}@T->@
        allall S1S1=T@T->@
        andS1 and S2some(S1&S2)@T->@

        (Close Table)

      Syntax of Set Expressions

    6. propositional_expression::= set_theoretical_proposition |...,

    7. set_theoretical_proposition::= |[T:Types] (expression(T) "in" expression(@T) | expression(@T) "=" expression(@T) | expression(@T)),

    8. For T:Types, expression(@T)::= simple_set_expression | union | intersection,

    9. union::= SERIAL(intersection,"|"),
       	Dog | Cat

    10. intersection::= SERIAL(complementary_set_expression,"&"),
       	Shot_haired & Barkless & Dog

    11. complementary_set_expression::= Cartesian_product | complementary_set_expression complement Cartesian_product.
    12. complement::="but_not" | "~", The text form is used in EBCDIC.

      Note. The above definition is expressed recursively to express the associativity of complements:

    13. A~B~C = (A~B)~C.

    14. complementary_set_expression = Cartesian_Product #(complement Cartesian_product).

    15. 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.
       	Point = Real >< Real.

    16. 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.
       	|{ {1,2}, {2,3} }
    17. = {1, 2, 3}.
       	&{ {1,2}, {2,3} }
    18. = {2}.

    19. 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")".
       	{ shadow, ginger }
       	( A \cup B ~ C )

    20. set_of_sets::= "@" simple_set_expression | simple_set_expression "@" expression(Nat0).
    21. @A = { B | B==>A }.
    22. A@n = { B:@A | Card(B) = n }.

        A@n was new and tentative on Thu Aug 19 at 11:20:05 PDT 1999 but became standard notation
      1. 2008-06-27 Fri Jun 27 08:06 .

    23. elementary_set::= intention | extension |comprehension | singleton | empty_set |type_name | "$"structure_description,
    24. 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


    25. intention::= "{" loose_binding #(","loose_binding ) "||" proposition "}" | "$" loose_bindings "(" proposition ")",
    26. comprehension::= "{" expression where_lexeme loose_binding #(","loose_binding ) "." proposition "}",
    27. where_lexeme::="||" | "." .
    28. extension::= finite_extension |informal_extension,
    29. finite_extension::="{" list_of_elements "}"| "$(" list_of_elements ")"
    30. informal_extension::= "{" list_of_elements "..." "}"|"$(" list_of_elements "..." ")",

      An informal extension will stop most automatic proof checkers from validating results.

    31. list_of_elements::= element #(punctuation element),
    32. singleton::= "{"element"}" | "$(" element ")".

    33. For Type T, e:T, e::@T={e}.

    34. 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:

    35. my_circle::=$ Net{x,y:Real, x^2+y^2=y^2 },
    36. CIRCLE::=Net{x,y:Real, r:Real, x0,y0:Real, (x-x0)^2+(y-y0)^2=r^2 },
    37. (CIRCLE)|-my_circle=$ CIRCLE(r=>1, (x0,y0)=>(0,0)}

    38. structure_description::= "$" documentation, [ notn_13_Docn_Syntax.html ] and [ notn_14_Docn_Semantics.html ]

    39. structure_expression::=R(expression), [ notn_12_Expressions.html ]

    40. |-structure_expression= "(" identifier "=>" expression #( (|",") identifier "=>" expression) ")",

      Semantics of Set Expressions


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

      1. |- (set0): t in {x:T||W(x)} iff W(t).

        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.

      2. |- (unambiguous_null_set): {}.@T = {x:T||false}.

        Universal set

      3. 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))}.

      4. 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:

      5. {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

      6. even = { 2*n || n:Nat0 }.

        Note. This is one place where variables are declared after they are used.

      7. (Set Operators)|- (union_semantics): For A,B: @T, A | B = {x:T || x in A or x in B }.

      8. (Set Operators)|- (intersection_semantics): For A,B: @T, A & B = {x:T || x in A and x in B }.
      9. (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
      10. ~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
      11. ~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

      12. For Type T, A:@T, ~A::= T~A.

        Equality of sets

      13. |- (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 [ semiring in math_41_Two_Operators ]

      14. For A,B:@T, A<>B iff not(A=B).


      15. For x,y:T1, x is y::=(x = y),
      16. For x:T1,X:@T1, x is_a X::=(x in X).

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


        How many elements are in this set?
      18. For X:@T, n:Nat0, |X| = n iff for n x:T (x:X).
      19. For Type T, Card[T]::@T->Nat0= map[X:@T](|X|).
      20. For Type T, X:@T, Card(X)::Nat0= Card[T](X).
      21. 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:

      22. For Type T, Finite_sets(T)::@T=the subsets S of T that are finite. [ types.html#Finite_sets ]
      23. For Type T, S:@T. Finite_sets(S)::@T={F:@S. F in Finite_sets(T) }.

        Notice that

      24. |- (fin1): For Type T, A,B:@T, if A==>B in Finite_sets(T) then A in Finite_sets(T).
      25. |- (fin2): For Type T, A,B:@T, if A in Finite_sets(T) then A&B in Finite_sets(T).
      26. |- (fin3): For Type T, A,B:@T, if A,B in Finite_sets(T) then A|B in Finite_sets(T).
      27. |- (fin4): For Type T, A,B:@T, if A in Finite_sets(T) then A~B in Finite_sets(T).

      28. |- (cardinality_of_union): for Type T, α, β:Finite_sets(T) ( Card(α | β ) = | α | + | β | - |α & β| ).

        We can define a property of sets:

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

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

      31. For X:@T, X::@= for some x:T(x in X),

      32. For X:@T, for some x:T(x in X) = Card(X)>0.

      33. 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:

      34. some(X)::= (X<>{}).
      35. no(X)::= (X={}).
      36. all(X)::= (X=T).
      37. A and B::= some (A & B).

        Here is a readable distfix expression:

      38. no A and B::= no (A & B).

        Set Operators

      39. For T:Types, A,B:@T, A & B::= {x:T || x in A and x in B} ,
      40. ::= "&".
      41. &::@@T -> @T,
      42. |-For β:@@T, &β={x:T || for all B:β(x in B)}.
      43. (above)|-A & B = &{A,B}.
      44. For T:Types, A,B:@T, A | B::= {x:T || x in A or x in B},
      45. ::= "|".
      46. |::@@T -> @T,
      47. |-For β:@@T, |β={x:T || for some B:β (x in B)},
      48. (above)|-A | B = |{A,B}.
      49. For T:Types, A,B:@T, A ~ B::= {x:T || x in A and not x in B},
      50. "but_not"::="~".

      51. (above)|-(@T,|,{},&,T,~) in Boolean_algebra.
        1. A&B = B&A.
        2. A|B = B|A.
        3. A&(B&C) = (A&B)&C.
        4. A|(B|C) = (A|B)|C.
        5. A | A = A.
        6. A & A = A.
        7. A~A={}.
        8. ...

          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.

        9. A~B = A & (T~B).
        10. ~(A&B) = T~(A&B) = (T~A)|(T~B) = ~A | ~B.
        11. ...

        (Cartesian products): these look like set expressions but are really part of the MATHS theory of types.

      52. For T:Types, A,B:@T, A><B::@(T><T)={ (a,b) || a in A and b in B }.

        (subsets): predicates.

      53. For T:Types, A,B:@T, A==>B::= for all a in A(a in B),
      54. ::= "==>".
      55. A<==B::= B==>A.
      56. all A are B::= (A==>B).
      57. For T:Types, A,B:@T, A=>>B::= A ==>B and A<>B,
      58. ::= "=>>".
      59. A<<=B::= B=>>A.

        There are many useful theorems for subsets:

        1. (above)|- (subseteq_reflexive): For all Types T, A:@T, A ==> A.
        2. (above)|- (subset_irreflexive): For all Types T, A:@T, not (A =>> A).

        3. (above)|- (subseteq_transitive): For all Types T, A,B,C:@T, if A ==> B ==> C then A ==> C.
        4. (above)|- (subset_transitive): For all Types T, A,B,C:@T, if A =>> B =>> C then A =>> C.
        5. (above)|- (subset_subseteq): For all Types T, A,B,C:@T, if A =>> B ==> C then A =>> C.
        6. (above)|- (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:

        7. (subseteq_transitive)|-(==>; ==>) = ==>.
        8. (subset_transitive)|-(=>>; ==>>) = =>>.
        9. (subset_subseteq)|-(=>>; ==>) = =>>.
        10. (subseteq_subset)|-(==>; =>>) = =>>.

        11. (above)|- (subset_complement): For all Types T, A,B:@T, if A ==> B then T~B ==> T~A.
        12. (above)|- (intersection_is_subset): for all Types T, A,B:@T, A & B ==> B and A & B ==>A.
        13. (above)|- (union_is_superset): for all Types T, A,B:@T, A ==> A | B and B ==> A | B.

        14. (above)|- (subset_union_form): for all Types T, A,B:@T, A==>B iff A | B = B.
        15. (above)|- (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?

        16. (above)|- (Product_of_subsets): for all Types T, A,B,C,D:@T, if A==>C and B==>D then A><B ==> C><C. This result is the basis for arguing that a license plate id with three letters and three digits will need six characters to encode it.

        Proofs are omitted but can be supplied by the reader as an exercise... [click here [socket symbol] Prove_subset_properties if you can fill this hole]

        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:

      60. Choice::@=For all A:Sets, π:partitions(A), some choice:π-->A, all B:π ( 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:

      61. |- (axiom_of_choice): Choice.

        This appears in other forms as part of the theory of relations and functions, [ Choice in logic_5_Maps ]

        The axiom of choice was used long before Zermelo made it an explicit axiom in 1904. It appears as the 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 [ Axiom_of_Choice ] in the Wikipedia.

        Also see Skolem functions in [ logic_5_Maps.html ]

      Proofs involving Sets

        The following proof patterns are common:
        To proveAssumeDeriveNotes
        A=Ba:Aa:BAnd also

        (Close Table)

        There are a large number of provable facts about sets

      1. (above)|- (glb): A<==A&B==>B.
      2. (above)|- (lub): A==>B|A<==B.

        There are also some easily proved derivation rules

      3. (above)|- (seteq): A=B iff A==>B and B==>A.
      4. (above)|- (converse): A==>B iff ~B==>~A.
      5. (above)|- (barbara): If A==>B==>C then A==>C.
      6. (above)|- (celarent): If no A are B and all C are B then no C is B.
      7. (above)|- (darii): If all M is P and some S are M then some S are P.
      8. (above)|- (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 [ syllogisms.html ]

      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

    41. penguin ⊂ aquatic & flightless & bird.
    42. ostriche ⊂ bird & flightless ~ aquatic.

      Representing complex families of sets -- ontologies or domains of discourse -- in this form make many consequence transparent. For example

    43. No penguin and ostriche, one is aquatic and the other is not.
    44. penguin | ostriche ⊂ flightless & bird ⊂ bird.

      For more on this see [ logic_8_Natural_Language.html ] (Semantics) and [ notn_16_Classification.html ] (Notation). Caveats when 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 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:

    45. large::@object->@object.

      Possibly with this definition in terms of an attribute size:object->Real&Positive.

    46. For S:@object, large(S) = {x:S. size(x) > 75 * mean(size o S)}, perhaps, or
    47. 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

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

    48. Chapter_14::PBI=following

      1. |-NONSTANDARD.
      2. T::Types.
      3. |-Set Operators // :: infix( T^T, @T, @T).
      4. For all f:T->T, A:@T, f//A = { f(x) || x:A }.
      5. For A,B,C:@T.
      6. (-1)|-| //{ {A,B}, {C} } = { |{A,B}, |{C} } = {A|B, C}.
      7. (-1)|-| | //{ {A,B}, {C} } = | {A|B, C } = A | B | C.
      8. (Set Operators)|-|{{A,B}, {C}} = {A,B,C }.
      9. (Set Operators)|-||{{A,B}, {C}} = |{A,B,C } = A | B | C.
      10. (above)|-| | //{ {A,B}, {C} } = ||{{A,B}, {C}} .

        Whiehead and Russell (PM *42) prove that

      11. (above)|- (infinite_union_associative): For all κ: @@@T, | |// κ = | | κ.
      12. (above)|- (infinite_intersection_associative): For all κ: @@@T, & &// κ = & | κ.

      (End of Net)


    49. 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:
    50. P::=A/p Thus, given for a1,a2:A, a1 =/p a2, for all b:B, a1 in b iff a2 in b.


    Tree by Knuth

      Source: Knuth 69, Vol 1, Section 2.3 Trees p305

      A typical tree is T where

      1. T::=(nodes=>{1,1.1,1.2,1.2.3}, root=>1, m=>2, subtree=>(T1,T2)),
      2. T1:=(nodes=>{1.1}, root=>1.1, m=>0, subtree=>()),
      3. T2:=(nodes=>{1.2,1.2.3}, root=>1.2, m=>1, subtree=>(T3)),
      4. T3:=(nodes=>{1.2.3}, root=>1.2.3, m=>0, subtree=>()).

      Definition of a tree

    1. TREE::=

      1. |-numbers.
      2. nodes::Finite(Sets),
      3. root::nodes,
      4. fan_out::Nat0,
      5. subtree::1..fan_out->@nodes, -- These are ordered trees
      6. |-nodes~{root}>== {subtree(i) || i:1..m},
      7. |-For all i:1..m, subtree(i) in $ TREE.


      |-For T:$ TREE, i:Nat0, T[i]::=T.subtree[i].

      ??{convergence because lim |nodes|=0}??

    2. forest::={F:@TREES||for T1,T2:F(no T1&T2)}

    3. (above)|-if T:$ TREE then T~{root} in forest.

. . . . . . . . . ( end of section Sets) <<Contents | End>>

Notes on MATHS Notation

Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

For a complete listing of pages in this part of my site by topic see [ home.html ]

Notes on the Underlying Logic of MATHS

The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

For a more rigorous description of the standard notations see

  • STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  • above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  • given::reason="I've been told that...", used to describe a problem.
  • given::variable="I'll be given a value or object like this...", used to describe a problem.
  • goal::theorem="The result I'm trying to prove right now".
  • goal::variable="The value or object I'm trying to find or construct".
  • let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  • hyp::reason="I assumed this in my last Let/Case/Po/...".
  • QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  • QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  • RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.