Given the naturals, define repeat = (: (: repeat(n, r) ←r |{relations}) ←n |{naturals}) by:

- repeat(0, r) is the universal identity (which relates x to x for all x), regardless of r; and
- repeat(n&unite;{n}, r) = repeat(n, r)&on;r, for every relation r and natural n.

Thus, for example, repeat(1, r) = r for all r; repeat(1) is {relations}, the identity on relations. Likewise, repeat(2, r) is r&on;r and repeat(3, r) is r&on;r&on;r; so repeat(n, r) is the result of composing r with itself n times. (Note: the outputs of repeat, {repeat(n): natural n}, are equivalent to the Church numerals, named after Alonzo Church, who first introduced them. My notation for relations is based on his lambda calculus.)

By interpreting repeat(n)&on;repeat(m) as repeat(n.m) we can define a multiplication on naturals; by interpreting (: repeat(n, f)&on;repeat(m, f) ←f :) as repeat(n+m), we can define an addition. I shall show, below, that we can interpret each in the required way, that the resulting multiplication and arithmetic do lead to the basic properties familiar from whole-number arithmetic and combine to form a ringlet, implying lots of useful properties of the naturals. When we compose the reverse of repeat(n) after repeat(m), we can even define a division; but that is a topic for another page, as is repeat's clean interaction with the ingredients of equivalence.

I could equally specify repeat in terms of the bulk action of composition, indeed repeat = scale(bulk(&on;)) in those terms, but my discussion of bulk action depends on arithmetic, which I derive below from repeat, so I avoid a cyclic dependency by defining repeat independently here. None the less, everything about binary operators does apply equally to &on;, so we can indeed define its bulk action and establish that repeat is just what that bulk action leads to and all the same results shall hold. We just need to deal with repeat in a raw mode before we can establish the framework within which to build the general theory that'll let us handle the same material more fluidly.

One could use repeat(1) = {relations} in place of the given specification of repeat(0), in a context that isn't comfortable with the universal identity – or if you prefer to start your counting at 1 instead of 0.

When starting from 0, one might hope to replace repeat(0) with something less enormous; at first sight, we might hope to get away with some identity that composes with the input to give the input, and this could depend on the input. When we come to consider repeat(n, r)&on;repeat(m, r) = repeat(n+m, r), the cases n = 0 (with non-zero m) and m = 0 (with non-zero n) require repeat(0, r) to subsume both (r: x←x :) and (: x←x :r), whose union is {values of r} = {x, y: r relates x to y}.

Sadly, that fails when we come to repeat(n, g&on;h) = repeat(n, g)&on;repeat(n, h) for n = 0 when h = g has left and right values but no value that's both, e.g. the singleton mapping 1←0, so that g&on;h = empty = h&on;g, hence so is {values of g&on;h), the proposed value of repeat(0, g&on;h), yet each of repeat(0, g) and repeat(0, h) is their (non-empty) collection of values, which composes with itself to produce itself, not empty.

So, to use something less powerful than the universal identity as output of repeat(0), it would be necessary to complicate the statements and proofs below in so far as they implicate repeat(0) – or to limit ourselves to (: repeat :{positive naturals}). That last option is not so unreasonable, after all; and is actually all I really need when I come to consider division, which has to exclude 0 in any case, and the ingredients of equivalence. It remains that we may as well specify (: repeat |{naturals}), since the above choice for repeat(0) does in fact work in so far as repeat(0) is relevant.

