The definitions and proofs on this page emply an approach to induction which I learned from Conway. I may have messed it up somewhat in the process, of course. If you are happy with (non-naïve) set theory, you can use essentially similar methods to define the Ordinals – indeed, this page's Autumn '98 revolution is about the realisation that my page on the ordinals needed set theory only for a limited few properties I could have out of finiteness instead.

The Natural Numbers

The natural numbers are the counting numbers – the non-negative whole numbers. Some treatments of them, including mine, include zero as a natural, others do not. They are extensively studied.

Definition: a natural number is a finite collection of which every member is a natural number and a sub-collection. Thus empty, having no members, is a natural number because it is finite.

I could have defined the natural numbers to be the finite ordinals: instead I give a definition almost identical to that for the ordinals, but replacing set with finite collection. I chose to do this so that I have the natural numbers without needing to go into set theory: the definition above is more primitive than the finite ordinals definition.

Definition: a list is a mapping, f, for which (:f|) is a natural number: if this is successor(n), f is denoted [f(0), …, f(n)], though the sanity of that claim has to wait until later. For reference, a sequence is a mapping f for which (:f|) subsumes each of its members, each of which is natural; which will end up meaning that either (:f|) is a natural or (:f|) is {naturals}; in the latter case, f is described as an infinite sequence, for reasons which will become apparent.

A list f is described as a list of members of (|f:) or of any collection subsuming this (likewise for sequences). Thus, for instance, a list of naturals is a mapping ({naturals}:f|N) for some natural N. The left values of a list (or sequence) are described as entries in it; its right values are described as indices into the list. For any list f, the natural number (:f|) is referred to as the lengh of f; every valid index of f is a member of f's length.

Successor

The successor, N, of any natural number is, like the successor of any finite collection, finite: furthermore, it contains and subsumes its predecessor which, in turn, contains and subsumes (because it is a natural number) all of N's other members. Consequently, since subsumes is transitive, N subsumes all its members; all its members are natural numbers, so N is also a natural number. Thus the successor of any natural is natural.

Every natural subsumes itself and each of its members, hence every member of its successor. Two naturals with equal successor, of which each is a member, consequently subsume one another and are equal. A collection N is finite iff {monic (N|:N)} = {mapping (N:|N)}, so consider N = {naturals} and S = (N:successor|N), which is a mapping; it is monic, but it isn't (N|:N) because empty, in N, isn't a left value of N – it's not a successor – so {monic (N|:N)} and {mapping (N:|N)} aren't equal and N = {naturals} is infinite, i.e. isn't finite. In particular, {naturals} isn't a natural – which is a good thing.

Theorem: No natural number is a member of itself.

Proof: describe a natural number as clean, for the duration of this proof, precisely if it is not a member of itself. For any natural, N, whose members are all clean, and any n in N, we have: n in N and n not in n implying n not equal to N. Thus N isn't equal to any of its members, so N is clean. [To get an unclean natural number, you'd need to have one already, you aren't given any by the definition, so you can't get any.] Thus, by induction, every natural number is clean.

Note that the collection of all natural numbers is a collection of natural numbers and subsumes each of its elements. If it were finite, it'd thus be a natural number and a member of itself, which would be messy. Fortunately, I've already shown that it's infinite.

The theorem above, along with various others, follows the same form as for the ordinals; the naturals are simply the finite ordinals, so I'm removing (2000/Oct) large slices of this page which duplicate, less tidily, what I've now written there.

Old bits awaiting tidy-up

