To the best of my limited knowledge, this formalism is credited to John von Neumann.

A context may, for some type – call it nice

– of
collection, define a nice

to be: a nice
collection of nice ordinals which subsumes each of its members; the principle
of strong induction then says that, for any type of nice ordinal, we can prove
that all nice ordinals are of this type iff we can prove that any nice ordinal
whose members are of the given type must itself be of that type (the slogan
here being: if constructing a nice ordinal not of this type necessarily
depends on having one of them already, as a member, there is no way you can
construct one, so they don't exist). **ordinal**

Examples: when nice

is finite we obtain the
finite ordinals, a standard (and very useful) model of the counting numbers
(taking 0 as the first

counting number, but hey). For those familiar
with the orthodox notion of a set

, which I model as a type of
collection, one obtains the set ordinals known to that orthodoxy as the
ordinals

.

It is worth noting early that a context using such a construction may need
to take care not to use it too liberally – it will shortly emerge that a
context which allows this construction for some type, nice, for which {nice
ordinals} is nice, that context is doomed to inconsistency (the principle of
strong induction is very powerful). That it works for finite and set is
largely a tribute to how strong a condition finite

is and how well
designed the orthodox notion of set

is. That it can patently lead to
inconsistency if allowed too liberally may be viewed as a downside of this
approach: but I find it very beautiful, so I'm giving my best account of it,
rather than supposing that all contexts will be happy to let me model the
naturals this way.

In so far as any intersection of a non-empty collection of nice collections is guaranteed to be nice, any non-empty intersection of nice ordinals is a nice ordinal. Proof: each member of the intersection is a member of each of the nice ordinals intersected; hence is a nice ordinal and subsumed by each of the nice ordinals intersected, hence also by their intersection.

In so far as the union of any nice collection of nice collections is
guaranteed to be be a nice collection, any nice union of nice ordinals is
necessarily a nice ordinal. Proof: each member of the union is a member of
(at least) one of the nice ordinals united, hence subsumed by this, hence
subsumed by the union; and, being a member of some nice ordinal, is a nice
ordinal. So the union is nice and subsumes each of its members, each of which
is a nice ordinal. Example: In particular, each nice ordinal is a nice
collection of nice ordinals, so its union is a nice ordinal. I'll describe an
ordinal as a nice **limit** if it is equal to its union.

Presumptions: the notion of nice ordinal

only makes sense in so far
as nice

is such a notion as guarantees that empty is a nice collection
and the successor of any nice collection is also nice – or, to put it
another way, I'm not aware of anyone using it other than for the sake of an
initial portion satisfying Peano's axioms (there's a first one, which isn't
the successor of anything; each of them has a successor; and the successors of
distinct ones are distinct). So I'll presume this holds for whatever notion
of nice

is under discussion.

Empty is (presumed) nice and has no members to let it down on the rest of the definition of a nice ordinal, hence it's a nice ordinal. If n is a nice ordinal, it subsumes each member of successor(n) = {n, i: i in n}, which subsumes n, so successor(n) subsumes each of its members; each member of successor(n) is a nice ordinal and successor(n) is (presumed) nice, hence it is also a nice ordinal. We may thus introduce a known collection of nice ordinals, Peano = {empty, successor(i): i in Peano}.

**Theorem**: no nice ordinal is a member of itself.

Proof: describe a nice ordinal as clean, for the duration of this proof, precisely if it is not a member of itself. For any nice ordinal N whose members are all clean and any n in N, we have:

n in Nandn not in nso N has a member which n lacks, enabling us to distinguish n from N. Thus N isn't equal to any of its members, so N is clean. [The definition of the nice ordinals gives us no unclean ones and we cannot construct any.] Thus, by (strong) induction, every nice ordinal is clean. QED.

Since the collection of all nice ordinals subsumes each of its elements,
each of which is a nice ordinal, we need it to not be nice, or it'd be a nice
ordinal, a member of itself and a contradiction of the theorem above. One
could get into deep trouble by trying the case where nice

means is
not a member of itself

, unless by finding a better-behaved type which
subsumes this one.

