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:

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

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

I'll describe a numeric domain as differential iff

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)

Written by Eddy.
$Id: numeric.html,v 1.3 2009-08-09 14:40:00 eddy Exp $