### Order Types

There is a nice little theory of order types that examines simple orderings up to isomorphism.
It is not little in its potential but the literature is fairly small.
There are several nice easy results.
For each non-negative integer n there is just one order type of n elements.
There are many denumerable order types.
The positive integers, the negative integers and all integers are of three distinct denumerable order types if we assume their ordinary ordering.
One writes the order type of the positive integers as ω.
If x is an order type then x* is the reverse order type.
ω* is the order type of the negative integers.
If x and y are order types then x+y is the order type where all elements of x precede all elements of y.
This operation does not commute.
ω* + ω is the order type of the integers.
ω + ω* is the type of the reciprocals of the non-zero integers.
For finite n, n = n*.
In the context of order type expressions, digits denote order types.
“2” denotes the unique order type with two members.

If x and y are order types then x•y is the order type consisting of y copies of x.
It is a lexicographic ordering of the Cartesian product:

(x', y') ≤ (x'', y'') ↔ y' ≤ y'' ∧ (y' = y'' → x' ≤ x'')

This notation seems backwards but it is the convention.
2•ω = ω ≠ ω•2.
{1/n | n>0} ∪ {2 + 1/n | n>0} is a set of reals ordered as ω•2.
These two binary operators, + and • , both associate but neither commutes.
(a + b)•c = a•b + a•c does not generally hold but a•(b + c) = a•b + a•c always holds.
A nice theorem is that there is just one denumerable order type with the property that between any two distinct members, there is another, except it must be agreed whether there is a greatest element and whether there is a least element.
With neither this is the order type of the rationals, r.
r = r+r.
Applying Dedekind’s cuts to the order type of the rationals gives us the order type of the reals, R.
R = R + 1 + R.
Applying the cut to R leads to the same order type R and thus R is said to be ‘order complete’.
The order type R has the properties of the reals that are captured in point set topology.

The star performers of order types are the ordinals.
An order type is *well ordered* if every non-empty subset has a first element.
With the axiom of choice we can prove that any set can be well ordered.
Another easy theorem is that of two well ordered sets, one is isomorphic to an initial portion of the other.
This means that all well ordered types, called *ordinals*, are them selves simply ordered by set inclusion, indeed even well ordered.
Note that ω and ω•2 are well ordered and in fact distinct ordinals.