None the less, using (: {values of r} ←r :{relations}) as the action of 0, where all other naturals n act as repeat(n), is sometimes constructive; for example, in my treatment of natural ratios I use this, naming it ρ, as it avoids various difficulties with the universal identity (above and beyond the fact that some foundations don't support such an entity). Most of the following works for it, with the exception of commuting relations having commuting repeats, with repeat(n, g&on;h) = repeat(n, g)&on;repeat(n, h), which ends up only being true for positive n or when g, h and g&on;h = h&on;g have the same collection of values. Having repeat(0) output the universal identity avoids that limitation below, but there are contexts in which it is unproblematic to use the values-of-the-relation choice for repeat(0).

Various things are intuitively obvious (to anyone familiar with the usual arithmetic of counting numbers) yet need to be proven, if only to establish that the naturals, as I've defined them, actually deserve to be identified with the vernacular's counting numbers.

I shall describe repeat(n, r), for any natural n and relation r, as a
repeat of

r; i.e. a result of applying some output of repeat to r. We need
to establish that composing repeats of r always produces a repeat of r; thence
that repeating repeats of r always produces a repeat of r.

We have repeat(n&unite;{n}, r) = repeat(n, r)&on;r; we shall need to know that this is in fact also equal to r&on;repeat(n, r). So suppose repeat(i, r)&on;r = r&on;repeat(i, r) for all i in n, for some natural n; if this implies that repeat(n, r)&on;r = r&on;repeat(n, r) then we can induce that this holds for every natural n. If n is empty, we have repeat(n, r)&on;r = r = r&on;repeat(n, r) because repeat(n, r) is the universal identity. Otherwise, n is i&unite;{i} for some i in n, hence repeat(n, r) = repeat(i, r)&on;r = r&on;repeat(i, r) for this i; but then repeat(n, r)&on;r = r&on;repeat(i, r)&on;r = r&on;repeat(n, r) and we have shown what we needed. Thus every repeat of r commutes with r.

Next suppose we have some natural n for which, for all i in n and every natural m, (: repeat(i, r)&on;repeat(m, r) ←r :) = repeat(k) for some natural k; if we can show the same holds with n in place of i, then we can induce that it holds for every natural n. (Note that the phrasing, in terms of a mapping derived from repeat(i) and repeat(m) yielding repeat(k), ensures that the k involved does not depend on r, as might be implicit if we merely showed that repeat(i, r)&on;repeat(m, r) = repeat(k, r) for some natural k.) So consider (: repeat(n, r)&on;repeat(m, r) ←r :) for some natural m. If n is empty, each repeat(n, r) is the universal identity and (: repeat(n, r)&on;repeat(m, r) ←r :) = repeat(m). Otherwise, n is i&unite;{i} for some i in n and

- (: repeat(n, r)&on;repeat(m, r) ←r :)
- = (: repeat(i, r)&on;r&on;repeat(m, r) ←r :)
- = (: repeat(i, r)&on;repeat(m&unite;{m}, r) ←r :)
by the previous result, r&on;repeat(m, r) = repeat(m, r)&on;r,

- = repeat(k)
for some natural k, by the inductive hypothesis applied to i in n.

We can duly induce that every composite of repeats of a given relation is a repeat of that relation. From this it immediately follows that a repeat of a repeat of r is indeed also a repeat of r. In each case, the number of repeats of r in the result is independent of r; it depends only on the numbers of repetitions in each of the ingredients used to make the result. Thus the collection of repeats of any given relation is closed under composition; as is the collection of outputs of repeat.

Next, suppose we have two relations h and g that commute with one another, that is h&on;g = g&on;h. We shall need to know that any repeat of h likewise commutes with any repeat of g; and that a repeat of h&on;g can be rewritten as the relevant repeat of h composed with that of g. All of this just amounts to saying that shuffling the order of a ({g,h}::) list doesn't change the result of composing the entries in the list.

First, suppose we have some natural n for which, for all i in n,
h&on;repeat(i, g) = repeat(i, g)&on;h; if we can infer, from this, that the same
holds with n in place of i then we can induce that it does indeed hold for every
natural n. If n is empty then repeat(n, g) is the universal identity and duly
commutes with h, as required. Otherwise, n is i&unite;{i} for some i in n and
we have h&on;repeat(n, g) = h&on;repeat(i, g)&on;g = repeat(i, g)&on;h&on;g =
repeat(i, g)&on;g&on;h = repeat(n, g)&on;h, as required. Thus, whenever h
commutes with g, h also commutes with every repeat of g. Taking a repeat of g
in h's place, with h in g's place (since commutes with

is necessarily a
symmetric relation), we can further infer that every repeat of g commutes with
every repeat of h.

Finally, for this section, suppose we have some natural n for which, for every i in n, repeat(i, h&on;g) = repeat(i, h)&on;repeat(i, g). If n is empty, we have repeat(n, h&on;g) = repeat(n, h)&on;repeat(n, g) because the universal identity is an identity, so composing it with itself gives itself. Otherwise, n is i&unite;{i} and

- repeat(n, h&on;g)
- = repeat(i, h&on;g)&on;h&on;g
- = repeat(i, h)&on;repeat(i, g)&on;h&on;g
by the inductive hypothesis

- = repeat(i, h)&on;h&on;repeat(i, g)&on;g
thanks to the first result in this section

- = repeat(n, h)&on;repeat(n, g)

and we can duly induce that repeat(n, h&on;g) = repeat(n, h)&on;repeat(n, g) for every natural n, whenever h&on;g = g&on;h.

Next I need to show that repeat is monic; that is, repeat(n) = repeat(m) precisely if n = m. To this end, consider the mapping succ = (: n&unite;{n} ←n :), which maps each natural to its successor. Suppose we have some natural n for which, for all i in n, repeat(i, succ, empty) = i. If n is empty, repeat(n, succ, empty) = empty = n as the universal identity maps empty to itself. Otherwise, n is i&unite;{i} = succ(i) for some i in n and, for this i, repeat(n, succ) = repeat(i, succ)&on;succ = succ&on;repeat(i, succ) by the above; it thus maps empty to repeat(n, succ, empty) = succ(repeat(i, succ, empty)) = succ(i) = n, using the inductive hypothesis; from which we can infer that indeed repeat(n, succ, empty) is n for every natural n.

It immediately follows that, whenever naturals n, m have repeat(n) = repeat(m), by passing succ to each and empty to the result, we can infer n = m. Thus repeat is monic.

The various ways of combining repeat's outputs, above, that we showed must produce outputs of repeat, can thus be pulled back to ways of combining the inputes to repeat, whose outputs we combined, to produce the unique natural that repeat maps to the result of combining those outputs.

The properties of repeat now enable us to define the standard arithmetic operations on the natural numbers.

We now know that, for any naturals n, m, repeat(n)&on;repeat(m) is repeat(k)
for some unique natural k; we can duly define a binary operator, multiply = (:
({naturals}: n.m ←m :{naturals}) ←n :{naturals}), defined by
repeat(n)&on;repeat(m) = repeat(n.m). This binary operator is known
as multiplication

and commonly pronounced times

– i.e. n.m
is pronounced en times em

. It is unambiguous, thanks to repeat being
monic. Since composition of relations is
associative – i.e. (f&on;g)&on;h = f&on;(g&on;h) for all relations f, g, h
– our multiplication is also necessarily associative, (n.m).k = n.(m.k)
for all naturals n, m, k, allowing us to write the given product as n.m.k
without needing parentheses to indicate the order in which to perform the two
multiplications.

For 1 = empty&unite;{empty}, we have repeat(1) = {relations}, the identity
on relations; repeating

a relation once just means applying
it. Composing this before or after any other repeat gives that same repeat;
thus 1.n = n = n.1 for every natural n. In particular, as multiply(n) maps 1 to
n, we can infer that multiply is monic: multiply(n) = multiply(m) implies n =
multiply(n, 1) = multiply(m, 1) = m. Later, we shall see that each output of
multiply, aside from multiply(0), is also monic; but, to establish that, I'll
need some more tools.

For 0 = empty, we have repeat(0) mapping every relation to the universal identity; composing this before repeat(n) maps every relation to repeat(n) of the universal identity, which is necessarily the universal identity, so repeat(n)&on;repeat(0) = repeat(0); while composing it after repeat(n) maps every relation, via its repeat(n), to the universal identity, so repeat(0)&on;repeat(n) = repeat(0) again. Thus n.0 = 0 = 0.n for every natural n.

Now, repeat(n, empty) is empty for every positive natural n yet repeat(0, empty) is the universal identity. So consider any naturals n, m with n.m = 0; thus repeat(n, repeat(m, empty)) is the universal identity. Either m is empty or: repeat(m, empty) is empty and repeat(n, empty) can only be the universal identity if n is 0. Thus n.m = 0 implies that either n or m is 0.

Suppose we have some natural n for which, for all i in n and every natural m, i.m = m.i, i.e. repeat(i) commutes with repeat(m). We have already established that repeat(0) and repeat(1) commute with repeat(m) for every natural m; so we need only consider the case n > 1. We thus know n = i&unite;{i} for some i in n with i.m = m.i for every natural m. Now consider

- repeat(n)&on;repeat(m)
- = (: repeat(n, repeat(m, r)) ←r :{relations})
- = (: repeat(i, repeat(m, r))&on;repeat(m, r) ←r :{relations})
- = (: repeat(m, repeat(i, r))&on;repeat(m, r) ←r :{relations})
by the inductive hypothesis

- = (: repeat(m, repeat(i, r)&on;r) ←r :{relations})
by applying repeat(m, h)&on;repeat(m, g) = repeat(m, h&on;g) when h&on;g = g&on;h, given that r and repeat(i, r) commute.

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

and n.m = m.n also. Thus, by induction, we infer that our multiplication is Abelian, a.k.a. commutative, i.e. it doesn't care about the order of its operands. We incidentally also see that the outputs of repeat all commute with one another.

Define a binary operator add = (: ({naturals}: n+m ←m :{naturals}) ←n :{naturals}) by repeat(n+m) = (: repeat(n, r)&on;repeat(m, r) ←r :); we know the right-hand side of this is repeat(k) for some natural k, by the above, for any given n and m; and k can clearly only depend on n and m, by the structure of the right-hand side, so this does define a binary operator; and repeat is monic, so the binary operator is unambiguous. We've established that repeats of any given r commute with one another – repeat(n, r)&on;repeat(m, r) = repeat(m, r)&on;repeat(n, r) for any relation r and naturals n, m – so n+m is necessarily equal to m+n, making our addition Abelian. Composition of relations is associative, hence so is our addition: (n+m)+p = n+(m+p) for any naturals n, m and p, allowing us to write n+m+p without need of parentheses to indicate the order in which to do the additions. As repeat(0, r) is the universal identity for every relation r, 0+m = m = m+0 for every natural m, making 0 an identify for our addition. In particular, as add(n, 0) = n for each natural n, we can infer that add is monic: if add(n) = add(m) then n = add(n, 0) = add(m, 0) = m.

Since repeat(1) = (: r ←r :{relations}), we get repeat(n, r)&on;repeat(1, r) = repeat(n&unite;{n}, r) so that n+1 = n&unite;{n} and add(1) = (: 1+n ←n :{naturals}) is the successor operation (used above in the proof that repeat is monic) on {naturals}. Now suppose we have some natural m for which, for all i in m, add(i) = (: repeat(i, add(1)) :{naturals}). If m is 0 = empty, repeat(0, add(1)) is the universal identity; which is why I restricted repeat(i, add(1)) to naturals, so that (: repeat(0, add(1)) :{naturals}) is the identity on {naturals}, which is indeed add(m) = add(0) from the last paragraph. Otherwise, m is i+1 for some i in m, with add(i) = (: repeat(i, add(1)) :{naturals}); so now consider, for this i and any natural n, n+m = n+i+1 = add(1, add(i, n)); this being true for every natural n, we have add(m) = add(1)&on;repeat(i, add(1)) = repeat(i+1, add(1)) = repeat(m, add(1)), which is (: :{naturals}) as m is non-empty. We can thus infer add(m) = (: repeat(m, add(1)) :{naturals}) for m whenever it's true for every i in m; and, from this, we can induce that it's true for all naturals.

Endlessly repeating the (: :{naturals}) to narrow repeat(0)'s output gets boring fast and only detracts from readability, so please interpolate an implicit application of this restriction to any repeat(n, add(m)) hereafter. Applying repeat(n, add(1)) = add(n) to a product, we have add(n.m) = repeat(n, repeat(m, add(1))) = repeat(n, add(m)) from the definition of multiplication. This little fact shall prove endlessly useful when we come to study ratios – especially when combined with the associativity of addition, which can be expressed as add(n)&on;add(m) = add(n+m).

Suppose, for some natural m, we know that add(i) is monic for each i in m;
i.e. i+n = i+p for some naturals p and n

, with i in m, implies n =
p

. If m is empty, we have add(0) as the identity, which is manifestly
monic. Otherwise, m is i+1 for some i in m and, whenever naturals p and q
satisfy m+p = m+q, we have i+1+p = i+1+q whence 1+p = 1+q, i.e. p&unite;{p} =
q&unite;{q}; as p subsumes every member of p&unite;{p} and q is a member of it,
we know p subsumes q; conversely, q subsumes p and we have p = q. Thus add(m)
is monic whenever add(i) is monic for all i in m; from which we may induce that
all outputs of add are monic. This is equivalent to saying our addition is
cancellable: n+p = m+p implies n = m.

We have now shown that add is associative, abelian and cancellable; that it is flat and closed arises from its definition, which limits it to {naturals} and exploits results we showed earlier that ensure it combines any two naturals to make a natural. Consequently, add is indeed (as its name and my title for this section suggest) an addition (in my formal sense of the term).

Suppose we have a natural m for which, for all i in m, i+n subsumes i for every natural n. If m is empty, m+n inevitably subsumes m because everything does; otherwise, m is i+1 for some i in m. For any natural n, we know i+n subsumes i; consequently, i is in 1+i+n = m+n. Every member of m = 1 +i = i&unite;{i} either is i or is in i; m+n is natural so subsumes each of its members; m+n has i as a member and subsumes i, hence subsumes m. We can now induce that m+n subsumes m (and, by symmetry, n) for all naturals n, m. Furthermore, if n is non-empty it is i+1 for some i in n, m+i subsumes m so m+n = m+i+1 has m as a member; every natural m is in m+n for every positive natural n.

Since each add(i) is a monic mapping ({naturals}: |{naturals}), its left-relation (| add(i) :) is a collection of naturals; each natural in it is i+n for some natural n, so subsumes i, hence isn't a member of i, so i and (| add(i) :) are disjoint (their intersection is empty). Consider a natural m for which, for each i in m, i&unite;(| add(i) :) is {naturals}. If m is empty, then (| add(m) :) is just (| n←n :{naturals}) which is {naturals}. Otherwise, m is 1+i for some i in m, with {naturals} = i&unite;(| add(i) :) so every natural not in i is i+n for some natural n; when n is 0, this is i in m, otherwise n is 1+j for some natural j and i+n = i+1+j = m+j in (| add(m) :); thus every natural not in m is in (| add(m) :) and m&unite;(| add(m) :) = {naturals}. In particular, every positive natural m has 0 in m hence 0 not in (| add(m) :), so p +q = 0 implies p = 0 = q, for natural p, q: no positive natural has an additive inverse (in {naturals}).

Given the ordering of the naturals, we can now assert, for any naturals n, m: either

- n subsumes m, in which case n is not in m and there is some natural p for which m+p = n; or
- n is in m, in which case there is some non-zero natural p for which n+p = m.

The last follows from m not being in n, hence there being a p with n+p = m, and m not being equal to n (since m is not a member of itself), hence p is not 0. We can equally restate the three-way split of the ordering as: for any naturals n, m, exactly one of the following holds true:

- n = p + m, for some positive natural p, and m is in n
- n+0 = m = n = m+0
- n + p = m, for some positive natural p, and n is in m

Exercise: when natural m subsumes natural n, show that the p for which n+p = m is in fact p = {i in m: i+n in m}.

In particular, this ensures that addition and the ordering behave sensibly together: for naturals g, h, n, m with g≤h and n≤m we have h = g+q and m = n+p for some naturals q and p, each of which is zero precisely if the matching ≤ was in fact =, so that

- h +n = g +n +q so g +n ≤ h +n
- h +m = g +n +p +q so g +n ≤ h +m

with equality in the latter precisely when p +q = 0, which arises precisely if p = 0 = q, i.e. when each original ≤ was in fact equality also. If we have naturals g, n, m with g+n < g+m then we have g+n+p = g+m for some positive natural p; as add(g) is monic, this implies n+p = m, hence n < m, i.e. we can cancel a common term added to both sides of a comparison without changing the truth of the comparison.

Suppose we have naturals n, m and i; consider add(i.(n +m)) = repeat(i,
add(n)&on;add(m)), in which we know add(n) and add(m) commute, so we can use the
repeat(i, g&on;h) = repeat(i, g)&on;repeat(i, h) result above to get
add(i.(n+m)) = repeat(i, add(n))&on;repeat(i, add(m)) = add(i.n)&on;add(i.m) =
add((i.n) +(i.m)). As add is monic, this tells us i.(n +m) = (i.n) +(i.m). To
save some parentheses hereafter, let us adopt the orthodox convention that
multiplication binds more tightly than

addition: x.y.z +p.q is read as
(x.y.z) +(p.q), and so on. Thus i.(n +m) = i.n +i.m;
i.e. multiplication distributes over

addition.

We've already seen that our addition is associative, commutative and cancellable; and our multiplication is associative, with identity 1; since the latter distributes over the former, they thus constitute a ringlet on {naturals}. I next prove some technical details about exactly what kind of a ringlet it is; see the linked discussions for the detailed implications. We've already seen that this ringlet has no proper zero-divisors.

Consider naturals n, m and p for which n.p = m.p, with p positive. Suppose that n subsumes m (since one of n, m must subsume the other); there is thus some natural i for which n = m+i and n.p = n.p +i.p. Now, add(n.p) is monic and maps 0 to n.p but also maps i.p to n.p; so i.p must be 0, and we're given that p is positive, so i must be 0, ensuring n = m. Thus each multiply(p), with p positive, is monic and the natural ringlet is descalable (i.e. its multiplication is cancellable aside from 0).

For naturals n, m, p with n < m and p positive, we have some positive natural k for which n +k = m, whence (applying distributivity) p.m = p.(n +k) = p.n +p.k; as p and k are non-empty, so is p.k hence p.m > p.n whenever m > n and p is positive. Thus, for p positive, one of the following holds true for any given naturals n, m:

- n < m and p.n < p.m
- n = m and p.n = p.m
- n > m and p.n > p.m

Since exactly one of these holds true, we can infer that multiplying by a positive natural preserves orderings. In particular, if n.p < m.p, with p positive, we can infer n < m, thus m = n+k for some positive natural k, for which we shall find m.p = n.p +k.p; thus if n.p +q = m.p for some naturals n, m with p, q positive, q is in fact k.p for some positive natural k. Thanks to this, the natural ringlet cancels down completions.

Now consider any ideal C in {naturals} with at least some non-zero member. Let m be intersect({i in C: 0 in i}), the smallest non-zero member of C. [I shall prove that C is a principal ideal, specifically {m.k: natural k}.] For any n in C, consider R = {natural r: n = r +i.m for some natural i}; clearly n is in R, as n +0.m = n. [The aim here is to show that 0 is in R, too; i.e. that n = i.m for some natural i.] For any r in R, if r ≥ m we have r = m +p for some natural p < r and n = r +i.m for some natural i, whence p +(1 +i).m = p +m +i.m = r +i.m = n, so p is also in R. If we now take r = intersect(R), we get the minimal natural in R; as it is minimal (and m is positive), there is no p in R for which r = p +m, so r < m; and we have some natural i for which r +i.m = n. As i.m and n are in C, which is an ideal, r is also in C; but is < m, which is the smallest non-zero member of C; therefore r = 0 and n = i.m is a multiple of m [which is what we introduced R to help us prove]. Thus every member of an ideal of {naturals} is a multiple of the least non-zero member of the ideal [i.e. C = {m.k: natural k}], so every ideal of {naturals} is a principal ideal and the naturals form a principal ideal ringlet. This, in turn, shall lead to unique prime factorisation of the positive naturals (which, I assure you, is a very important and useful property).

Now consider any naturals x, y with x > 0 and let q = unite({natural i: y
subsumes i.x}), the largest natural for which q.x is not greater than y; this q
is known as the quotient

of y upon division by x. Since y
necessarily subsumes q.x, we have some natural r for which y = r + q.x; this r
is known as the remainder

of y upon divison by x. Since q
+1 is not in the union from which we obtained q, we know y < (q +1).x whence
r +q.x = y < x +q.x and can infer, by cancelling q.x, that r < x. This
establishes that natural arithmetic forms
a Euclidean ringlet (with the identity
as size

function, d). This would establish that natural arithmetic is a
principal ideal ringlet, independently of the preceding paragraph (whose proof
has strong similarities to the reasoning here).

For a graphical aid to understanding why multiplication behaves the way it does, check out Ben Orlin's Sixth Sense for Multiplication.

Written by Eddy.