If we define < by m < n iff m in n in {naturals}, it is a full strict order on the naturals: for any n, m we have exactly one of n<m, n=m or m<n (as a side-effect of the previous theorem; combine any two of these statements and you'd find an unclean natural); in particular, given any two naturals, one of them subsumes the other (since n<m implies m subsumes n, m<n implies n subsumes m, and m=n implies each subsumes the other). If natural n subsumes natural m, n not in n implies n not in m, hence either m=n or m<n, i.e. m is in successor(n); so (: {natural m: n subsumes m} ←n |{naturals}) is ({naturals}:successor:).

Given a monic (m:g|n) for some naturals n, m, suppose n subsumes m. We can read the collection m as the relation (n: i←i |m), which is a monic mapping, and compose m with g to get (n: m&on;g |n) monic (n:|n) hence a mapping (n|:n), so m subsumes (:i←i:m&on;g) subsumes n. Since, for any two naturals n and m, either n subsumes m or m subsumes n, and any monic (m:g|n) enables the former to imply the latter, we may conclude: (m:g|n) monic implies m subsumes n when m, n are natural. Furthermore, whenever one natural m subsumes another, n, we have a monic (m:n|n) so, in fact m subsumes n iff there is some monic (m:|n).

Theorem: Every non-empty natural is a successor.

Proof: Consider a natural N. For any n in N, N subsumes successor(n). Either N is successor(n) or successor(n) is in N. Thus either N is the successor of one of its members or all such successors are members of N, that is N subsumes (|successor:N): in the latter case, we have monic (N:successor|N), making (N|successor:N), as N is finite; and empty isn't a successor, so it isn't in N, so it subsumes N, so N is empty. Thus either N is empty or N is a successor.

Thus:

or, to put it another way, Kroneker was right. Anything natural is conventionally called a natural number.

Numerals

When construed as a natural, empty is called zero or 0; its successor, {0}, is called one or 1; {0, 1} is called two; {zero, one, two} is called three. This may be continued as long as your patience and capacity for counting last.

Formally, I'll define names for natural numbers in base two as: the base two names of zero and one are 0 and 1, as given. For any natural number whose base two name is a succession of repeats of the digit 1, the base two name of its successor is obtained by replacing each 1 with a 0 and prepending a 1 to the result – so two is written 10. The base two name of any other natural number has at least one 0 in it: its successor's base two name is obtained by copying out the given name up to but not including the last 0, replacing this 0 with a 1 and replacing each subsequent 1 (if any) with a 0. Thus one is 1, three is 11 (so four is 100), five is 101, six is 110, seven is 111 (so eight is 1000) and so on.

One may equally define other names for numbers by various means: and the above may be generalised, given single-character names for the members of some natural n>1, to name natural numbers in base n.

Intersections

Consider the intersection of a non-empty collection of naturals. Each of the naturals involved subsumes the intersection, hence each of its members, hence the intersection subsumes each of its members; as the collection is non-empty, the intersection is a sub-collection of at least one natural, so each of its members is natural and it is finite. Thus the intersection of a non-empty collection of naturals is natural.

For any non-empty collection, C, of naturals, with intersection n, we have n not in n, hence there must be some member, N, of C with n not in N: whence either n = N or N in n, whence n subsumes N. Since N is in C and n = intersect(C), N subsumes n, so N=n. Thus any non-empty intersection of naturals is one of the naturals intersected: it is not equal to any of the other members, but each of them subsumes it, consequently it is < all the other members, making it a minimal element. So any collection of naturals has a minimal element.

Unions

For any collection, C, of naturals, any member of unite(C) is a member of some natural in C, so natural and subsumed by a member of C, so subsumed by unite(C): thus any union of naturals subsumes each of its members, each of which is natural. Describe a collection of naturals as unitive if it subsumes each of its members: so a natural is a finite unitive collection of naturals. Any unitive C subsumes its union, because it subsumes each of its members. Any unitive C which is subsumed by some natural is finite and hence natural. A union of naturals subsumed by some given natural is necessarily unitive and subsumed by that natural, hence finite, hence natural. In particular, the union of any natural, N, is natural and N subsumes it.

What I want to prove is that any finite union of naturals is natural. What I can now prove is that the union of any list of naturals is natural.

Theorem: the union of any list of naturals is a natural: if the list is non-empty, the union is one of its members.

Proof: by dealing directly with the easy cases and inductively with the rest. If the list is empty, so is its union, which is consequently natural (as empty is natural). Otherwise, the list is ({naturals}: f |successor(n)) and its union is unite(:f:n)&unite;f(n).

For any naturals n, m, we know that either n subsumes m or (optionally via n being in m) m subsumes n. Consequently, their union is either n or m.

So now consider some natural, n, for which each list ({naturals}: |n) has a natural union and either this is an entry in the list or the list is empty (in which case the union is empty = n). Any list ({naturals}: f |successor(n)) has unite(f) = unite(:f:n)&unite;f(n), which is either f(n) or unite(|f:n). If n is empty, so is the latter, so unite(f) = f(n) = f(empty) is an entry in f: otherwise, unite(|f:n) is an entry in (:f:n), hence in f. Either way, unite(f) is an entry in f – and natural.

Clearly, if n is the union of some non-empty list of naturals, it subsumes every entry in that list so, all the other entries are members of this one: that is < n. Thus, in fact, every non-empty list has a maximal element which is the union of the list.

Lemma: every sub-collection of a natural is the collection of outputs of some list. Proof: describe a natural as listable if every subcollection of it is the collection of outputs of some list. If N is a natural whose members are all listable, consider a sub-collection, S, of it. Let n = unite(S): it's subsumed by unite(N), which is natural, so n is finite and unitive, hence natural. Either N is empty, implying S is empty, so S is the collection of entries in [], the empty list; or unite(N) is in N and subsumes n, so n is a member of N. Now n = unite(S) subsumes every member of S, so all other members of S are members of n, which is listable. So S = {n}&unite;M for some sub-collection M of n, which is listable, giving us a list (M|f|h) for some natural h, so define a list (S: g :successor(h)) by g(h) = n, (:g:h) = f. We find (|g:) = {n}&unite;M = S, so N is listable. Therefore, by induction, every natural is listable [we can't build a non-listable natural without having one already at our disposal].

