.Open Orders
. Basis
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:
.Table Set of Elements	Relationships that impose an order
.Row Plans	cheaper, easier, more fun, ...
.Row Products	safer, cheaper, faster, bigger, smaller, better, worse,...
.Row Events	Occurs before, more likely than,...
.Row Numbers	Less than, greater then, less then or equal, greater then equal
.Row Natural Numbers	divides
.Row Points in space	above, below, to the right, to the left, before, behind
.Row Components in a system	is a part of (APO), part_whole, composition
.Row Types of Objects	is a kind of (AKO), inheritance, derived_from, subtype_supertype
.Row Parts of a program	depends on
.Row Subsets of a set	==>(subset of)
.Row Sets	functional dependency(there exists a many-one mapping from _ to _)
.Row Sets	existence dependency(for each _ there must exist a unique fixed _)
.Row Letters	Earlier in the alphabet
.Row Words	dictionary order (lexographic order)	
.Row Boolean Values	implies
.Row {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:
.Table Set of Elements	Relationships
.Row Pieces of a program	coupling
.Row Points in space	close to, surrounding
.Row Numbers	Having 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.  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).
We would not want A part to depend B and B to depend on A, this 
would imply something that might not work well, rather like
trying to fly by pulling hard on one's boot laces.  This property
is an example of `antisymmetry` here.

The following definitions and theorem are to be found in
standard::=http://www/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)}.

