A Glossary for foundation's shadow

This page gathers together definitions of various important entities in mathematics and points readers to more extensive definitions of those entities. All definitions here are built on my discussion of relations and the (now out-of-date) denotations I (used to) introduce for these.

Primitive Relations

[ denotations, eg -> and {} | relations | mappings ]

reverse
s-> (s relates y to x; x->y)

This is a mapping: it accepts any relation, s, and converts it into the relation, r, for which s relates y to x is equivalent to r relates x to y. A relation, s, is described as symmetric (under reversal) if s= reverse(s): reverse, read as a relation, is symmetric. For a symmetric s, s relates x to y implies s relates y to x.

sub-relation
relates s to r precisely if, for all x, y, s relates x to y implies r relates x to y.

That is, s is a sub-relation of r precisely if s relating x to y implies that r does the same: r may, of course, relate some values to one another over and above those related by s. Two relations are deemed equal precisely when each is a sub-relation of the other: indeed, sub-relation's intersection with its reverse is just the identity on relations. [See discussion under relations.]

subsumes
= reverse(sub-relation)

I'll say that one relation subsumes another if the latter is a sub-relation of the former. In particular, any set subsumes each of its subsets and any map subsumes any of its restrictions. I used to use the word contains to mean sometimes has as a member and sometimes has as a sub-whatever: I now use subsumes for the latter meaning, to avoid ambiguity.

(universal) equality or identity
x->x

This is a mapping and is symmetric (under reversal). Its sub-relations are called collections: a value x is described as in a collection A precisely if A relates x to x. This is equivalent to x being an initial or final value of A, given that A is a sub-relation of identity.

Equality also appears under the synomym embed, as its restriction (S: embed :D), when S is a sub-collection of D: this is the natural embedding of S in D. Note that, more generally, (S: x->x :D) is the identity on (S|)'s intersection with (|D).

empty
{}

This is the relation which doesn't relate anything to anything. It is a sub-relation of every relation - including identity, so it is a collection. It is also a mapping.

all
relates x to y for any x and any y.

