What are numbers

I'll describe a domain, A, as `additive' in so far as context provides for it a binary operator, +, to which context has given meaning as `addition', provided:

• plus = (A| a-> (A| b-> a+b :A) :) is a mapping and does satisfy the assertions given (uses of `(A| ... :...)' in the denotation)
• (A: plus |) is closed under composition; in particular (+ is associative), for each a, b in A, plus(b)&on;plus(a) = plus(b+a) [I can just about believe there may be situations in which to relax the constraint to plus(b+a) subsumes plus(b)&on;plus(a), but leave that for another time]
• ...
• and will that do ?

This allows us, using `repeated addition', to define a scaling by the positive naturals: namely 1.a = a and, for any positive naturals n and m, (n+m).a = n.a + m.a; relying on associativity to ensure that this gives the same answer when n, m are replaced by alternatives with the same sum. For each n I'll define scale(n) to be (A| a-> n.a :A); we presently have (|scale:) subsuming {positive naturals} but as we go along we'll come up with further candidate members, so I'll describe a member of (|scale:) as a `scalar', so (|scale:) = {scalars}. For each a in A we can construct the mapping ({scalars}| n-> n.a :A), call it ray(a).

• 1.a = a, (n+m).a = n.a + m.a for any positive naturals n, m.
• scale = ({scalars}| n-> (A| a-> n.a :) :)
• ray = (A| a-> ({scalars}| n-> n.a :A) :)

Given additive domains A, W, I'll say that a relation (A: f :W) `respects addition' precisely when f(a+b) = f(a) + f(b) for all a, b in A; we can write this as f&on;plus(a) = plus(f(a))&on;f for each a in A. Note that each scale(n) respects addition. A binary operator, *, on A is described as `a multiplication' on A iff, for each c in A, a-> c*a respects addition. When a multiplication, *, on A produces answers in A, we can construe it in terms of star = (A| a-> (A| b-> a*b :A) :) as an embedding of A in {(A|f:A): f respects addition}, which subsumes (:scale|). Indeed, if * has a natural identity, e, star(e) will be scale(1), the identity on A; from which we can infer a model, within A, of the positive naturals as (:ray(e)|).

I'll describe an additive domain, (A: a-> (A: b-> a+b: A) :) as numeric iff

• for each positive natural n, (A: scale(n) |) is A; consequently we can divide by naturals [given a in A, observe that any member of (| scale(n) :{a}), just given to be non-empty, will serve as a/n]; consequently, we can extend (|scale:) to the positive rationals
• we have a multiplication on A posessed of an identity, e: given which we extend (|scale:) by writing A's multiplication as (A| a-> (A| b-> a.b :A) :) and identifying the members of (:ray(e)|) with the scalars we had before
• and will that do ?

I'll describe a numeric domain as differential iff

• there is a mapping from that domain to itself, we may as well call it exp, whose derivative is the linear map `multiply by the mapping's value'.
• ...
• and will that do ?

A binary operator, +, provides us with an embedding, plus, of A in {(A::A)} defined by a-> (A: b-> a+b :A) and guaranteed to deliver (:plus|) closed under composition: i.e., for any a, b in A, plus(a)&on;plus(b) is always plus(c) for some c in A. That this c is a+b corresponds to associativity of +.

When we repeat plus(a), composing it with itself repeatedly, say n times, we obtain plus(n*a)