(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.
BASIC_ORDER::=Net{
  Set::Sets, 
  relation::@($Set,$Set),
  strict_relation::@($Set,$Set),
  strict::=strict_relation,
  inverse::@($Set,$Set),
  strict_inverse::@($Set,$Set).
 |-(BO1): $inverse = /$relation.
 |-(BO2): $strict_inverse = /$strict_relation.
}=::BASIC_ORDER.
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.

ORDER::=Net{ 
	|- $BASIC_ORDER.
	|- (O0):  relation in Transitive($Set) & Reflexive($Set) & Antisymmetric($Set).
	|- (O1): strict_relation=relation~Id($Set),
(O0, def)|-(O2): strict in Transitive($Set) & Asymmetric($Set).
(O2, ITisAT)|-(O3): strict in Irreflexive($Set).

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

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

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

Exercise: Verify that |- $ORDER( Set=>Int, relation=>(<=), inverse=>(>=), strict=>(<), strict_inverse=>(>), not finite, total, ...).

STRICT_ORDER::=Net{ 
 |- $BASIC_ORDER.
 |- (SO1):  strict in Transitive($Set) & Asymmetric($Set).
 |- (SO2): relation= $strict | Id($Set).
(SO1, SO2) |- (SO3): relation in Transitive($Set) & Reflexive($Set) & Antisymmetric($Set),
(SO3) |- (SO4): $ORDER.
}=::STRICT_ORDER.
  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.

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

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
(number theory)|- divides in Quasi_order(Int).
(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.
QUOSET::=Net{
	$Set::Sets, 
	relation::Quasi_orders(X).  
	qr::=relation. -- shorthand

	equivalent::= $qr & /$qr.  
	(def)|-(QO1); equivalent in Equivalence_relations($Set).
	Equivalence_classes::=$Set/equivalent.
	(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).
	relation::@(Equivalence_clases, Equivalence_classes)=for some x:(1st), y:(2nd) ( x relation y).
	(def)|-(QO3): For all E,F:Equivalence_classes,  E relation F iff for all x:E, y:F(x $qr y).
	
	(def)|-(QO4): relation in  Partial_orders(Equivalence_classes).

}=::QUOSET.


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

. Posets
Poset stands for a partially ordered set.

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

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

poset(<=) ::=$standard_order,
poset(<) ::=$standard_order.

All posets define a digraph:
 For $ORDER, graph::= the DIGRAPH(nodes=>$Set, arcs=>strict),
()|-(acyclic_graph): no cycles(graph).

 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.
(numbers)|-(Ex1): Integer and Real in $standard_order and Net{not $finite, $total}.
(char)|-(Ex2): Char in $standard_order and Net{$finite, $total}.
(numbers)|-(Ex3): Nat, Nat0 in standard_order with Left_limited(<) & not $finite & $total.

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

Kuratowski(3,3) ::=following,
.Net
Based on Kuratowski's 3,3 complete graph.
|-(K1):	 $Set={a,b,c,d,e,f}, 
	(<)={a,b,c}><{d,e,f}
()	|- $ORDER.       
	...more below
.Close.Net
()|- Kuratowski(3,3) in standard_order and Net{finite, not total}.

. Interval Notation
INTERVALS::=Net{ 
	|-(I0): $ORDER.  
The [x,y] and (x,y) notation of the calculus and analysis is ambiguous. 


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

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

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

 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
.See http://www/dick/maths/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.

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

}=::INTERVALS.

. Ranking
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:
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
	N:=|Set|.
	above::Set>->[1..N] = map[x](1 + |x.< | ), 1+the number of items above x.
	below::Set>->[1..N] = map[x](N - |x.> | ), N-the number items below x.
	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:
.Table x	a	b	c	d	e	f	g
.Row a
.Row b	a	.
.Row c	a	b	.
.Row d	a	.	.	.
.Row e	a	.	.	.	.
.Row f	a	.	.	d	e	.
.Row g	a	.	.	d	e	f	.
.Row | x.> |	6	1	0	2	2	1	0
.Row | x.< |	0	1	2	1	1	3	4
.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 (loteries) of paris of elements, then their is
a unique natural ranking that indicates (up to scale) how much
different elements are worth.

.Open Optimal values

OPTIMIZATION::=$MINMAX,
MINMAX::=Net{
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 however - what will
be defined as 'min' below may be called 'least' in some texts and papers 
and vice versa.  I define several models of these words.

 |- $ORDER.

Least(greatest) elements in a set have no lesser(greater) elements in the set,
 For S:@$Set ~{{}},
	least(S) ::@$Set= {x:S || for all s:S, if s relation x then s=x},
	greatest(S) ::@$Set= {x:S || for all s:S, if s inverse x then s=x}.
	(def)|-(OP1): least(S)={x || for no y:S (y strict x)}.
	(def)|-(OP2): greatest(S)={x || for no y:S (y strict_inverse x)}.

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

.See http://www/dick/maths/math_11_STANDARD.html
(def)|-(OP4): if $relation in Left_limited(S) then some least(S).
(def)|-(OP5): if $relation in Right_limited(S) then some greatest(S).
(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.
 For S:@$Set~{{}},
        minima(S)::@$Set= {x:S || for all s:S(x relation s)},
        min(S) ::= minima(S),
        maxima(S)::@$Set= {x:S || for all s:S(x inverse  s)},
        max(S) ::= maxima(S),
	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.
 ()|-(OP7): for all S:$Set, min S ==> least S ==>S.
        ()|-(OP8): 0..1 min S.
        ()|-(OP9): max S ==> greatest S==>S.
        ()|-(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.
()|-(OP11): if $total then least=min and max=greatest and for all S:Finite($Set)(one min(S) and one max(S)).

This is not so in a general partially ordered set:
Kuratowski(3,3) ::=Net{ 
	(K1) ...from above (K2):.
	()|- least($Set)={a,b,c}, |- greatest={d,e,f},
	()|- min($Set)=max(set)={}.

	...more to follow
	}=::Kuratowski.
 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:
	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.
 For S:@$Set,
          lb(S) ::@$Set= {x:$Set || for all s:S(x relation s)},
          ub(S) ::@$Set= {x:$Set || for all s:S(x inverse s)},
         slb(S) ::@$Set= {x:$Set || for all s:S(x strict s)},
         sub(S) ::@$Set= {x:$Set || for all s:S(x strict_inverse s)},

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

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

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

 For S,  
        lsub(S) ::@$Set= least(sub(S))),
        gslb(S) ::@$Set= greatest(slb(S))).
 For S, lub(S) ::@$Set= least(ub(S))),
        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 
.See http://www/dick/maths/math_32_Semigroups.html#SEMILATTICE
and
.See http://www/dick/maths/math_41_Two_Operators.html#LATTICE
 for this approach.

. Example Kuratowski Part 3
Kuratowski(3,3) ::=Net{ 
from (K2)...continued
(K3):
	()|- sub{a,b,e}={d,e,f}, 
	()|- lsub{a,b}=least{d,f}={d,f}, 
	()|- ub{a,b,e}={a,b,d,e,f},
	()|- lub{a,b}=least{a,b,d,e,f}={a,b}.
	Therefore there exist `finite` posets with as many of lub's and glb's as we might want.
	()|- least{a,b,e}={a,b}=lub{a,b,e}
}=::Kuratowski.

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
 For S:@$Set~{{}},
        sup(S) ::=supremum(S)::@$Set= the(i:ub(S) || for all b:ub(S)(b inverse i)),
        inf(S) ::= infimum(S)::@$Set= the(s:lb(S) || for all b:lb(S)(b relation s)),
	()|-(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
 For S:@$Set~{{}},
        sinf(S) ::= 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)),
        ssup(S) ::= 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)),
	()|-(OP17): inf(S) and sup(S) in S

