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

Ordinals

A context may, for some type – call it nice – of collection, define a nice ordinal 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).

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.

What does that give us ?

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 N and n not in n so 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

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 its members, which may be re-phrased as n 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.

Order

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,

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-definite implies N is M-definite whence, by strong induction, every nice ordinal is M-definite, so M is definitive. Each member of M is definitive implies M 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.]

Limits

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.

Addition

We can define an addition on the nice ordinals as follows: for any nice ordinals n, 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).

Multiplication

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

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

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

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.

Isomorphism classes

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.