I mainly use it as a place-holder, but it does show up (in its true naked form) if we try to intersect empty collections. As a place-holder, its typical use is in (A:all:B) which relates each final value of A to every initial value of B (so it's akin to a Cartesian product).

zero
a type; every (::{zeros}) isa zero

Note that any (empty::) is trivially a zero, hence so is any (::{(empty::)}), as well as every (::{(::{zeros})}). This is a strongly-inductive definition, so handle with care; but combining it with the natural reading of 0 as {} suffices to make every (::{0}) a zero.

produce
c -> x -> c

This is a mapping: it accepts any value, c, as input and produces a constant mapping as output: this mapping, produce(c), accepts (and ignores) any value, producing c as its output. Notice that produce is not, itself, a constant mapping, though its outputs are (and every constant mapping is a restriction of one of produce's outputs).

Remember to read the formulaic denotation as c-> (x->c).

fixed-point
relates r to x iff r relates x to x.

When r is a mapping, this relates it to those values which it preserves. Not all relations (or mappings) have fixed points. Identities have nothing else: fixed-point relates any collection to each of its members. A relation is described as reflexive if it has, as fixed points, all of its values, both initial and final. I'll say x is in r as a short-hand for x is a fixed point of r: this coincides with the usual meaning of in on collections and is convenient in other contexts.

unite
unite(r) relates x to y precisely if some final value of r relates x to y.

This is the union of all the final values of r. When r is a collection of relations, unite(r) is the union of its members. I'll refer to a union of pickles as a short-hand for the union of some relation of which each final value is a pickle, with anything in place of pickle for which that makes sense. Likewise for an intersection of.

By the nature of the definition, unite(f) = unite(f|) for any relation f: when f is a collection, f = (f|) so this says little; but when f is some more general relation (especially if given as some lengthy denotation, rather than as a simple name) I'll often write unite(f|) to remind readers that unite only cares about f's final values. (I used to define unite as uniting f's fixed points: but analogy with summation and similar operations calls for bulk actions to work on the final values of a relation, allowing for repetition even though unite ignores repeats.) If I want to refer to the union of the initial values of some relation, f, I can still do so as unite(|f), of course - or as unite(reverse(f)).

intersect
intersect(r) relates x to y precisely if every final value of r relates x to y.

This and unite generalise the binary operators &intersect; and &unite;, which combine two relations, A and B, as if the collection {A, B} had been the argument to intersect or unite, as appropriate. Fixed points of unite and intersect are rather interesting. If some value e has no final values (eg empty, but equally any non-relation), unite(e) is empty, while intersect(e) is all, the all-relation, which relates every value to every value: and unite(all) is all, while intersect(all) is empty.

Rene
({relations}: r-> Rene(r) :)

with Rene(r) relating ((|r)|u:) to ((|r)|v:) precisely if: r relates x to V implies V composes cleanly after ({x}:u:) with composite ({x}:v:). That is, V&on;({x}:u:) = ({x}:v:), and (|V) subsumes ({x}:u|).

When r is a pair, [s, t], of relations (so r is a mapping whose outputs are relations: its inputs are 1 and 0), Rene(r) is written s×t. When s and t are collections, s×t is the collection of lists, [a, b] with a in s and b in t.

When r is a mapping whose outputs are collections, Rene(r) is a collection whose members are mappings: each f in Rene(r) satisfies: (|r) = (|f) and; for each x in (|r), f(x) is in r(x). A pair of collections is just a special case of this with (|r) = {1,0} = 2.

When r is a mapping whose outputs are mappings, so is Rene(r). It accepts, as input, any mapping u which accepts the same inputs as r and, for each such, x, r(x) accepts u(x) as input. It maps each such u to ((|r)| x-> r(x,u(x)) :), ie Rene(r,u) accepts any input, x, accepted by r, feeds it to each of u and r, then feeds u's output as input to r's output.

When r is a collection of collections, Rene(r) is a collection whose members are mappings: a member of Rene(r) maps each member, x, of r to one of its members; u(x) is in x=r(x).

When r is a mapping whose outputs are relations, Rene(r) relates mappings to mappings: it relates u to v precisely if they accept the same inputs as r and, for each such, x, r(x) relates u(x) to v(x). Rene(r) is then

({mapping ((|r)| x->y :r(x))}:
u-> ((|r): x->(r(x)&on;u)(x) = r(x,u(x)) :r(x))
:{mapping ((|r)| x->z :(r(x)|))})

singleton
x-> y-> (x->y)

This is a mapping: it accepts any value, x, and produces a mapping, singleton(x). This accepts any value, y, and produces a mapping, singleton(x,y), which accepts x but nothing else, producing y as its output for x. Any such (second-stage) output of singleton is known as a singleton: these can be used in some contexts which might otherwise deploy a pair (eg disjoint sum).

Examples

shred
({relation r}: r-> {singleton(a,w): r relates a to w} :)

Thus shred(r) is the collection of singleton sub-relations of r; and unite&on;shred is the identity on relations, since unite(shred(r)) trivially relates x to y precisely if r does.

disjoin
r-> ((|r)| x->s :({x}: shred&on;r |))

This is a mapping: disjoin(r) relates x to s precisely if r relates x to some w of which s is a singleton sub-relation - notice that r may relate x to several such w, for any given s. This generalises the disjoint sum.

whereMap
r-> ({x: ({x}:r:) is a singleton}: r :)

This extracts a mapping from an arbitrary relation by throwing out any initial value which is related to more than one final value. It is a mapping; whereMap(whereMap) = whereMap = whereMap&on;whereMap; and its restriction to mappings is identity - ({mapping m}: whereMap :) = ({mapping m}: f->f :).

uniteMap
r-> ((|r): x-> unite({x}:r:) :)

This extracts a mapping from an arbitrary relation. Like whereMap, it is a mapping and acts as the identity on mappings, so long as their outputs are all relations: also, uniteMap &on; uniteMap is uniteMap. It throws away any final values (of its input, r) which aren't relations: given input r, its output uniteMap(r) is a mapping which, given input x, yields as output a relation, uniteMap(r,x). This relates u to v precisely if r relates x to some relation which relates u to v.

takes
(singleton: (x->y)->x :)

So, for any singleton s, {takes(s)} = (|s). Takes is a mapping: whenever some relation has singletons as its final values, composing takes after the relation has the effect of replacing each of its final values with the one initial value of that final value.

gives
(singleton: (x->y)->y :)

or takes&on;reverse, with the corresponding implications. Note that when f is a mapping which yields singletons, gives&on;f is the mapping obtained by replacing each output of f with its one final value.

pairs
r -> ((|r:{u}): x->y :(|u))

This relates x to y precisely if r relates x to some u of which y is an initial value.

pack
r-> (shred(pairs(r)): (x->y)-> (: ({x}:r|): v->u :({y}:v|) :) :).

Pack is a mapping: it converts a relation, r, into a relation, pack(r), which relates singletons to relations. For a mapping f whose outputs are all mappings, pack(f) is a mapping, and its outputs are all singletons. For any x which f accepts and y which f(x) accepts, pack(f) accepts the singleton relation x->y, aka the pair [y,x], and maps it to the singleton f(x)->f(x,y). Thus pack(f)'s inputs are obtained by gathering up two inputs to f using singleton: it produces an audit trail of outputs; one is usually interested in f(x,y), for which one can use gives&on;(pack(f)), since all pack(f)'s outputs are singletons.

r-> ({sub-relations of pairs(r)}: s-> (((|s):r|)

Tools

under
f-> reverse(f)&on;f

When f is a mapping, this is the equivalence on (|f) which relates x to y precisely if f(x)=f(y). For a general relation, r, under(r) is a relation on (|r), still, and trivially symmetric and reflexive, just not necessarily transitive. [As an example, let a, b, x, y, z stand for some distinct values, consider the relation unite({x->a, y->a, y->b, z->b}) - this unites the singleton relations which are the members (hence final values) of the {…} collection - and let e be the relation to which under maps this union. Then e relates x and y to one another; e relates y and z to one another; but e does not relate x to z.] Under(r) relates x to y precisely if there is some a for which r relates both x and y to a.

quotient
r-> x-> ({x}:r|)

This mapping turns a relation, r, into a mapping: it maps a value x to {y: r relates x to y}, aka ({x}:r|), the collection of values to which r relates x. Thus uniteMap, above, is just r-> unite&on;(quotient(r)). When r is an equivalence, quotient can be very useful - and every equivalence is a fixed point of under&on;quotient. When f is a mapping, there is some mapping g for which g&on;(quotient&on;under(f)) = f; that is, f can be factorised via quotient&on;under(f).

transpose
f-> x in (|u), u in (f|); x-> (: f relates y to w, w relates x to v; y -> v :)

This is a mapping (and, strictly, I don't need to use the brackets that don't have | in them, but I hope they help). It only cares about those final value of its input which are non-empty relations: and all of its outputs are mappings.

Composing it with itself, we find transpose&on;transpose = uniteMap&on;({relation r}: r-> (:r:{non-empty relation}) :). The pre-filter given to uniteMap here just thins down any relation (or, indeed, any mapping) to one whose outputs are all non-empty relations. If f relates x to empty (and to no other relations), then (transpose&on;transpose)(f) doesn't accept x as input: whereas uniteMap(f) relates x to empty (and to nothing else). On a mapping whose outputs are non-empty mappings (ie they accept at least one input each), transpose&on;transpose acts as the identity.

[By contrast, without any need for filtering, transpose composes with uniteMap (in either order) to give transpose. Sounds similar to the way triple-negation equates to negation, in logic, with double-negation being a slightly trickier subject.]

final
y-> (f relates x to y; x->f)

This is a mapping: for any value y, final(y) is a relation: it relates x to f precisely if f relates x to y. This is reverse&on;(transpose(reverse)) and transpose&on;(transpose(transpose)), at least on non-empty relations.

Pause to notice the subtle distinction between:

f(g(x)) = (f&on;g)(x)

in which g is composed before f, x is fed to g as an argument, g(x) then being fed to f, so both f, g must be mappings; and

f&on;(g(x))
eg with f, g and x all equal to transpose or g=transpose, f=reverse=x

which composes g(x) before f, g being a mapping while g(x) and f are relations, though of course they may be mappings.

Likewise, transpose(transpose) is quite another thing from transpose&on;transpose, which is r->(: r :{non-empty relation}) - transpose is self-inverse on relations whose final values are all non-empty relations.

Notice that final(y) relates x to f iff f relates x to y, so that f in (final(y)|) is equivalent to y in (f|). Since, for every x, y, there is a singleton(x,y) which does relate x to y, every x and y have x in (|final(y):) and (see below) y in (:initial(x)|).

initial
x-> (f relates x to y; f->y)

This is the transpose of the identity on relations. It is a mapping: for any value x, initial(x) is a relation: it relates f to y precisely if f relates x to y. Notice that f in (|initial(x):) iff x in (|f).

evaluate
x-> (f->f(x)) = (mapping: initial(x) :)

This is the transpose of the identity on mappings. It is a mapping: evaluate(x) is in turn a mapping, accepting any mapping which accepts x; evaluate(x,f) is then f(x). The analogue for final is y-> (y=f(x), x->f), which is a mapping but its outputs are relations, not mappings; nor are their reverses mappings.

successor
r-> r&unite;(r->r)

This is a mapping which accepts any relation: successor(r) is a relation which relates x to y precisely if: r relates x to y or x=r=y. If r is a fixed point of r, this is just r: otherwise, it is one atomic relation, r->r or {r}, bigger. This is the tool with which the natural numbers are manipulated.

delegate
f-> intersect({relation g: f, unite(|g) and unite(g|) are all sub-relations of g})

This is a mapping which accepts any relation, f: delegate(f) has f as a sub-relation, as well as each of its initial or final values which is a relation.

On {relation f: f is neither initial nor final for delegate(f), whose initial and final values are all relations}, successor is closed and one-to-one. [The trailing whose … clause can be amended to allow other things than relations, so long as these are all defined a priori to any relation.] There is a strong sense in which these are the only constructible relations.

Bertrand
{relation r: r does not relate r to r}

Whether Bertrand relates Bertrand to Bertrand is, of course, undecidable - in the strong sense that taking either case as an assumption is guaranteed to yield a contradiction. Only in accepting our ignorance can we hope for consistency: but Heisenberg's heirs will not be scared by that ! [wombat]

transitive-closure
r-> intersect({C: r and r&on;C are sub-relations of C})

This is equally thought of as unite({r, r&on;r, r&on;r&on;r, …}), or defined inductively.

Counting

Ordinal
= {set N: Ordinal subsumes N, N subsumes each n in N}

Note that this only works if we can't prove that Ordinal is a set !

Natural
= {collection n: n subsumes each of its members, each of which is in Natural}

This is the collection {0, 1, 2, …} wherein: 0 is another name for empty; 1 is another name for successor(empty) = {0}; and, generally, 1+n (in common parlance) is {0, …, n} for each n in Natural.

repeat
(Natural: n-> (relation: f-> repeat(n,f) :relation) :)

wherein repeat(n,f) is defined inductively by repeat(0,f) = (|f) and, for each natural n, repeat(successor(n),f) = f&on;repeat(n,f). [Transitive-closure(f) is then just unite(Natural: n-> repeat(successor(n),f) :).] Notice that, when f is a mapping, so is each repeat(n,f) with n in Natural.

add
(Natural: n-> (Natural: m-> add(n,m) = repeat(n,successor,m) :Natural) :)

Thus add(1) is successor's restriction to Natural. [Strictly, add(0) is Natural itself.] The value of add(n,m), ie add(n)(m), is generally written as m+n. In particular, successor(n) is n+1.

When add is interpreted as a binary operator on Natural, various theorems about it can be proved. It is Abelian (that is, n+m=m+n: I will usually write successor(n) as 1+n rather than n+1), associative (k+(n+m) = (k+n)+m) and cancellable (n+m=n+k implies m=k). It has an identity, 0, and respects the natural order on Natural (namely, n<m precisely if n is in m) in the sense: n<m implies, for any natural k, n+k<m+k - furthermore, for any n<m, there is a unique natural k>0 for which n+k=m. The collection {natural n: 0<n} is called the positive integers: it is equally (Natural:successor|).

I'll also discuss contexts in which other things than naturals can be added and will use + for the binary operator involved and call the associated function add, as here.

multiply
(Natural: n-> (Natural: m-> multiply(n,m) = m.n = repeat(n,add(m),0) :Natural) :)

When read as a binary operator, this has 1 as identity, is Abelian, is associative and distributes over add. Its restriction to the positive integers is cancellable, respects order and can be expressed as multiply(1+n) = (: m-> repeat(n,add(m),m) so as to skip the need for an additive identity.

For any natural, n, we can extend multiply(n) to any context in which we have an addition, at least when n is positive (so that we can use the form without a presumed additive identity). This induces a multiplicative action of the (positive) naturals on every additive domain, which I'll always write as m-> n.m. I'll also use . as the binary operator for other multiplications which distribute over addition, generally those which may be viewed as extending this natural action of the naturals (typically involving some suitable image of the naturals among the multiplicative domain's members). (Other multiplications will usually be denoted with · as operator.)

power
(Natural: n-> (Natural: m-> power(n,m) = repeat(n,multiply(m),1) :Natural) :)

We can read this as a binary operator, too, power(n,m) = m^n, but it: isn't Abelian; has no left identity (no m for which m^n=n for all n); yet has a right-identity, 1, as m^1=m for each m; its restriction to n>0 is right cancellable (p^n = q^n implies p=q for n>0) and its restriction to m>1 is left cancellable (m^p = m^q implies p=q for m>1).

For any natural, n, we can extend power(n) to any context in which we have a multiplication. I won't generally use ^ as a binary operator, preferring power(,) as the denotation. We may also be able to extend power to accept some other inputs than naturals, eg sqrt = (: x-> power(1/2, x) :), in some contexts: in particular, wherever we have suitable log and exp functions at our disposal, for which power(n,x) = exp(n.log(x)) gives the right properties.

(list:supply:)

defined inductively by:

Since I write lists in the order (1+n:s:) = [s(n), …, s(0)] and supply arguments to mappings in the order (f(x))(y) = f(x,y), this means that supply([a,…,z]) maps f to f(a,…,z). Although a is highest-numbered in the list, it is supplied first.

Notice that transpose(supply) maps a relation, r, to a relation whose initial values are lists. This is transpose(supply, r): it relates [] to r, [a] to z iff r relates a to z, [a,b] to z iff r relates a to some y which relates b to z, [a,b,…,l,m] to z iff there are some n,o,…,x,y for which r relates a to n, n relates b to o, …, x relates l to y and y relates m to z.

reduce
a-> (list: s -> reduce(a,s) :), defined inductively by:

The second condition means that reduce(a,(1+n|s:)) relates x to z precisely if a relates s(0) to some q for which reduce(a,(n:s:))&on;q relates x to z. reduce(a, [n,…,w,x]) = reduce(a,[n,…,w])&on;a(x) = (Y| y-> (…(y*x)*…)*n :Y) = (Y| y-> y*(x. .n) :Y) when X = Y = {relation anonyme} with a = (X| x-> (X| y-> y&on;x :X) :), so that a(x,y) = y&on;x, reduce(a,(n: i-> s(1+i) :)) &on; a relates s(0) to some q which relates x to z. When a is a mapping, this becomes reduce(a,(1+n|s:) = reduce(a, (n: i-> s(1+i) :)) &on; (a&on;s(0)) - this composes a(s(0)), which needs to be a relation, before reduce(a, [s(n),…,s(1)]) - which will be reduce(a,[]) if n is 0. When a is a binary operator, (X| x-> a(x) = (Y| y-> a(x,y) :Y) :), we have (a|) as a sub-collection of {mapping (Y|:Y)}. It is usual to write a(x,y) in the form x*y for some * such as +, ×, … or &on;, which turns reduce(a, [x,…,o,n]) into (Y| y-> ((…(y*x)*…*o)*n) :Y).

If, for some mapping (X| star :{mapping (Y|:Y)}) with star(x,y) written y*x, every w, x in X imply a unique z in X for which a(z) = reduce(a,[w,x]), we can infer a binary operator on X, (X| stir :{X|:X}), defined by reduce(star,[w,x]) = a(stir(w,x)). [That uniqueness will involve a being cancellable.] When X is Y, star=stir iff star is associative. In any case, stir associates over star. Writing stir(w,x) as x.w, we obtain reduce(star, (1+n|s:)) = (Y| y-> ((…(y*s(n))*…s(1))*s(0)) :Y) = star(reduce(stir, (n|s:), s(n)))

[ denotations, eg -> and {} | relations | mappings | collections ]

livery
Written by Eddy.