MATHS: Orders

Set of Elements	Relationships that impose an order
Plans	cheaper, easier, more fun, do_before, ...
Products	safer, cheaper, faster, bigger, smaller, better, worse,...
Events	Occurs before, more likely than,...
Numbers	Less than, greater then, less then or equal, greater then equal
Natural Numbers	divides
Points in space	above, below, to the right, to the left, before, behind
Components in a system	is a part of (APO), part_whole, composition
Types of Objects	is a kind of (AKO), inheritance, derived_from, subtype_supertype
Parts of a program	depends on
Subsets of a set	==>(subset of)
Sets	functional dependency(there exists a many-one mapping from _ to _)
Sets	existence dependency(for each _ there must exist a unique fixed _)
Letters	Earlier in the alphabet
Words	dictionary order (lexographic order)
Boolean Values	implies
{a,b,c,x,y,z}	{(a,x),(a,y),(a,z), (b,x), (b,y), (b,z), (c,x), (c,y), c,z)}

Set of Elements	Relationships
Points in space	close to, surrounding
Numbers	Having the same remainder with respect to a particular divisor

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.

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.
(Sets) |- finite::@= (Set in FiniteSets).
total::@= (relation in Total(Set)).
(def)|- (O4): if total then not_comparable_with = {}.

}=::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.

Net{

Set

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.

|- (K1): Set={a,b,c,d,e,f},
(<)={a,b,c}><{d,e,f}
()|-ORDER.
...more below

(End of Net)

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

x	a	b	c	d	e	f	g
a
b	a	.
c	a	b	.
d	a	.	.	.
e	a	.	.	.	.
f	a	.	.	d	e	.
g	a	.	.	d	e	f	.
\| x.> \|	6	1	0	2	2	1	0
\| x.< \|	0	1	2	1	1	3	4

Net{

|-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 finite S then some least(S) and some greatest(S).
[ 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.
(above)|- (OP7): for all S:Set, min S ==> least S ==>S.
(above)|- (OP8): 0..1 min S.
(above)|- (OP9): max S ==> greatest S==>S.
(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.
(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:
Kuratowski(3,3)::=
Net{
1. K1 ...from above
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
}=::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)},
(above)|- (OP12): lb({})=ub({})=slb({})=sub({})=Set.
(above)|- (OP13): for all x:sub(S)|slb(S) (not x in S).
(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).
(above)|- (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 [ SEMILATTICE in math_32_Semigroups ] and [ LATTICE in math_41_Two_Operators ]
for this approach.

Example Kuratowski Part 3
Kuratowski(3,3)::=
Net{
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}
}=::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),
supremum(S)::@Set= the(i:ub(S) || for all b:ub(S)(b inverse i)),
inf(S)::=infimum(S),
infimum(S)::@Set= the(s:lb(S) || for all b:lb(S)(b relation s)),
(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
For S:@Set~{{}},
sinf(S)::=strict_infimum(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_suprememum(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)),
(above)|- (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))).
(above)|- (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).

Duality
1. DUALITY_BASIS::=following,
  Net
  1. X:Set. f, g:: X>->Real & Positive.
  (End of Net)
  Example of one solution solving two problems
  
  Net
  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,
  Net
  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?
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.

Net{

|-MINMAX.
(complete): For all S:@Set ~{{}}, one lub(S).
Source: Manes & Arbib 86

}=::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.

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.

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).
(above)|- (SO4): for some f:Real^Set, δ:Real ~ Negative, for all x,y( f(x) > f(y)+δ iff x P y).
For x,y:S, x concurrent y::= not (x P y) and not (y P x).

}=::SEMIORDER.

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{
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.
}=::Example1.
(above)|- (PW2): finite iff finite objects.
parts::=/isin, -- the parts of x are those things "isin x".
(above)|- (PW3): For x:objects, parts(x)= {y:objects || y isin x}.
(above)|- (PW4): For no x (x in parts(x)).
(above)|- (PW5): for all x (x in parts(universe)).
elements::={x || no parts(x)},
compounds::=objects~elements,
(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...
is_component_of::=isin~(|[i:2..]isin^i),
components::=map[x:objects]/is_component_of(x).
(above)|- (PW7): |[i:2..]isin^i = isin^2,
(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)}...
}.

Net{

objects={(0..r]| r:(0..)},
for all r1,r2:objects, (0..r1] isin (0,r2] iff r1<r2.
(above)|-[0,r1] is_component_of [0..r2] iff r1<r2 and for no r3(r1<r3<r2).
But,
(above)|-for all r1, r2, if r1<r2 then r1<(r1+r2)/2<r2
(above)|-for no x:objects, some components(x).

}=::Example2.

Net{

labels::Sets,
tags::#labels. The notation for strings of symbols (#, !, ...) is in [ logic_6_Numbers..Strings.html ] and [ 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.

Net{

|-PART_WHOLE
|- (FPW0): finite.
(above)|- (FPW1): one N:Nat, all x(expansion(x)<=N).
N::=the N:Nat, all x(expansion(x)<=N) [click here if you can fill this hole]
(above)|- (FPW2): for all x, some l:components(x)-->1..N
(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)}.

}=::FINITE_PART_WHOLE.

Net{

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.

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),
⊥::=bottom.
|-|-(WO_induction): invariants(strict) & (in(⊥))={Set}.

}=::WOSET.

Net{

S::Set, (<) ::Transitive(S) and Trichotomettic(S). (<=) ::=(<|=), (>) ::=(/<), (>=) ::=(/<=).
|- (KWO0): For all A:@S~{{}}, some min(A).
(above)|- (KWO1): For all A, one min(A).
(above)|- (KWO2): (<) in Left_limited(S). [Knuth 69, 1.2.1.Ex15.f]. [ Kinds of relations in math_11_STANDARD ]
(above)|- (KWO3): no s:Nat->S(>(s)).
(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 ]

}=::KWOSET.

Net{

WOSET

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). [ Kinds of relations in math_11_STANDARD ]
Minimal::=Set of elements greater than nothing else:@S,
Minimal::= {x:S || for all y:S(not y < x)}.

}=::WELL_FOUNDED_SET.

Net{

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.