. Optimizing a function or map
 For X:Sets~{{}},  f:X->$Set, opt:{min,max,glb,lub,inf,sup,...}.
	`opt` functions are used for picking desirable items:
. Example of Software Transaction specification Part 1
	`Pick_inexpensive:=Objects_available.cost.min./cost`.
	Not that `opt` is not in @(S,S) so `cost;opt;/cost` is not well formed.

 For X:Sets~{{}}, f:X->$Set, opt:{min,max,glb,lub,inf,sup,...},
	(opt mod f)(X) ::= /f(opt(f(X))).
	()|-(OP18): X. (opt mod f)=/f(opt(f(X))).
. Example of Software Transaction specification Part 2
	`Pick_inexpensive=Objects_available.(min mod cost)`.

. Don't try to Optimize Two or more Objectives.
 For X:Sets, |X|>=2,  opt:{min,max,glb,lub,inf,sup}, if |$Set|>2 then
	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`.
	Pick_perfect=Objects_available.(min mod money) & Objects_available.(max mod quality).

.Open Duality
.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.
.Box
Was that confusing enough? I've been trying to work out a clear
and correct model of this kind of duality for 16 years.
.Close.Box

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.
DUALITY_BASIS::=following,
.Net
	X:$Set.
	f, g:: $X>->Real & Positive.
.Close.Net
. Example of one solution solving two problems
.Net
	|- $DUALITY_BASIS( X=> Rectangle,  f=> perimeter,  g=> area).

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

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

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

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

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

more $TBA.

.Close.Net
DUALITY::=following,
.Net
	|- $DUALITY_BASIS.
	For x: Real & Positive, M(x)::=(max mod f)(/g(x)).
	For x: Real & Positive, m(x)::=(min mod g)(/f(x)).
	fM::=f o M,
	gm::=g o m.

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

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

	|- (FinkGalliter2): for all y1,y2 ( f(y1) < f(y2) iff g(y1) < g(y2) ).
	|- (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.

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

.Close.Net

.Close Duality

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

However
	X.(opt mod f).(opt mod g)
is often well defined, but not necesarily the same as
	X.(opt mod g).(opt mod f)
}=::MINMAX.

. 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
COMPLETE::=Net{
|- $MINMAX. 
 (complete): For all S:@$Set ~{{}}, one lub(S).
.Source Manes & Arbib 86
}=::COMPLETE.
complete_partially_ordered_sets::=$ $COMPLETE.$Set,
cpo::=$complete_partially_ordered_sets.
 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
convergent::@Seq(S)={s || some $lub(s)}.
 ()|-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):
.See http://www/dick/maths/math_11_STANDARD.html#UNARY
 For f:$Set->$Set,
	increasing_points(f) ::={h:$Set || h<=f(h)}, 
	decreasing_points(f) ::={h:$Set || h<=f(h) }.
	()|- $fixed_points(f) = $increasing_points(f) & $decreasing_points(f).

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

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

ascending_chains::@Seq($Set)={ s || <=(s) },
ascending::=$ascending_chains.
strict_ascending_chains::@Seq($Set)={ s || <(s) },
strict_ascending::=$strict_ascending_chains,
()|-(PO3): for all a:$ascending, some I:@Nat0( (<=)I->$Set). 
()|-finite_sequence::= { s:Seq($Set)|| pre(s) in Finite_set}.
.See http://www/dick/maths/logic_6_Numbers..Strings.html#Finite Sequences

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

descending_chains::@Seq($Set)={ s || >=(s) },
descending::=$descending_chains,
strict_descending_chains::@Seq($Set)={ s || >(s) },
strict_descending::=$strict_descending_chains,

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

CHAIN_COMPLETE::=Net{
	|- $MINMAX. 
 For all S:$chain, some $lub(S).
.Source Nielson & Nielson 92


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

Scott_topology::=OPEN_TOPOLOGY(Space=>$Set, Open=>Scott_open_sets).
}=::CHAIN_COMPLETE.
chain_complete_partially_ordered_sets::=$ $CHAIN_COMPLETE.$Set,
ccpo::=$chain_complete_partially_ordered_sets,
 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.
.See http://www/dick/maths/math_24_Domains.html#DOMAIN

TARSKI_KNASTER::=Net{ 
	|- $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.

	|- $MINMAX.
	f::$monotonic,
	H::=$increasing_points(f).
	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), 

}=::TARSKI_KNASTER.

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

 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) )  }?

.Close

. Semi-orders
Semi-orders are used for several urposes including the modelling
of before/after relationships between events in time.
SEMIORDER::=Net{
.Source Luce 56, Library of Congress call number BF39.C66 and CACM, Feb 1978.
Set::Sets,  
P::@(S,S)= previous_to.
 |-(SO1):For all x,y,z,w:S, if x P y P z then x P w or w P z,
 |-(SO2): For all x,y,z,w, if x P y and z P w then x P w or z P y,
 |-(SO3): for no x(x P x).

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

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

}=::SEMIORDER.

. 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:
.See http://www.soc.unitn.it/dsrs/IMC.htm

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

PART_WHOLE::=Net{ 
	objects::Sets,  -- the things that are wholes and/or parts
	isin::$strict_order(objects).
	APO::=isin.
	|-(PW0): $MINMAX(Set=>objects, strict=>isin,...)

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

	Example1::=Net{
		objects::={auto,engine,radiator,radiator_cap,wheel1,wheel2,....}
		isin::={(engine,auto),(radiator,engine),(radiator,auto),..}
	 	universe::=auto.

		()|- engine isin auto.
		()|- radiator isin engine.
	}=::Example1.

	()|-(PW2): finite iff $objects in Finite.

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

	elements::={x || no $parts(x)},
	compounds::=$objects~$elements,
	()|-(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...
	is_component_of::=$isin~(|[i:2..]$isin^i),
	components::=map[x:$objects]/$is_component_of(x).
	()|-(PW7): |[i:2..]$isin^i = $isin^2,
	()|-(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:
	Example2::= Net{
	 objects={(0..r]| r:(0..)},
	  for all r1,r2:objects, (0..r1] isin (0,r2] iff r1<r2.
	  ()|- [0,r1] is_component_of [0..r2] iff r1<r2 and for no r3(r1<r3<r2).
	  But,
	  ()|- for all r1, r2, if r1<r2 then r1<(r1+r2)/2<r2 
	  ()|- for no x:objects, some components(x).
	}=::Example2.

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

	()|-(PW9): if $finite then $discrete.
. Proof of PW9
	Let{
	|-(0):	 not discrete,
	(0)	|-(1): for some x:compounds, no components(x)
	(1)	|-(2): some parts(x0), 
	(1)	|-(3): parts(x0)==>parts^2(x0),
	()	|-(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)},
	()	|-(6): R==>(<>),
	()	|-(7): R in (any)-(some),
	  (choice)|-(8): some  f:(any)-(1)(f==>R),
	()	|-(9): map[i](x0.f^i): Nat-->parts(x),
	()	|-(10): not finite.

. Proof of 4
		Let{
		|-	(4.1): y in parts(x0), 
		(3)	|-(4.2): y in parts^2(x0), 
		(4.2)	|-(4.3): y in parts(x2) and x2 in parts(x0), 
		(4.3)	|-(4.4): y <> y' in parts(x0)
		}
	}
choice::=See 
.See http://www/dick/maths/logic_5_Maps.html#Choice

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

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

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

	(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) ) }
	(def)|-(PW10): For x,y, interface(x,y)=glb{x,y}.

	TAGGING::=Net{ 
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.

	labels::Sets, 
	tags::#labels.
The notation for strings of symbols (#, !, ...) is in
.See http://www/dick/logic_6_Numbers..Strings.html
and
.See http://www/dick/math_62_Strings.html

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

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

	}=::TAGGING.

	hierarchy::@ for all x,y (no $common(x,y)).
	tree::@= $discrete and $hierarchy.
	branches(x) ::=|[I:@Nat]{B:I-->$objects||$components($objects) and B[1]=x).
	infinite_branches(x) ::={B:$branches||cor(B) in InfiniteSets).
	expansion::Nat0=fun[x]Card($components(x)).

	A Version of Konig's Infinity Lemma [Knuth 69,Vol 1, 2.3.4.3 Theorem K.]	
	()|-(Konig1): if not $finite and $tree and for all x($components(x) in FiniteSets)) then for some $infinite_branches($universe).
. Proof of Konig1
	Let{ 
	|-(K0): not $finite, 
	|-(K1): $tree, 
	|-(K2): for all x($components(x) in FiniteSets).

	 ()|-(K3): for all x:$objects, if $parts(x) in InfiniteSets then for some y:$components(x)($parts(y) in InfiniteSets)
  	 B1:=$universe,
  	 ()|-(K4):$parts(B1) in Infinite,
  	 ()|-(K5):some y:$components(B1)(y in InfiniteSets),
  	 ()|-(K6):B2 in $components(B1) and $parts(B2) in InfiniteSets,
    	...


. Proof of K3
		Let{ 
			|-(K3a): x:$objects,	
			|-(K3b): $parts(x) in InfiniteSets,
			|-(K3c): all y:$components(y)($parts(x) in FiniteSets).
			()|-(K3d): $components(x) in FiniteSets,
			()|-(K3e): $parts(x)>=={$parts(y)||y:$components(x)} in $finite
			()|-(K3f): Card($parts(x))=+[y:$components(x)]Card($parts(y))<>infinity
			()|-(K3g): parts(x) in finite.
   		}
	}
}=::PART_WHOLE.

Part_whole::=$ $PART_WHOLE.

FINITE_PART_WHOLE::=Net{
	|- $PART_WHOLE
	|-(FPW0): finite.
	()|-(FPW1): one N:Nat, all x($expansion(x)<=N).

	N::=the N:Nat, all x($expansion(x)<=N)
.Hole
	()|-(FPW2):  for all x, some l:$components(x)-->1..N
	()|-(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)}.
}=::FINITE_PART_WHOLE.

. Is_a

IS_A::=Net{ for describing generaliaztion, subtyping, subclasses, inheritance, exported...
	objects::Sets,  
	isa::strict_order(objects).
	AKO::isa.
	|- MINMAX(Set=>objects, strict=>isa,...)
	universe::objects.
	|-(isa1): lub(objects)={universe}. 
	super::@(objects,objects).
	|-(isa2): isin =super;do(super).
	|-(isa3): sub=/super.
	For A:Sets, p:objects->A, inheritted(p) ::@=for all objects x,y(if x isa y then p(x)=p(y)).
	For A, p, exported(p) ::@=for all objects x,y(if y  isa x then p(x)=p(y)).
}=::IS_A.

.Open Specially Ordered Sets
. Totally Ordered Sets
TOSET::=$ORDER and Net{total}.
totally_ordered_set::=$Toset.
Toset::= `Totally Ordered Sets`
Toset::= $ $TOSET,
 For X, toset(X) ::=$Toset(X).$Set,
toset::=$Toset.$Set. 

Totally ordered sets are also known as linearly ordered sets:
Linearly_ordered_sets::=$loset.
loset::=$toset.
Loset::=$Toset.
. Well Ordered Sets
WOSET::=Net{
	A partially ordered set where every subset has one least element.
	$ORDER.
	|-(WO0): for all S:@$Set~{{}} (one least(S)).
	bottom::=the least($Set),
	\bot::=$bottom.
	|-|-(WO_induction): invariants(strict) & (in(\bot))={$Set}.
}=::WOSET.
well_ordered_set::=$woset.
Woset::=`Well ordered sets`::= $ $WOSET,
 For X,woset(X) ::=$Woset(X).$Set,
woset::=$Woset.$Set. 

(Nat, <=) in $ $WOSET.

Knuth has a different definition 
.Source Knuth 69, 1.2.1.Ex15.
KWOSET::=Net{  Knuth's Well Ordered Set.
	S::$Set, 
	(<) ::Transitive(S) and Trichotomettic(S).
	(<=) ::=(<|=), 
	(>) ::=(/<), 
	(>=) ::=(/<=).
	|-(KWO0):For all A:@S~{{}}, some min(A).
	()|-(KWO1): For all A, one min(A).
	()|-(KWO2):(<) in Left_limited(S). [Knuth 69, 1.2.1.Ex15.f].
.See http://www/dick/maths/math_11_STANDARD.html#Kinds of relations
	()|- (KWO3): no s:Nat->S(>(s)).

()|- (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 
.See NOETHERIAN_INDUCTION
}=::KWOSET.

. Well-Founded Sets
WELL_FOUNDED_SET::=Net{  Not to be confused with a well ordered set!
	A well_founded set is a partially ordered set where the relation is
left_limited.  This means that any sequence:
	...x3<x2<x1<x0
has to be finite.  In otherwards there are no infinite descending chains.
	|-(WF0): $ORDER(S, <=,<,>,>=).
	|-(WF1): (<) in Left_limited(S).
.See http://www/dick/maths/math_11_STANDARD.html#Kinds of relations
	Minimal::=`Set of elements greater than nothing else`:@S,
	Minimal::= {x:S || for all y:S(not y < x)}.
}=::WELL_FOUNDED_SET.

NOETHERIAN_INDUCTION::=Net{
Emmy Noether's discovery - The Strongest Induction Principle Known to Humanity.

	WELL_FOUNDED_SET(S=>X).
	|-|-(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).

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

}=::NOETHERIAN_INDUCTION.

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

.Close Specially Ordered Sets

. See Also
See 
.See http://www/dick/maths/math_24_Domains.html
and 
.See http://www/dick/maths/math_41_Two_Operators.html#LATTICE
for further developments in the theory of orders.
.Close Orders