[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_21_Order
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sun Oct 9 11:22:53 PDT 2011




      A set of elements is said to be ordered if it has a relationship with special properties defined on it. Here are some standard examples:
      Set of ElementsRelationships that impose an order
      Planscheaper, easier, more fun, do_before, ...
      Productssafer, cheaper, faster, bigger, smaller, better, worse,...
      EventsOccurs before, more likely than,...
      NumbersLess than, greater then, less then or equal, greater then equal
      Natural Numbersdivides
      Points in spaceabove, below, to the right, to the left, before, behind
      Components in a systemis a part of (APO), part_whole, composition
      Types of Objectsis a kind of (AKO), inheritance, derived_from, subtype_supertype
      Parts of a programdepends on
      Subsets of a set==>(subset of)
      Setsfunctional dependency(there exists a many-one mapping from _ to _)
      Setsexistence dependency(for each _ there must exist a unique fixed _)
      LettersEarlier in the alphabet
      Wordsdictionary order (lexographic order)
      Boolean Valuesimplies
      {a,b,c,x,y,z}{(a,x),(a,y),(a,z), (b,x), (b,y), (b,z), (c,x), (c,y), c,z)}

      (Close Table)

      Here are some relations that are not orders in this technical sense:
      Set of ElementsRelationships
      Points in spaceclose to, surrounding
      NumbersHaving the same remainder with respect to a particular divisor

      (Close Table)

      Take for example a set of components/modules/classes/pieces of a program and the relation of one part depending on another. In other words if one changes then the dependent module may also have to be changed. Now if part A depends on part B and part B depends on part C then we would expect A to also depend on C indirectly. We call this transitivity (see standard). But, We would not want A part to depend B and B to depend on A, this would imply a difficult time making changes. The property that stops this is called antisymmetry.

      The following definitions and theorems are to be found in

    1. standard::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html

      (standard) |-For X:Sets, Quasi_orders(X) ::= Reflexivity(X) & Transitive(X) ,

      (standard) |-For X, Partial_orders(X) ::=Quasi_orders(X)& Antisymmetric(X),

      (standard) |-For X, Strict_partial_orders(X) ::= Irreflexive(X) & Transitive(X), (standard) |-For X, Total(X) ::={R:@(X,X)|| @(X,X)~R = /R },

      (standard) |-For X, Connected(X) ::={R:@(X,X)|| Total(X) and R | /R = @(X,X)}.

    2. (standard)|- (ITisAT): For X:Sets, Irreflexive(X) & Transitive(X) = Asymmetric(X) & Transitive(X).

      The following defines the formal structure of all ordered sets - a set of elements and four relations that may or may not hold betwee any pair of elements in the set.

    3. BASIC_ORDER::=
      1. Set::Sets,
      2. relation::@(Set,Set),
      3. strict_relation::@(Set,Set),
      4. strict::=strict_relation,
      5. inverse::@(Set,Set),
      6. strict_inverse::@(Set,Set).
      7. |- (BO1): inverse = /relation.
      8. |- (BO2): strict_inverse = /strict_relation.

      Note. I could have used definitions rather than declarations+axioms. Using axioms makes it clear that I wish to supply a relation and have the inverse derived from it as in ORDER and I wish to supply an inverse and derive the relation from it as in STRICT_ORDER below.

    4. ORDER::=

      1. |-BASIC_ORDER.
      2. |- (O0): relation in Transitive(Set) & Reflexive(Set) & Antisymmetric(Set).
      3. |- (O1): strict_relation=relation~Id(Set),
      4. (O0, def)|- (O2): strict in Transitive(Set) & Asymmetric(Set).
      5. (O2, ITisAT)|- (O3): strict in Irreflexive(Set).

      6. (O1, O2, O3)|- (Splitting theorem): (=)= relation & inverse.

      7. not_comparable_with::@(Set,Set)= @(Set,Set) ~strict_inverse~ strict.
      8. (Sets) |- finite::@= (Set in FiniteSets).
      9. total::@= (relation in Total(Set)).
      10. (def)|- (O4): if total then not_comparable_with = {}.

      Note. The two conditions, finite and total can be asserted, denied, or left undetermined whenever the ORDER is reused: for example
    5. (ORDER)|-ORDER(Set=>1..100, relation=>divides, finite, not total).

      Exercise: Verify that

    6. (ORDER)|-ORDER( Set=>Int, relation=>(<=), inverse=>(>=), strict=>(<), strict_inverse=>(>), not finite, total, ...).

    7. STRICT_ORDER::=

      1. |-BASIC_ORDER.
      2. |- (SO1): strict in Transitive(Set) & Asymmetric(Set).
      3. |- (SO2): relation= strict | Id(Set).
      4. (SO1, SO2)|- (SO3): relation in Transitive(Set) & Reflexive(Set) & Antisymmetric(Set),
      5. (SO3)|- (SO4): ORDER.

    8. Note that by asserting that we can derive ORDER (SO4) we have claimed we can derive all of the axioms in ORDER and so all the definitions, declarations, and theorems are also automatically a part of STRICT_ORDER.

    9. Strict_order::=the set of tpls satisfying STRICT_ORDER.
    10. Strict_order::=$ STRICT_ORDER.
    11. strict_order::=The sets which have < as a strict order
    12. strict_order::=Strict_order(strict=>(<)).Set.
    13. For X, strict_order(X)::=Strict_order(X).Set.

      Any set with an empty relation is a trivial order. A singleton set {x} has a strict order relation{}. A set{a,b} with two sets is ordered by {(a,b)} or by {(b,a)} but not by {(a,b), (b,a)}.

      Fishburn in 197? demonstrated that if one starts with a strict order (as defined above STRICT_ORDER) and uses it to define a relation and then takes that relation and the rules of ORDER to generate another strict relation then one gets the original relation back again.

      Quasi Ordered Sets

      Source: Birkhoff & Bartee 70, pp258-259. (math_11_STANDARD) |-For X:Sets, Quasi_orders(X) ::= Reflexivity(X) & Transitive(X).

      Example Quasiorders

    14. (number theory)|-divides in Quasi_order(Int).
    15. (monoids)|-For all Abelian_Monoid M, divides:=rel[a,b:M](for some x(a x = b)), divides in Quasi_order(M).

      The following shows that every quasi_order has an associated partial order defined between sets of relatively unordered elements.

    16. QUOSET::=
      1. relation::Quasi_orders(X).
      2. qr::=relation. -- shorthand

      3. equivalent::= qr & /qr.
      4. (def)|-(QO1); equivalent in Equivalence_relations(Set).
      5. Equivalence_classes::=Set/equivalent.
      6. (def)|- (QO2): For all E,F:Equivalence_classes, for all x:E, y:F(x qr y) or for no x:E,y:F(x qr y).
      7. relation::@(Equivalence_clases, Equivalence_classes)=for some x:(1st), y:(2nd) ( x relation y).
      8. (def)|- (QO3): For all E,F:Equivalence_classes, E relation F iff for all x:E, y:F(x qr y).

      9. (def)|- (QO4): relation in Partial_orders(Equivalence_classes).


    17. (QUOSET)|-For all QUOSET, ORDER (Set=>Equivalence_classes, relation=>relation.@(Equivalence_classes,Equivalence_classes) ).


      Poset stands for a partially ordered set.

    18. (ORDER)|- (simple_duality): For all variables(ORDER), if ORDER then ORDER (relation=>inverse, inverse=>relation, strict=>strict_inverse, strict_inverse=>inverse).

    19. POSET::=ORDER.
    20. Poset::= $ POSET.
    21. poset::= $ POSET.Set.
    22. For X, poset(X)::= $ POSET(Set=>X).Set.
    23. standard_order::= $ ORDER(relation=>(<=), inverse=>(>=), strict=>(<), strict_inverse=>(>) ).Set,

    24. poset(<=)::=standard_order,
    25. poset(<)::=standard_order.

      All posets define a digraph:

    26. For ORDER, graph::= the DIGRAPH(nodes=>Set, arcs=>strict),
    27. (above)|- (acyclic_graph): no cycles(graph).

    28. For ORDER, Haase_digraph::=the DIGRAPH(nodes=>Set, arcs=>strict~(|[n:2..] (strict^n) ) ). In words, arcs that are already implied by transitivity are not shown in the Haase graph.

      Example Posets.

    29. (numbers)|- (Ex1): Integer and Real in standard_order and Net{not finite, total}.
    30. (char)|- (Ex2): Char in standard_order and Net{finite, total}.
    31. (numbers)|- (Ex3): Nat, Nat0 in standard_order with Left_limited(<) & not finite & total.

    32. (sets)|- (Ex4): For S:Sets, ORDER(Set=>S, relation=>(==>), strict=>(=>>)).

    33. Kuratowski(3,3)::=following,
        [picture of set described below] Based on Kuratowski's 3,3 complete graph.
      1. |- (K1): Set={a,b,c,d,e,f},
      2. (<)={a,b,c}><{d,e,f}
      3. ()|-ORDER.
      4. ...more below

      (End of Net)

    34. (above)|-Kuratowski(3,3) in standard_order and Net{finite, not total}.

      Interval Notation

    35. INTERVALS::=

      1. |- (I0): ORDER. The [x,y] and (x,y) notation of the calculus and analysis is ambiguous.

      2. For x,y:Set, x..y::@Set= {z:Set || x relation z relation y},

      3. For x,y:Set, (x..y) ::@Set= {z:Set || x strict z strict y},

      4. For x,y:Set, [x..y) ::@Set= {z:Set || x relation z strict y},

      5. For x,y:Set, (x..y] ::@Set= {z:Set || x strict z relation y}.

        x..y is called a closed interval, and (x..y) is called an open one. The other two kinds of interval are called half open intervals. See topology for generalisations to open and closed subsets of other types [ math_91_Topology.html ]

        Notice that this notation may be confusing because when f:Set->T, f(x..y) <> f((x..y)).

        The following two definitions are inpired by the Unified Modeling Language.

      6. For x:Set, x..*::@Set= {z:Set || x relation z },
      7. For y:Set, *..y::@Set= {z:Set || z relation y},
      8. (above)|-x..y = x..* & *..y.



      An every day problem is sorting out our priorities. It is usually easy to compare a pair of options and see which one we prefer. With half-a-dozen options it is not so easy. One empirirical technique is to tabulate all pairs and for each pair note your preferred item. You can than count the number of times each item is preferred and get a series of numbers indicating a rough priority. Ranking is a theoretical version of this process. It is about attaching numbers to elements in a partially ordered set so that the numbers reflect the ordering of the elements in the partially ordered set. This is also called topological sorting.

      If these numbers are the heights of the nodes in a plot of the graph then we say that it is a Haase diagram of the poset.

      Define a standard ranking as a map from each element in the Set to a real number between 1 and |Set| inclusive which preserves the ordering:

    36. For ORDER, Rank(Set)::= (Set,<)>->([1..|Set|], <).

      Notice that if r:Rank(Set) then we can not reason from r(x)>r(y) that x>y. We can show that not(x<y) but a partial ordering may omit certain pairs that have ordered ranks.

      Here are three rankings that are simple to calculate -- with time O(|Set|^2). For example

    37. N:=|Set|.
    38. above::Set>->[1..N] = map[x](1 + |x.< | ), 1+the number of items above x.
    39. below::Set>->[1..N] = map[x](N - |x.> | ), N-the number items below x.
    40. rank::= (above+below)/2. are all rankings. Proofs are left as an exercise (Hint: if x'>x then x' and x'.< are in x.<).

      There is a simple way to calculate the values of |x.> | and | x.< | by hand on a small number of items. Prepare a grid with every pair of items and write in the larger of each pair in the squares in the grid. Count the squares where an item appears in its own row, and where other items occur. These are the two numbers. In practice the complete grid is symmetric and so half is ommitted. The counting goes along a row to the diagonal and then down. Here is an example:
      | x.> |6102210
      | x.< |0121134

      (Close Table)

      Knuth[Knuth 69] gives algorithms for topological sorting.

      Van Neuman and Morgenstern take this theory a lot further in their "General Theory of Games and Economics". They show that if the set has a linear order and an operation that constructs new elements as combinations (lotteries) of elements, then there is a unique natural ranking that indicates (up to scale) how much different elements are worth.

      Optimal values

      2. MAXMIN::=MINMAX.
      3. MINMAX::=
          Problem - to give meaning to such words as biggest, best, largest, worst, etc - in the general case, if at all possible. This turns out to be subtler than it looks. There is no common terminology - what will be defined as 'min' below may be called 'least' in some texts and papers and vice versa. So I define several models of these words.

        1. |-ORDER.

          Least(greatest) elements in a set have no lesser(greater) elements in the set,

        2. For S:@Set ~{{}},
        3. least(S)::@Set= {x:S || for all s:S, if s relation x then s=x},
        4. greatest(S)::@Set= {x:S || for all s:S, if s inverse x then s=x}.
        5. (def)|- (OP1): least(S)={x || for no y:S (y strict x)}.
        6. (def)|- (OP2): greatest(S)={x || for no y:S (y strict_inverse x)}.

        7. (def)|- (OP3): if finite S then some least(S) and some greatest(S).

          [ math_11_STANDARD.html ]

        8. (def)|- (OP4): if relation in Left_limited(S) then some least(S).
        9. (def)|- (OP5): if relation in Right_limited(S) then some greatest(S).
        10. (def)|- (OP6): if relation in Trichotometic(S) then 0..1 least(S) and 0..1 greatest(S).

          Minimal elements in a set are less than or equal to all members of that set.

        11. For S:@Set~{{}},
        12. minima(S)::@Set= {x:S || for all s:S(x relation s)},
        13. min(S)::= minima(S),
        14. maxima(S)::@Set= {x:S || for all s:S(x inverse s)},
        15. max(S)::= maxima(S),
        16. In all posets, the minima(maxima) are among the least (greatest) and if there exist any minima(maxima) then there can only be one of them.
        17. (above)|- (OP7): for all S:Set, min S ==> least S ==>S.
        18. (above)|- (OP8): 0..1 min S.
        19. (above)|- (OP9): max S ==> greatest S==>S.
        20. (above)|- (OP10): 0..1 max S.

          Most authors fail to distinguish maxima from greatest and least from minima probably because in they are the same when we talk about numbers and other total orders.

        21. (above)|- (OP11): if total then least=min and max=greatest and for all S:Finite_sets(Set)(one min(S) and one max(S)).

          This is not so in a general partially ordered set:

        22. Kuratowski(3,3)::=
          1. K1 ...from above [picture of set described below]
          2. (K2):
          3. (above)|-least(Set)={a,b,c},
          4. (above)|-greatest={d,e,f},
          5. (above)|-min(Set)=max(set)={}.

          6. ...more to follow K3

        23. Therefore there exist finite posets with any number of least/greatest elements and no maxima/minima.

          Many infinite sets have no least(greatest) elements. As an example Nat has no greatest elements and so no maxima. Also the reciprocals of the natural no-zero numbers:

        24. Reciprocals::=1/Nat ={1/n ||n:Nat} has no least elements and so no minima. Notice that the ordering relation on Nat and Reciprocals are linear orders. Thus there may be no least/minima/greatest/maxima for some subsets of linearly ordered sets.

          However Reciprocals is bounded below by 0. Further for any number x>0 there is some y such that 1/y is less than x - so that 0 is the greatest number that is below all the reciprocals. Thus 0 is the greatest lower bound on Reciprocals. To formailize these ideas we start with the ideas of upper and lower bounds. MATHS.MINMAX defines both strict and unstrict versions. The unstrict ones are common in mathematical texts and the strict versions less common.

          Now (strict) lower (upper) bounds are elements (strictly) less(greater) than all members of the set.

        25. For S:@Set,
        26. lb(S)::@Set= {x:Set || for all s:S(x relation s)},
        27. ub(S)::@Set= {x:Set || for all s:S(x inverse s)},
        28. slb(S)::@Set= {x:Set || for all s:S(x strict s)},
        29. sub(S)::@Set= {x:Set || for all s:S(x strict_inverse s)},

        30. (above)|- (OP12): lb({})=ub({})=slb({})=sub({})=Set.
        31. (above)|- (OP13): for all x:sub(S)|slb(S) (not x in S).

        32. (above)|- (OP14): for all s:sub(S), u:ub(S), g:greatest(S), m:max(S), (g and m relation u and g and m strict s).

        33. (above)|- (OP15): For S, not least(sub(S))==>S and not greatest(slb(S))==>S.

        34. For S,
        35. lsub(S)::@Set= least(sub(S))),
        36. gslb(S)::@Set= greatest(slb(S))).
        37. For S, lub(S)::@Set= least(ub(S))),
        38. glb(S)::= greatest(lb(S))). Note lsub and gslb are rare in mathematics. Another approach is to start with a definition of lub and/or glb and work back to the order from there. See [ SEMILATTICE in math_32_Semigroups ] and [ LATTICE in math_41_Two_Operators ]
        39. for this approach.

          Example Kuratowski Part 3

        40. Kuratowski(3,3)::=
            from (K2)...continued [picture of set described below]
          1. (above)|-sub{a,b,e}={d,e,f},
          2. (above)|-lsub{a,b}=least{d,f}={d,f},
          3. (above)|-ub{a,b,e}={a,b,d,e,f},
          4. (above)|-lub{a,b}=least{a,b,d,e,f}={a,b}.
          5. Therefore there exist finite posets with as many of lub's and glb's as we might want.
          6. (above)|-least{a,b,e}={a,b}=lub{a,b,e}


          Most authors consider glb and the supremum to be the same, and similarly for lub and the infimum. I now define both strict and non-strict forms - as found in different texts.

          Source: After Godement 69, Algebra, Herman, Paris, France. 5,2, pp91

        41. For S:@Set~{{}},
        42. sup(S)::=supremum(S),
        43. supremum(S)::@Set= the(i:ub(S) || for all b:ub(S)(b inverse i)),
        44. inf(S)::=infimum(S),
        45. infimum(S)::@Set= the(s:lb(S) || for all b:lb(S)(b relation s)),
        46. (above)|- (OP16): (inf = lub) and (sup=glb). Godement claims that for all sets of cardinal numbers the inf and sup exist, and are unique - by allowing positive and negative infinite numbers.

          Source: After General Topology, Springer Verlag 1984, para 7.1.1

        47. For S:@Set~{{}},
        48. sinf(S)::=strict_infimum(S),
        49. strict_infimum(S)::@Set= the(i:Set || for all x:S(i relation x) and for all b, if b strict_inverse i then for some x:S(b inverse x)),
        50. ssup(S)::=strict_suprememum(S),
        51. strict_supremum(S)::@Set= the(s:Set || for all x:S(x relation s) and for all b, if b strict s then for some x:S(b strict_inverse x)),
        52. (above)|- (OP17): inf(S) and sup(S) in S

          Optimizing a function or map

        53. For X:Sets~{{}}, f:X->Set, opt:{min,max,glb,lub,inf,sup,...}.
        54. opt functions are used for picking desirable items:

          Example of Software Transaction specification Part 1

        55. Pick_inexpensive:=Objects_available.cost.min./cost.
        56. Not that opt is not in @(S,S) so cost;opt;/cost is not well formed.

        57. For X:Sets~{{}}, f:X->Set, opt:{min,max,glb,lub,inf,sup,...}, (opt mod f)(X) ::= /f(opt(f(X))).
        58. (above)|- (OP18): X. (opt mod f)=/f(opt(f(X))).

          Example of Software Transaction specification Part 2

        59. Pick_inexpensive=Objects_available.(min mod cost).

          Don't try to Optimize Two or more Objectives.

        60. For X:Sets, |X|>=2, opt:{min,max,glb,lub,inf,sup}, if |Set|>2 then
        61. for some f,g:X->Set, no ((opt mod f)(X) & (opt mod g)(X)).

          Example of Multiple Optimization

          It is difficult to find something that is both cheapest and best.
        62. Pick_perfect=Objects_available.(min mod money) & Objects_available.(max mod quality).


            .Road_Works_ahead There is often a kind of duality between two different attributes or criteria however. Maximizing one with the other fixed gives a function that when minimized is the less than maximizing the function of minimum with respect to the other variable with the first variable fixed.
              Was that confusing enough? I've been trying to work out a clear and correct model of this kind of duality for 16 years.

            This section follows studying A. M. Fink and Juan A. Galiter's 1992 paper in the American Mathematical Monthly (Vol65, No. 3, June 1992) entitled "For every Answer There are Two Questions".

            In some circumstances a pair of functions generate dual optimization problems.

          1. DUALITY_BASIS::=following,
            1. X:Set. f, g:: X>->Real & Positive.

            (End of Net)

            Example of one solution solving two problems


            1. |-DUALITY_BASIS( X=> Rectangle, f=> perimeter, g=> area).

            2. (primal_problem): Given a perimeter p, which rectangle has maximum area.
            3. For p:Real & Positive, M(p)::=(max mod area)(/perimeter(p)).
            4. (dual_problem): Given an area a, which rectangle has minimum perimeter.
            5. For a:Real & Positive, m(a)::=(min mod perimeter)(/area(a)).

            6. In this case the solutions to both problems are always squares.
            7. (Rectangle)|-Square = Rectangle( length=breadth ).

            8. (above)|-img M = img m = Square.

            9. For p, M'(p) = area(M(p)),
            10. For a, m'(a)::=perimeter(m(a)).

            11. More, solving one problem discovers a solution of the other problem.
            12. (above)|-For all p, m'(M'(p)) = p,
            13. (above)|-For all a, M'(m'(a)) =a.

              more TBA.

            (End of Net)

          2. DUALITY::=following,

            1. |-DUALITY_BASIS.
            2. For x: Real & Positive, M(x)::=(max mod f)(/g(x)).
            3. For x: Real & Positive, m(x)::=(min mod g)(/f(x)).
            4. fM::=f o M,
            5. gm::=g o m.

            6. |- (FinkGalliter1): img M = img m.
            7. Y::= img M.

              Here is my best guess (so far) of the conditions needed to guarantee duality.

            8. |- (FinkGalliter2): for all y1,y2 ( f(y1) < f(y2) iff g(y1) < g(y2) ).
            9. |- (FinkGalliter3): f|Y and g|Y in X---Real & Positive. Note: f and y are not one-one and onto in general, but they are on Y.

            10. (above)|- (duality): gm o fM = Id = fM o gm.

            (End of Net)

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

          Arrow's Theorem

          Political life is rife with setting prioritites an attempting to reconcile different people's preferences. We model these situations as a set of alternatives and a set of orders (or rankings). The question then arises if there is an algorithm that (in some way or other) ballances the multiple preferences. Unfortunately there is a depressing theorem that shows that any such algorithm, given enough options and preferences will have non-democratic, or even insane properties. For example the algorithm will allow one person to be a dictator, or it might mean that when someone reverses their preferences then the algorithm will go in the opposite direction....

          Open-ended Exercise on Bentham's Definition

          When is the greatest good for the greatest number meaningful?


        63. X.(opt mod f).(opt mod g) is often well defined, but not necesarily the same as
        64. X.(opt mod g).(opt mod f)


        Conclusion re Optimal values in General Posets

        In a general poset none of the optima have to exist. Since we often need optima to exist we define and study special subsets and special posets where we can show that a particular class of optima do exist.

        Complete Posets

      4. COMPLETE::=

        1. |-MINMAX.
        2. (complete): For all S:@Set ~{{}}, one lub(S).

          Source: Manes & Arbib 86

      5. complete_partially_ordered_sets::=$ COMPLETE.Set,
      6. cpo::=complete_partially_ordered_sets.
      7. For X, cpo(X)::=$ COMPLETE(X).Set. In a complete partially ordered set every subset has a unique least upper bound.

        Special Subsets and Functions in Posets

      8. convergent::@Seq(S)={s || some lub(s)}.
      9. (above)|-For s:convergent, one lub(s). for s:convergent, lim(s) ::=the lub(s).

        Consider any map from an poset to itself then some points wil increase when the map is applied and some will decreas and some will not change.
        (fixed_points): [ UNARY in math_11_STANDARD ]

      10. For f:Set->Set,
      11. increasing_points(f)::={h:Set || h<=f(h)},
      12. decreasing_points(f)::={h:Set || h<=f(h) }.
      13. (above)|-fixed_points(f) = increasing_points(f) & decreasing_points(f).

      14. increasing_functions::={f:Set->Set || for all x( x <= f(x))},
      15. increasing::=increasing_functions.

      16. (above)|- (PO1): increasing={f:Set->Set || (=) in (Set,f)->(Set,<=)}
      17. monotone_functions::={f:Set->Set || for all x,y( if x<=y then f(x)<=f(y) )},
      18. monotonic::=monotone_functions.
      19. (above)|- (PO2): monotonic = (<=)(Set->Set).
      20. continuous::@monotonic={f || for all s:convergent ( lim(f(s))=f(lim(s)) ). Compare Math.Topology.CONTINUITY.

      21. ascending_chains::@Seq(Set)={ s || <=(s) },
      22. ascending::=ascending_chains.
      23. strict_ascending_chains::@Seq(Set)={ s || <(s) },
      24. strict_ascending::=strict_ascending_chains,
      25. (above)|- (PO3): for all a:ascending, some I:@Nat0( (<=)I->Set).
      26. (above) |- finite_sequence::= { s:Seq(Set)|| pre(s) in Finite_sets(Set)}. [ Finite Sequences in logic_6_Numbers..Strings ]

      27. chain::@@Set={ A:@Set || for all x,y:A ( x <= y or y<=x ) }.
      28. (above)|- (PO4): for all a:ascending( img(a) in chain ).
      29. (above)|- (PO5): for all f:Set->Set, f in increasing iff map[i]f^i in ascending.

      30. descending_chains::@Seq(Set)={ s || >=(s) },
      31. descending::=descending_chains,
      32. strict_descending_chains::@Seq(Set)={ s || >(s) },
      33. strict_descending::=strict_descending_chains,

      34. directed::@@Set={P:@Set || for all u:Finite_sets(P), some ub(P)&P}.

      35. CHAIN_COMPLETE::=

        1. |-MINMAX.
        2. For all S:chain, some lub(S).

          Source: Nielson & Nielson 92

        3. Scott_open_sets::={U:@Set|| (for all x:U, y:Set, if x <= y then y in U) and (for all M:@Set, if lub(M) in U and M in directed then M&U<>{})}.

        4. Scott_topology::=OPEN_TOPOLOGY(Space=>Set, Open=>Scott_open_sets).

      36. chain_complete_partially_ordered_sets::=$ CHAIN_COMPLETE.Set,
      37. ccpo::=chain_complete_partially_ordered_sets,
      38. For X, ccpo(X)::=$ CHAIN_COMPLETE(X).Set.

        Some use the term complete for chain complete.

        Source: Gunter 92.

        Another variation of completeness is what I term Kleene Completeness, where every ascending sequence has a least upper bound. [ DOMAIN in math_24_Domains ]

      39. TARSKI_KNASTER::=

        1. |-COMPLETE.

          Source: Tarski 55, A. TARSKI "A Lattice Theoretical fixedpoint theorem and its applications," Pacific Journal of Maths, V5, 1955, pp285-309

          Tarski published the general version. The special case for (@X, ==>) by B. Knaster (1928) is often sufficient - hence the literature calls this the Knaster-Tarski Fixed Point theorem.

        2. |-MINMAX.
        3. f::monotonic,
        4. H::=increasing_points(f).
        5. L::=decreasing_points(f).

          ??|-if some lub H then the lub H = the greatest fixed_points(f).

          ??|-if some glb L then the glb L = the least fixed_points(f),


      40. Countable_complete::=$ Net{Use MINMAX. for all S:countable, one lub(S)}.

      41. For all X:Sets, (@X,==>) in cpo and (the lub) = (|) and Seq(S)=convergent and for all f:X->X( f and /f in (continuous)@X->@X).

        ??{ For (S,<=):poset, S:@Set~{{}}, dominant(S):@S::={D:@S || for all y:S~D(y<=x)} }?

        ??{ For F:@@@Set, S.complete::@=for all S:F( one lub(S) ) }?


      Semi-orders are used for several urposes including the modelling of before/after relationships between events in time.
    41. SEMIORDER::=

        Source: Luce 56, Library of Congress call number BF39.C66 and CACM, Feb 1978.

      1. Set::Sets,
      2. P::@(S,S)= previous_to.
      3. |- (SO1): For all x,y,z,w:S, if x P y P z then x P w or w P z,
      4. |- (SO2): For all x,y,z,w, if x P y and z P w then x P w or z P y,
      5. |- (SO3): for no x(x P x).

      6. (above)|- (SO4): for some f:Real^Set, δ:Real ~ Negative, for all x,y( f(x) > f(y)+δ iff x P y).

      7. For x,y:S, x concurrent y::= not (x P y) and not (y P x).


      Parts and Whole

      .Used_in math_93_Graphics, monograph/02MATHS&TEMPO#Lift, monograph/03_Languages#Outlines, ...

      Compare work done by the elder Woodger on the axiomatisation of biology [Woodger 32].

      Conference: [ IMC.htm ]

      Applicable to: OOP ,data structures, programs, texts, documentation, ...

    42. PART_WHOLE::=
      1. objects::Sets, -- the things that are wholes and/or parts
      2. isin::strict_order(objects).
      3. APO::=isin.
      4. |- (PW0): MINMAX(Set=>objects, strict=>isin,...)

      5. universe::objects. -- the largest object
      6. |- (PW1): lub(objects)={universe}.

      7. Example1::=
        1. objects::={auto,engine,radiator,radiator_cap,wheel1,wheel2,....}
        2. isin::={(engine,auto),(radiator,engine),(radiator,auto),..}
        3. universe::=auto.

        4. (above)|-engine isin auto.
        5. (above)|-radiator isin engine.


      8. (above)|- (PW2): finite iff finite objects.

      9. parts::=/isin, -- the parts of x are those things "isin x".
      10. (above)|- (PW3): For x:objects, parts(x)= {y:objects || y isin x}.
      11. (above)|- (PW4): For no x (x in parts(x)).
      12. (above)|- (PW5): for all x (x in parts(universe)).

      13. elements::={x || no parts(x)},
      14. compounds::=objects~elements,
      15. (above)|- (PW6): objects>=={compounds, elements}.

        In many cases each object is assembled out of components, and each component is itself likely to be assembled from smaller components, and a part is a component or any part of a component...

      16. is_component_of::=isin~(|[i:2..]isin^i),
      17. components::=map[x:objects]/is_component_of(x).
      18. (above)|- (PW7): |[i:2..]isin^i = isin^2,
      19. (above)|- (PW8): For x:objects, parts(x)>=={components(x), parts(components(x)

      Proof of PW7

      Consider{ |[i:2..]isin^i =isin;do(isin)=isin^2}.

      Proof of PW8

      Consider { parts(x)>=={components(x), /isin^2(x)}...

    Example of a continuum

    In some cases there are no components. For example:
  1. Example2::=
    1. objects={(0..r]| r:(0..)},
    2. for all r1,r2:objects, (0..r1] isin (0,r2] iff r1<r2.
    3. (above)|-[0,r1] is_component_of [0..r2] iff r1<r2 and for no r3(r1<r3<r2).
    4. But,
    5. (above)|-for all r1, r2, if r1<r2 then r1<(r1+r2)/2<r2
    6. (above)|-for no x:objects, some components(x).


  2. discrete::@= for all x:compounds(some components(x)).

  3. (above)|- (PW9): if finite then discrete.

    Proof of PW9

  4. Let{
  5. |- (0): not discrete,
  6. (0)|- (1): for some x:compounds, no components(x)
  7. (1)|- (2): some parts(x0),
  8. (1)|- (3): parts(x0)==>parts^2(x0),
  9. ()|- (4): for y:parts(x0), some y' (y isin y' in parts(x0)), () |-(5): R:@(parts(x0),parts(x0)) ::={y,y'||y isin y' parts(x0)},
  10. ()|- (6): R==>(<>),
  11. ()|- (7): R in (any)-(some),
  12. (choice)|- (8): some f:(any)-(1)(f==>R),
  13. ()|- (9): map[i](x0.f^i): Nat-->parts(x),
  14. ()|- (10): not finite.

    Proof of 4

  15. Let{
  16. |- (4.1): y in parts(x0),
  17. (3)|- (4.2): y in parts^2(x0),
  18. (4.2)|- (4.3): y in parts(x2) and x2 in parts(x0),
  19. (4.3)|- (4.4): y <> y' in parts(x0)
  20. }
  21. }
  22. choice::=See [ Choice in logic_5_Maps ]

  23. For x, components(x) = greatest(slb{x}).

  24. For x,y:Things, common(x,y)::= slb{x,y}.

  25. For x,y, interface(x,y)::= gslb{x,y},

  26. (def)|- (PW9): For x,y, interface(x,y)= {z:objects||z in common(x,y) and for no w:objects~{z} (z isin w in common(x,y) ) }
  27. (def)|- (PW10): For x,y, interface(x,y)=glb{x,y}.

  28. TAGGING::=
      Tagging is a process of assigning a string to every part so that we can (1) identify each part, and (2) encode the structure of the objects.

    1. labels::Sets,
    2. tags::#labels. The notation for strings of symbols (#, !, ...) is in [ logic_6_Numbers..Strings.html ] and [ math_62_Strings.html ]

    3. Dewey_decimal::@.
    4. Dewey_decimal iff labels=Nat.
    5. Knuth has an excellent discussion of "Dewey Decimal Notation".

    6. tag::objects-->tags,
    7. universe.tag=().
    8. For all x,y:objects, some t:tags ( y.tag = (x.tag!t) iff y isin x).
    9. For all x,y:objects, (if y in components x then for one l:labels( x.tag = (y.tag!l) )).


  29. hierarchy::@ for all x,y (no common(x,y)).
  30. tree::@= discrete and hierarchy.
  31. branches(x)::=|[I:@Nat]{B:I-->objects||components(objects) and B[1]=x).
  32. infinite_branches(x)::={B:branches||not finite cor(B) ).
  33. expansion::Nat0=fun[x]Card(components(x)).

  34. A Version of Konig's Infinity Lemma [Knuth 69,Vol 1, Theorem K.]
  35. (above)|- (Konig1): if not finite and tree and for all x( finite components(x)) then for some infinite_branches(universe).

    Proof of Konig1

  36. Let{
  37. |- (Konig0): not finite,
  38. |- (Konig1): tree,
  39. |- (Konig2): for all x(not finite components(x)).

  40. (above)|- (Konig3): for all x:objects, if not finite parts(x) then for some y:components(x)(not finite parts(y))
  41. B1:=universe,
  42. (above)|- (Konig4): not finite parts(B1),
  43. (above)|- (Konig5): some y:components(B1)(not finite y ),
  44. (above)|- (Konig6): B2 in components(B1) and not finite parts(B2),
  45. ...

    Proof of Konig3

  46. Let{
  47. |- (Konig3a): x:objects,
  48. |- (Konig3b): not_finite parts(x),
  49. |- (Konig3c): all y:components(y)( not finite parts(x)).
  50. (above)|- (Konig3d): not finite components(x),
  51. (above)|- (Konig3e): parts(x)>=={parts(y)||y:components(x)} and finite parts(components(x).
  52. (above)|- (Konig3f): Card(parts(x))=+[y:components(x)]Card(parts(y))<>infinity
  53. (above)|- (Konig3g): finite parts(x).
  54. }
  55. }


  • Part_whole::=$ PART_WHOLE.


    1. |-PART_WHOLE
    2. |- (FPW0): finite.
    3. (above)|- (FPW1): one N:Nat, all x(expansion(x)<=N).

    4. N::=the N:Nat, all x(expansion(x)<=N) [click here [socket symbol] if you can fill this hole]
    5. (above)|- (FPW2): for all x, some l:components(x)-->1..N
    6. (above)|- (FPW3): for some D:Nat, t:1..D->1..N, (TAGGING(labels=>1..N, tags=>1..D->1..N, tag=>t))

      Proof of FPW1

      Consider{N::=lub expansion(objects)}.



  • IS_A::=
      for describing generaliaztion, subtyping, subclasses, inheritance, exported...
    1. objects::Sets,
    2. isa::strict_order(objects).
    3. AKO::isa.
    4. |-MINMAX(Set=>objects, strict=>isa,...)
    5. universe::objects.
    6. |- (isa1): lub(objects)={universe}.
    7. super::@(objects,objects).
    8. |- (isa2): isin =super;do(super).
    9. |- (isa3): sub=/super.
    10. For A:Sets, p:objects->A, inheritted(p)::@=for all objects x,y(if x isa y then p(x)=p(y)).
    11. For A, p, exported(p)::@=for all objects x,y(if y isa x then p(x)=p(y)).


    Specially Ordered Sets

      Totally Ordered Sets

    1. TOSET::=ORDER and Net{total}.
    2. totally_ordered_set::=Toset.
    3. Toset::= Totally Ordered Sets
    4. Toset::= $ TOSET,
    5. For X, toset(X)::=Toset(X).Set,
    6. toset::=Toset.Set.

      Totally ordered sets are also known as linearly ordered sets:

    7. Linearly_ordered_sets::=loset.
    8. loset::=toset.
    9. Loset::=Toset.

      Well Ordered Sets

    10. WOSET::=
      1. A partially ordered set where every subset has one least element.
      2. ORDER.
      3. |- (WO0): for all S:@Set~{{}} (one least(S)).
      4. bottom::=the least(Set),
      5. ::=bottom.
      6. |-|-(WO_induction): invariants(strict) & (in(⊥))={Set}.

    11. well_ordered_set::=woset.
    12. Woset::=$ WOSET, Well ordered sets.
    13. For X, woset(X)::=Woset(X).Set,
    14. woset::=Woset.Set.

      (Nat, <=) in $ WOSET.

      Knuth has a different definition

      Source: Knuth 69, 1.2.1.Ex15.

    15. KWOSET::=
        Knuth's Well Ordered Set.
      1. S::Set, (<) ::Transitive(S) and Trichotomettic(S). (<=) ::=(<|=), (>) ::=(/<), (>=) ::=(/<=).
      2. |- (KWO0): For all A:@S~{{}}, some min(A).
      3. (above)|- (KWO1): For all A, one min(A).
      4. (above)|- (KWO2): (<) in Left_limited(S). [Knuth 69, 1.2.1.Ex15.f]. [ Kinds of relations in math_11_STANDARD ]
      5. (above)|- (KWO3): no s:Nat->S(>(s)).

      6. (above)|- (Induction principle): for P:@S(if for all x(if for all y(if y<x then y in P) then x in P) then P=S.

        Source: Knuth 69, 1.2.1.Ex15.g.

        Compare [ NOETHERIAN_INDUCTION ]


      Well-Founded Sets

        Not to be confused with a well ordered set(WOSET above)!
      1. A well_founded set is a partially ordered set where the relation is left_limited. This means that any sequence:
      2. ...x3<x2<x1<x0 has to be finite. In otherwards there are no infinite descending chains.
      3. |- (WF0): ORDER(S, <=,<,>,>=).
      4. |- (WF1): (<) in Left_limited(S). [ Kinds of relations in math_11_STANDARD ]
      5. Minimal::=Set of elements greater than nothing else:@S,
      6. Minimal::= {x:S || for all y:S(not y < x)}.


        Emmy Noether's discovery - The Strongest Induction Principle Known to Humanity.

      1. WELL_FOUNDED_SET(S=>X).
      2. |-|-(Noether1): For P:X^@, if for all x:Minimal( P(x) ) and for all x:X~ Minimal (if for all z:X(if z<x then P(z)) then P(x)) then for all x:X(P(x).


      3. |-|-(Noether2): For P:@X, if Minimal ==> P and for all x:X~Minimal (if \<(x)==>P then x in P) then P=X.



    18. lattice_order::= $ MINMAX and Net{for all F:Finite_sets(Set), one lub(F) and one glb(F)}.
    19. complete_lattice_order::= $ MINMAX and Net{for all F:@(Set), one lub(F) and one glb(F)}.

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

    See Also

    See [ math_24_Domains.html ] and [ LATTICE in math_41_Two_Operators ] for further developments in the theory of orders.

    . . . . . . . . . ( end of section Orders) <<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.