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

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 Nandn not in nimplying 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.

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 isN 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:

- empty is natural,
- the successor of anything natural is natural,
- nothing else is natural.

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

.

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

.

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.

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

vian 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).

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

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.

These may be built out of repetition. Begin with

- ({mappings ({relations}: :{relations})}: repeat :{naturals})

specified by:

- repeat(0) = ({the universal identity}: |{relations}) is constant
- repeat(1+n,f) = f&on;repeat(n,f) for every natural n and relation f.
- from which we may infer that

repeat(1) = {relations}, the identity on relations.

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

- repeat(n+m) = (: repeat(n,f)&on;repeat(m,f) ←f :)

a.k.a. (: t(n)&on;t(m) ←t :)&on;transpose(repeat), with each t being a transpose(repeat,f), so t(n) = repeat(n,f). - repeat(n.m) = repeat(n)&on;repeat(m)

(notice how much simpler this is, however one looks at it …)

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.

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.

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

- permute = (: (: h&on;(p&unite;{i in (:h|): i not in (:p|)}) ←h :{mappings (::{naturals})}) ←p :{natural permutations})

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 collectionimplies 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 yimpliesf 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.

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

- (: (: (: f(a,b,c) ←c :) ←b :) ←a :)

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:

- uncurrie = (: (: f(a,…,z) ←[a,…,z] :{lists}) ←f :{relations})
- and the monic currie = reverse(uncurrie)

or, arguably more formally:

- transpose(uncurrie,[]) = {relations}; i.e. for any relation f, uncurrie(f,[]) = f.
- for any relation f, list h and natural n for which uncurrie(f) relates s to (:h:n) and s relates v to h(n), uncurrie(f) relates v to (:h|1+n); a.k.a. uncurrie(f,(:h|1+n)) = uncurrie(f,(:h:n),h(n)),

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 HTML ? Need XHTML's DTD hacks to handle custom entities.Written by Eddy.