Now stand back a step: construe the definition of nice ordinals as a mapping between types of collection, expressing each type t by the collection {c: c isa t}; one of the mapping's atoms is {nice ordinals} ← {nice collections}, at least whenever strong induction holds true for {nice ordinals}. Considering any type, t, to be synonymous with {c: c isa t}, this can be phrased as: let C = {t: {collections} subsumes t}; define

- ordain = (C: p is not in t; p = {n in t: p subsumes n subsumes each i in n} ←t :C)

The constraint p is not in t

immunizes this against the
contradiction: any t for which the given value for p would be in t, were
ordain to relate t to p, has been excluded. The price of this is that whether
a given collection is in (:ordain|) is not, in general, decidable.

No output of ordain is a member of itself and ordain accepts each of its
outputs as an input. Proof: given p = ordain(t), n in p implies p subsumes n
subsumes each i in n; p is not in t, which subsumes p, so p is not in p; so
ordain(p) = p whenever p is in (|ordain:); i.e. (|ordain:) = {p: p in
ordain}. Thus fixed point of ordain

and output of ordain

are
synonyms; and ordain&on;ordain = ordain is a projection

.

So (|ordain:) is a collection of collections, hence in C: does ordain
relate it to anything ? Well, p in (|ordain:) implies p = ordain(p) is not in
p; in particular, p in (|ordain:) and p not in p

enables us to
distinguish p from (|ordain:) – one has a member the other lacks –
hence (|ordain:) is not a member of itself. From that one might expect to be
able to infer that ordain relates (|ordain:) to itself, but this would make
(|ordain:) a member of itself; the undecidability of is it in
(:ordain|) ?

is a prerequisite for surviving this conflict.

This is at least disconcerting, since ordain sets out to relate t to p
whenever p isn't in t and p subsumes each of its members, each of which
subsumes, in turn, each of its members – all of which holds true for
(|ordain:) as long as ordain *doesn't* relate it to
anything …

I would ideally replace p is not in t

with a constraint which
asserts that the principle of strong induction works in p without leading to a
contradiction; such a replacement would indeed imply p is not in t

. It
would be particularly interesting if the two constraints were
equivalent … or if some replacement for p is not in t

could
enable one to decide which collections are in (:ordain|). Whether strong
induction works for p

is up to this task is another interesting
question.

As to the appropriate phrasing of strong induction works for p

: for
such a type p and any type t, we can ask whether t subsumes n in p

implies n in t

; strong induction says that, if it does, t subsumes
p. So describe a collection, p, of collections as strongly inductive

iff p is subsumed by every t for which t subsumes n in p

implies n
in t

; we can then work with ({strongly inductive collections}: ordain :C)
in place of ordain. I'll retain the p is not in t

clause, as I suppose
discarding it would lead to trouble still.

Note, in particular, the collection t = {collection c: c not in c}:
whether things are members of t is plainly, in general, undecidable: t cannot
be equal to any of its members (since none of them is a member of itself),
which would appear to mean it is not a member of itself; in which case it
should be a member of itself. None the less, we can probe t by examining its
relationship with strongly inductive types: for any n, t subsumes n

says i in n implies i not in i

which, in turn, implies i in n
implies i is not n

since, unlike n, i doesn't have i as a member; so
if n in t

is decidable, it's true; i.e. if n in n

is decidable
it's false; if combining t subsumes n

with n in p

, for some
strongly inductive type p, renders n in n

decidable, we then find that
t subsumes p. If t were in (:ordain|) we'd get ordain(t) = p = {n not in n: p
subsumes n subsumes each i in n}, which t subsumes; this will only happen if
the resulting p is not in t, i.e. if p is in p, but p would then be in t; so t
isn't in (:ordain|), but does subsume (|ordain:).

Any member of a fixed point of ordain is itself a fixed point of ordain – i.e. (|ordain:) subsumes each of its members. Proof: consider n in p = ordain(t); ordain(n), if defined, must be {i in n: ordain(n) subsumes i subsumes each j in i}; since n is in p, n subsumes each i in n; since p subsumes n, each such i is in p, so subsumes each j in i; so, unless n is in n, ordain(n) is n.