Thus every union of a sub-collection of a natural is a member of that sub-collection (and maximal in it, as for lists).

Arithmetic

Given n in N, is successor(n) in successor(N) ? N subsumes successor(n), so isn't in it, so successor(n) doesn't subsume successor(N), so is in it.

From this elementary foundation we can define addition and multiplication. We'll shortly come to proofs of various properties of the natural numbers and these two combiners.

Some Properties

First: every natural number is a collection – i.e. an identity. Proof, by induction: empty is an identity; if a natural number, n, is an identity, then successor(n) = n&unite;(n←;n); this maps x to y precisely if x=n=y or n relates x to y; with n an identity, the latter implies x=y, like the former; so successor(n) is also an identity.

In particular, for any n, successor(n) subsumes n: consequently, it also subsumes anything that n subsumes. Thus each natural number subsumes each of its members [proof: true for empty, as it has no members so we've claimed nothing; whenever natural n subsumes each of its members, successor(n) subsumes n, hence each of n's members; so successor(n) subsumes each of its members]. Thus any fixed point of any member of a natural number, n, is also a fixed point of n: n subsumes unite(n).

Indeed, for natural n, unite(successor(n)) = n&unite;unite(n) = n, as n subsumes unite(n). We have unite(empty) = empty = unite({empty}); any other natural number, m, is successor(n) for some natural n and so successor(unite(m)) = successor(n) = m, making unite and successor mutually inverse on the non-empty naturals.

Now, empty isn't a member of itself, and any other natural number is (from the definition) successor(n) for some natural n = unite(successor(n)). If it were a member of itself, it'd be a member of one of its members (namely itself), and so a member of its union, which is n. So, given a natural number n which isn't a member of itself, so n isn't a member of any of its members: but n is a member of its successor, so successor(n) isn't a member of n; and n isn't a member of itself so it isn't equal to successor(n); so successor(n) isn't n or any of n's members; so successor(n) isn't a member of itself.

Consequently, no natural number is a member of itself and we have a strict ordering on the natural numbers, defined as m>n iff n<m iff n in m. For this, we find that n<m implies: n<successor(m) and; either successor(n)<m or successor(n)=m. In particular, for each natural number, n<successor(n), so there is no biggest natural number.

Addition and Multiplication

These may be built out of repetition. Begin with

specified by:

We can then construct an addition and a multiplication out of:

Since I prefer to do my binary operators in bulk, I'll wait until I've discussed lists before going into these further; among other things, construing repeat(n,f) as compose({f}:|n) is my true motive for chosing to have repeat(0) map each relation, f, to the universal identity, rather than to some collection. Working backwards from the eminently reasonable repeat(1) we can infer that repeat(0,f) must be an identity which, composed either side of f, will yield f; this only obliges the identity to subsume f's collections of left and right values, and that collection would serve perfectly well as repeat(0,f). On the other hand, ({f}:|0) is the empty list, regardless of f, so reading repeat(n,f) as compose({f}:|n) requires repeat(0) to map every relation to compose([]); that this is obliged to be the identity is a detail I'll defer until I've explored lists.

Lists

A list is just a mapping, f, with (:f|) a natural number: when this is empty, f is empty and is written []; otherwise, (:f|) is successor(n) for some natural n and I write f= [f(0),…,f(n)], meaning [f(0)], [f(0),f(1)] and [f(0),f(1),f(2)] when n is 0, 1 and 2, respectively. Thus [a,b,c] maps 0 to a, 1 to b and 2 to c. For a list f, (:f|) is known as the length of f. Lists of length two are a common representation for pairs.

Various bits of mathematics are commonly defined in terms of pairs of values: some of these, notably associative binary operators, are more tidily expressed as actions on lists. Some, such as the Cartesian product, naturally generalise even further, to arbitrary mappings.

One simple property of the natural numbers: since each natural number, n, is an identity, we have n = (:i←i|n) as a list: indeed, 1+n= [0,…,n] = {0,…,n}. Note, for contrast: that this is also {n,…,0}, since {…} doesn't care about the order of its entries, but; that the list [n,…,0] maps 0 to n, n to 0 and i to j precisely when i+j=n: so this isn't the same mapping – it isn't even a collection – except when n is 0.

Permutations

A permutation is a recipe for shuffling the entries in a list; there is a minimum length of list to which a permutation can apply itself; but, for any longer list, it makes perfect sense to apply the permutation to only the initial sequence of the list that's long enough, leaving the tail of the list alone.