Notice that empty is a fixed point of ordain. For any fixed point, p, of
ordain, consider p's successor. Now, n in ordain(successor(p)) iff n in
successor(p) and successor(p) subsumes n subsumes each i in n: n in
successor(p) means either n is p (in which case successor(p) does indeed
subsume n) or n is in p (whence, as successor(p) subsumes p, it also subsumes
n, which subsumes each i in n); thus, indeed, successor(p) =
ordain(successor(p)) is also a fixed point of ordain. One of the
characteristics of ordain's outputs is p subsumes each of its members, each
of which subsumes each of

, which may be re-phrased
as *its* membersn in successor(p) implies n subsumes each i in n

. If p is in
(:ordain|), this will imply p = ordain(p).

Consider a union of fixed points of ordain. Each of its members is in (at
least) one of the fixed points united; so it is subsumed by that fixed point;
hence equally by the union. So the union subsumes its members. Each member,
being a member of some fixed point, equally subsumes each of its
members. Likewise, each member of a non-empty intersection of fixed points of
ordain is in each of the fixed points in question, hence subsumed by each,
hence subsumed by the intersection; and, the intersection being non-empty, is
a member of some fixed point of ordain, so subsumes each of its members. Thus
either a union or a non-empty intersection of fixed points of ordain yields a
collection, p, for which n in successor(p) implies n subsumes each i in
n

.

**Theorem**: for any two nice ordinals, either they are equal or
one of them is a member of the other.

Proof: for the duration of which,

- for any nice ordinal m, describe any nice ordinal n as m-definite iff either m is in n or n is in successor(m) – i.e. is either m or a member of m
- describe a nice ordinal, m, as definitive iff every nice ordinal is m-definite
It suffices to prove that every nice ordinal is definitive.

So, consider a nice ordinal, M, each member of which is definitive; in order to determine whether every natural is M-definite, consider a natural N of which each member is M-definite.

Each member of N is M-definite; if M is a member of any member of N, it is also a member of N; if N is a member of successor(m) for any m in M, then N is in M, hence in successor(M); otherwise, each m in M is in N and each n in N is in successor(M); i.e. successor(M) subsumes N subsumes M. Then either M is in N, in which case N (being a nice ordinal, so subsuming this member) is successor(M); otherwise, all N's members are in M, so M subsumes N, whence M = N. The first case gives M in N, the second gives N in successor(M), as was true of the cases set aside at the outset; hence N is M-definite.

Each member of N is M-definiteimpliesN is M-definitewhence, by strong induction, every nice ordinal is M-definite, so M is definitive.Each member of M is definitiveimpliesM is definitive, whence every nice ordinal is definitive. QED.

On relations (in general) successor is defined as the mapping which takes
any relation, r, to its union with the collection {r}. This differs from r
unless r in r

. Note that successor(r) subsumes r and, consequently,
anything that r subsumes. If a nice ordinal is the successor of anything,
then that thing is a member of (and subsumed by) our nice ordinal and,
consequently, a nice ordinal (but note that empty, among others, is not the
successor of anything).

Consider any m in n, both nice ordinals: m is in n, so n subsumes m and, having m as a member, subsumes successor(m). Thus n subsumes unite(|successor:n): but each m in n is in successor(m) hence in this union, which thus subsumes n. Therefore, every nice ordinal is the union of the successors of its members, n = unite(|successor:n). (Note that unite(empty) is empty.) Equally, this says that n = unite(|successor:n) = unite(n)&unite;n = unite(successor(n)).

Every nice ordinal subsumes itself and each of its members, thus every member of its successor. If two nice ordinals have equal successor, each is a member of the other's successor so each subsumes the other, making them equal. Thus (: successor :{nice ordinals}) is monic. Since it doesn't produce empty as an output, so we find that {nice ordinals} is infinite.

**Lemma:** Every non-empty collection of nice ordinals has a
minimal element. Let N= intersect(C) for some non-empty collection, C, of
ordinals. N is a nice ordinal, so not a member of itself, so there must be at
least one member of C of which N is not a member. However, every member of C
subsumes N, so none of them is in N: N isn't in our given member of C, so the
order theorem only leaves the option of this member of C being N. Thus the
intersection of any non-empty collection of nice ordinals is one of the
members of the collection: and is a member of all the others. [Note, for
contrast, that the union of a non-empty (nice) collection of nice ordinals
need not yield one of the ordinals united – try any non-empty
limit.]

As mentioned above, I'll describe a nice ordinal as a (nice) limit iff it is equal to its union.

Consider a nice ordinal N and some n in N: we have n in N, so N subsumes n, so N subsumes successor(n), which is also a nice ordinal. Since N isn't a member of itself, it consequently isn't a member of successor(n); so, by the order theorem, either N is successor(n) or successor(n) is in N. Thus the successor of any member of N is either a member of N or equal to N: equally, any nice ordinal N either is the successor of one of its members or subsumes (|successor:N).

For any nice ordinal N, consider unite(N), which is the union of a nice collection of nice ordinals, hence a nice ordinal. We know N = unite(|successor:n), and since N subsumes each of its members, it also subsumes unite(N). The last paragraph tells us that either N subsumes (|successor:N) or N is successor(n) for some n in N. In the latter case, n subsumes every member of N so unite(N) is n, which isn't N. The former implies unite(N) subsumes unite(|successor:n) = N which subsumes unite(N), so N = unite(N) is a limit.

Thus we separate the night from the day: any nice ordinal is either the successor of one of its members, or equal to the union of its members; but never both.

We can define an addition on the nice ordinals as follows: for any nice ordinals n, m

- n+m = unite(| successor :{x+m, n+y: x in n, y in m})

Note that unite(|successor:C), with C a collection of nice ordinals, is just the least nice ordinal which subsumes C: each of its members is either a member of C or a member of some member of C.

Whenever x+m, for each x in n, and n+y, for each y in m, is a nice ordinal, we see that n+m is a union of nice ordinals, hence a nice ordinal. This is all strong induction needs to let us infer that n+m as a nice ordinal for all nice ordinals n, m. Similarly, whenever x+m = m+x, for each x in n, and n+y = y+n for each y in m, we find n+m = m+n: and so, by induction, conclude that + is Abelian.

When n is 0=empty, this is unite({successor(0+y): y in m}), so whenever every y in m has 0+y=y we obtain 0+m= unite(|successor:m) = m so, inductively, 0+m = m for every natural, m: likewise n+0 = n for every natural n. This is why empty is called 0: it is a natural additive identity.

When n is 1={0}, we have 1+m = unite(| successor :{0+m, 1+y: y in m}) = successor(m) &unite; unite({successor(1+y): y in m}). Now, if every member of m has 1+y = successor(y), which is either m or a member of m, so successor(1+y) is either successor(m) or one of its members: in either case, successor(m) subsumes unite({successor(1+y): y in m}) so we have 1+m = successor(m). Again, this is all strong induction needs to let us infer 1+m = successor(m) and, similarly, m+1 = successor(m) for every nice ordinal m. Consequently, I shall use 1+m in place of successor(m), for brevity.

For each x in n, we have x+m in n+m; for each y in m, we have n+y in n+m. Likewise we also obtain x+y in x+m and in n+y, either of which is in n+m and so subsumed by n+m, hence x+y in n+m. Since we're uniting successors, any member x of n permits us to ignore each t+m with t in x, because its successor will still be in the union by virtue of t+m being a member of x+m: likewise for any given y in m we can ignore n+s with s in y.

**Theorem**: addition is associative – i.e., for any
nice ordinals a, b, c, the sums (a+b)+c and a+(b+c) are
equal. **Proof**:

- (a+b)+c
- = unite(| successor :{u+c, (a+b)+z: u in a+b, z in c})
Now, u in a+b is, wlog, either a+y with y in b or x+b with x in a – every other value u could take is a member of one of these, so its contribution is subsumed by that of a u of the given form – so

- = unite(| successor :{(x+b)+c, (a+y)+c, (a+b)+z: x in a, y in b, z in c})
- a+(b+c)
- = unite(| successor :{a+v, x+(b+c): v in b+c, x in a})
- = unite(| successor :{a+(b+z), a+(y+c), x+(b+c): x in a, y in b, z in c})
and we see that, so long as each z in c has a+(b+z) = (a+b)+z, each y in b has (a+y)+c = a+(y+c) and each x in a has x+(b+c) = (x+b)+c, the first of these is the second, so a+(b+c) = (a+b)+c. Again, this suffices to induce that addition is associative.