Formally, a permutation p is a (one-to-one correspondence a.k.a.) monic mapping whose outputs are its inputs: (|p:) = (:p|) is a collection. I shall discuss the natural permutations, (n|p|n) for arbitrary finite n subsumed by {naturals}, extending each such implicitly via extend = (: p&unite;{naturals not in (:p|)} ←p :), so that its action on general lists is (: h&on;extend(p) ←h :{lists}) whose output is always a mapping but only a list if (h:p:) is a permutation, i.e. (h:p|) = (:h|), e.g. if (h|p:) i.e. (:h|) subsumes (|p:), which is (:p|).

and (:permute|) relates two permutations to one another if each is the union of a collection with their intersection – i.e. the only difference between them is that one of them (irrelevantly, given implicit extension) mentioned some of their fixed points that the other didn't – so I'll tend to ignore fixed points of permutations, implicitly replacing a permutation, p, with what's left when it forgets all its fixed points, (: p(x)←x; p(x) is not x :) = p&intersect;(p: not equal :p).

The reversal peculiar to lists can be encoded via a permutation on the indices of the list, namely (: i←j; i+j+1=n :n) with n the length of the list; permute maps this to the mapping ({lists}| (: h(i)←j; i+j+1=(:h|) :) ←h |{lists}), which is monic and composes with itself to give the identity on lists; it may fairly be abbreviated to (: [a,…,z] ← [z,…,a] :).

There's a quite different reversal, intrinsic to relations, for which I reserve the name reverse = (: r←s; r relates x to y iff s relates y to x :); any mapping f, with f&on;f equal to the collection (|f:), is equal to its own reverse, i.e. f is self-inverse iff f = reverse(f). In particular, this applies to reverse itself, as f, and to the list-reversor, (: [a,…,z] ← [z,…,a] :).

Proof that f&on;f = (|f:) is a collection implies f = reverse(f):

Suppose f relates x to y; every left value of f is a right value of (|f:) = f&on;f hence also of f; so f relates some w to x; but f&on;f is a collection and now relates w, via x, to y; so w = y and f relates y to x. Then f relates x to y implies f relates y to x, so reverse relates f to f. Q.E.D.

Note that I don't need to require f to be a mapping, though certainly any mapping yields a collection as (|f:) = f&on;reverse(f).

Note that (|f:) can be a collection without f being a mapping, though f&on;reverse(f) can't. If f relates both x and y to some z, then f&on;reverse(f) relates x to y; so if f&on;reverse(f) is a collection, f is a mapping. But, for any mapping f, construct not f as F = ((|f:): y←x; f doesn't relate y to x :(:f|)) and observe that (|F:) relates y to z iff {x: F relates y to x} = {x: F relates z to x} iff {x in (:f|): f doesn't relate y to x} = {x in (:f|): f doesn't relate z to x} iff {x: f relates y to x} = {x: f relates z to x} iff (|f:) relates y to z, whence (|F:) is the same collection as (|f:) though F won't be a mapping if (:f|) has more than two members.

Now, the reverse of a mapping is monic and the reverse of a monic is a mapping so the reverse of any one-to-one correspondence is another; and composing any one-to-one correspondence to the left of its reverse yields its collection of left values, likewise for right. If the reverse of a list h is a list (: i ← h(i) |n) then h is a monic list (n|h|m); and naturals are finite, so each of n and m must be as big as the other for h to be both monic and a mapping, making any list whose reverse is a list a permutation, so ({list}:reverse:{list}) = ({permutations}|reverse|{permutations}), which serves as inverse.

A permutation, p, acts on lists, via extend(p) = p&unite;(: i←i; i not in (|p:) :{naturals}), as (: h&on;extend(p) ←h :). The left value (output) is only a list when (h:p:) is a permutation.

Un-Currie-ing

When it came to representing functions which take several arguments I chose to follow an orthodoxy which reduces all functions to ones taking only one argument; the curried form of a function f taking, say, three arguments is

so that f = (: f(a) ←a :) as for any mapping, with f(a) = (: f(a,b) ←b :) and f(a,b) = (: f(a,b,c)←c :). Thus Currie's technique delivers inputs one at a time by introducing intermediates – the mapping, at each step, to which to deliver the next input; at the last step this delivers the final output; until then, it delivers the next intermediate.

There comes a time when one wishes to do the reverse: package several inputs together (e.g. so as to be able to say something relating to them collectively), deliver them all at once (which is easy as long as the uncurried function understands the packaging), e.g. so as to relate properties of the answer to collective properties of the inputs. As it happens, there is a very simple way to encode this as the mapping:

or, arguably more formally:

Thus currie(uncurrie(f)&on;permute(p)) permutes f's inputs according to p; for example, currie(uncurrie(f)&on;permute([1,0])) = transpose(f).

Valid CSS Valid HTML ? Need XHTML's DTD hacks to handle custom entities.
Written by Eddy.