In particular, (1+n)+m = 1+(n+m) = (n+m)+1 = n+(m+1), or successor(n)+m = successor(n+m) = n+successor(m).

One way to define multiplication is in terms of repetition, via (: repeat :{ordinals}) defined by repeat(0) = ({(:x←x:)}: |{relations}) – which maps every relation to the universal identity – and repeat(successor(n),r) = r&on;repeat(n,r), though handling of limits is an issue. We can then note that repeat(n,r)&on;repeat(m,r) = repeat(n+m,r) for any relation r and that repeat(n)&on;repeat(m) is what repeat(n.m) should be. [The members of (|repeat:) are known as Church ordinals; Alonzo Church formalized the naturals in terms of repetition.]

Another approach would be to use

- unite(| successor :{x.m +n.y −x.y: x in n, y in m})

as n.m, if we can first define subtraction. [Note that the given formula is n.m −(n−x).(m−y) which, when n and m are successors, gives n.m−1 among the values fed to successor and united, so we do have enough example members of n.m.] However, I don't see that working too well with limits … I'm not convinced we can do subtraction sensibly – i.e. that m in n implies the existence of p in n with m+p=n. Still, we can simulate a−b with {h: h+b in successor(a)}; when a is p+b for some nice ordinal p, this is just what we need, while at least specifying something guaranteed to exist when a is a limit. Using this approach suggests, for nice ordinals n and m, using

- {nice ordinal h: h + x.y in successor(x.m + n.y) for some x in n, y in m}

as n.m – and note that we can get rid of the unite(|successor:{…}) machinery of earlier definitions, since h+x.y in successor(x.m+n.y) ensures the same holds for each of h's members.

Now, by construction, n.m is a collection of nice ordinals. If we are given that x.m, n.y and x.y are nice ordinals whenever x is in n and y is in m, we have: successor(x.m+n.y) as a nice ordinal; if h+x.y is a member of this, then so is h; uniting successor(x.m+n.y) for each allowed x and y, we thus get a union of nice ordinals – hence a nice ordinal – which subsumes n.m; whence n.m is indeed a nice ordinal. Again, this is all we need for strong induction to imply that n.m is indeed a nice ordinal whenever n and m are.

Since addition is Abelian, x.m + n.y = n.y + x.m; then, for n.m to be equal to m.n, it suffices that every x in n and y in m obey x.m = m.x, y.n = n.y and x.y = y.x, as applying these will transform the formula for n.m into that for m.n; this is in an appropriately strong-inductive form, so we can duly infer that n.m is, indeed, equal to m.n for all nice ordinals n, m; thus that multiplication is Abelian.

When either n or m is empty, either x or y is accordingly granted no possible values, hence no h can satisfy the constraint and n.m is necessarily empty; thus 0.m = 0 = m.0 for every nice ordinal m. When n is 1 = {0}, we have x = 0 as x's only candidate, so a nice ordinal h is in 1.m iff h+0 is in successor(0+1.y) for some y in m; i.e. 1.m = unite(|successor:{1.y: y in m}); thus, if 1.y = y for every y in m, then 1.m will be equal to unite(|successor:m), which is m. This is enough for strong induction to tell us that, indeed, m.1 = 1.m = m for every nice ordinal m: 1 is an identity for multiplication.

**Theorem**: multiplication is associative – i.e., for
any nice ordinals n, m, r, the products (n.m).r and n.(m.r) are equal.
**Proof**: (missing)

The natural numbers is the collection of finite ordinals. [A collection S
is finite iff: for any mapping (S:f|S), f is monic iff f is epic

– that is, f is one-to-one iff (|f:) = S.] We have empty finite
because: (empty: f |empty) tells us that f is, in fact, empty, with (|f:) =
empty; and (|f:) = empty implies f = empty, with empty being a mapping and
equal to its reverse, hence one-to-one. If a nice ordinal n is finite, let N
be successor(n) and consider any mapping (N:f|N). Now, (:f:n) is a mapping
and is trivially (:f|n), since N subsumes n:

- if (N:f|N) is monic
then so is (:f|n). Now, f is monic, so if n is in (|f:n), then n is not f(n) and we can introduce the permutation (N|s|N) of n which swaps n and f(n) but acts as the identity on all other members of N; then s&on;f is also monic, with s(f(n)) = n and n not in (|s&on;f:n). Otherwise, n is not in (|f:n) so take s = N, the identity. Either way, n is not in (|s&on;f:n), yet (N:s&on;f|N), so n subsumes (|s&on;f:n) and we have (n:s&on;f|n) monic, hence epic, hence (|s&on;f:n) = n and (N:s&on;f|N) is monic, so s(f(n)) is in N but not in (|s&on;f:n) = n, hence s(f(n)) = n and (|s&on;f:N) is indeed N, whence s&on;f is epic; but s is just a (self-inverse) permutation, hence f is also epic.

- if (N:f|N) is epic
then n is in N = (|f:N), so let i = unite({n}:f|); this is the maximal member of N with f(i) = n. If i is n, let s be N, the identity on F's inputs; otherwise, let (N|s|N) be the permutation which swaps i and n and acts as the identity on the rest of N. Then (N:f&on;s|N) is also epic and maps n←n. Now, (|f&on;s:n) includes every member of N except possibly n = f(s(n)), hence subsumes n, so (n|f&on;s:n) is an epic mapping, hence monic (n:f&on;s|n) and, in particular, n = f(s(n)) is not in (|f&on;s:n), so (N:f&on;s|N) is also monic. Since s is a simple transposition, or the identity, we infer that f is also monic.

Thus n being a finite ordinal implies successor(n) is finite, so the successor of a finite ordinal is a finite ordinal.

Now, {naturals} = {finite ordinals} has a monic ({naturals}: successor
|{naturals}) which is *not* epic – empty isn't in (|successor:)
– hence {naturals} is not finite (which is just what we need to avoid
paradoxes, above). Indeed, {naturals} is the minimal
ordinal isomorphic to its successor. The isomorphism in question is (:
successor :{naturals})&unite;(: empty←{naturals} :), which is
({naturals}| |successor({natural})), with inverse (: {naturals}←empty
:)&unite;({naturals}| n ← successor(n) :{naturals}).

We call {} 0 and its successor, {0}, 1. [We can then represent any finite ordinal as a function from some finite ordinal to {0,1} (which we needn't name), writing those functions as finite binary strings with the usual interpretation. Thus naming 0 and 1 suffices to name all the finite ordinals (they are themselves, of course, the standard way of writing the two functions from 1 to {0,1}).]

Peano's axioms tell us to accept as valid: any property of the empty set, combined with any proof that a nice ordinal (or a finite ordinal, if we only want to prove a finite case) with that property constrains its successor to have that property, implies that every (finite) ordinal has that property. I think Peano stated the finite case, and I'm inclined to mistrust the infinite forms.

I believe I need to discuss the relationship between the set ordinals and the isomorphism classes of sets.

Within the category Set, we have a sub-category consisting of its
isomorphisms (which include all identities and permutations). Describing a
collection of sets as iso-closed if, between each pair of its members, there
is at least one isomorphism: an **isomorphism class** is an
iso-closed collection of sets which is not a proper sub-collection of any
iso-closed collection of sets.

One readily sees that: every set is a member of some isomorphism class; every (monic) embedding, aka injection, of one set in another implies at least one embedding of any member of the former's isomorphism class in any member of the latter's; likewise for any (epic) surjection. Set (or, possibly, Set with the axiom of choice) may be thought of as being characterized by: wherever an epic and a monic are parallel, there is an iso parallel to them. Consequently, if: there is an epic from some member of one isomorphism class to some member of another; and also a monic from some member of the first to some member of the second: then there is an iso between some member of the first and some member of the second, whence, since their union is thus iso-closed, they are not proper subsets of it: thus they are equal to it and, so, to one another. Thus, between one isomorphism class and a (different) nother, there can be monic or epic functions but not both. Our next interesting assertion about Set is that between any two isomorphism classes of Set, there are epics in one direction and monics in the other.

With the given assertions about the category Set, we now look at the ordinals. First: for any set, S, let sub(S) be the set of isomorphism classes from which there is a monic but no epic to S. For a nice ordinal, we have

Valid CSS ? Valid HTML ? Written by Eddy.