[ denotations | bestiary | relations | mappings ]
Well, it's pretty important, so here's its page. This is the tool I use in building the natural numbers. The following three statements about a relation, r, are rendered equivalent by the definitions of successor and fixed-point:
In particular, for any collection C of relations,
in which {n: n in C} is just C, as is unite({{n}: n in C}), so this
First, let's see what successor does to other relations I've introduced. Reverse is a fixed point of reverse. Sub-relation is a sub-relation of itself (as every relation is a sub-relation of itself). Equality has every value as a fixed point, itself included. Mapping is a mapping, so a fixed point of itself. All relates everything to everything, itself included. So these relations are their own successors. [This corresponds to sets which are members of themselves, in the foundations I was taught.]
The effect of successor on empty gives us the natural numbers, with a little application ;^>
Produce is a mapping: it maps produce to a constant mapping (whose single output is produce, of course) but produce is not constant. Singleton(singleton) is y-> ({singleton}: s->y :), whose final values only accept one input, singleton, whereas singleton's final values accept any input. Transpose(transpose) doesn't have empty as a final value (because its output for any x does, at least, relate {x} to x) but transpose does (given a non-relation as input, for instance: or given any restriction of produce(empty)). Final(final) relates x to f precisely if f relates x to final; any collection with final as a member relates final to final, so final(final) relates final to each such collection; so final(final) is not a mapping, whereas final is. [Note: for the related mapping transpose(transpose) = transpose&on;final, call it lanif, we find that lanif(lanif) relates produce(lanif) to every value, so lanif(lanif) is also not a mapping, whereas lanif is.] Likewise, initial(initial) isn't a mapping. Evaluate accepts any value: but evaluate(evaluate) only accepts mappings which accept evaluate. For any relation x, unite({x}) = x = intersect({x}): so every relation is a final value of unite and of intersect. Thus unite(unite) = all and intersect(intersect) = empty. Thus each of these mappings, not being a fixed point of itself, differs from its successor.
[Aside: the related mappings which produce the union and intersection of all fixed points of their input (as opposed to the final values) are somewhat harder to analyse. The uniter has the collection of natural numbers as a fixed point, so its self-image subsumes the naturals, so has each natural as a fixed point, but no non-empty natural is a fixed point of the uniter, so it isn't self-fixed. Each fixed point, r, of the intersector is a sub-relation of each of r's fixed points - it is their intersection. An example might be (if you can stomach the concept) a collection whose single element is itself. The intersection of all fixed points of the intersector, intersector(intersector) is thus a subrelation of every fixed point of every fixed point of the intersector. I expect this makes it empty, am confident that it can't be equal to the intersector, but lack a proof !]
As delegate is a sub-relation of delegate(delegate), and all is a fixed point of delegate, all is a fixed-point of delegate(delegate). Consequently, it is also a sub-relation of delegate(delegate). Thus delegate(delegate) is all, whereas delegate relates empty to nothing but empty.
Whether fixed-point and successor are fixed points of themselves doesn't look decidable, to me.
Or: when does successor distinguish its inputs ?
The way I've constructed the naturals allows me to prove that ({naturals}: successor :) and (: successor :{naturals}) are monic mappings (ie one-to-one) with (| successor :{naturals}) = {naturals} subsuming ({naturals}: successor |). Thus, if two inputs to successor produce the same output, if the output is natural then the two inputs were equal, and if either input was natural then so was the output. What follows below depends on an earlier approach to defining and reasoning with the naturals and ordinals.
A mapping, f, distinguishes its inputs (or is monic
) precisely when f(x)
= f(y)
implies x=y
. Now, successor(x) = successor(y) tells us that x is
either y or a fixed-point of y (because x is a fixed point of successor(x)) and,
likewise, y is either x or a fixed-point of x: consequently, either y=x or y
relates x to x, x relates y to y and otherwise x, y coincide
. In trying to
discuss whether this latter condition implies x=y, we run up against issues of
decidability: consequently, using the law of the excluded middle (as I do in the
following) is perilous.
Let Heirs = {r: {r} = (| successor :{successor(r)})} and refer to any member
of Heirs as an heir
. (I'm playing Humpty-Dumpty here, I'm afraid: can anyone
think of a better word than heir for this job ?) An heir, r, is the only thing
whose successor is successor(r). An heir whose successor is a self-fixed-point
is equal to its successor: s= successor(r) relates s to s, so successor(s) = s =
successor(r), but r is an heir, so s=r. More usefully, this tells us that an
heir which isn't one of its own fixed points has a successor which, likewise,
isn't self-fixed. It remains to see when we can also discover that the heir's
successor is an heir.
A relation, such as empty, which has no fixed points at all cannot be the successor of anything: in particular, it thus differs from its successor. Furthermore, the only fixed point of the ensuing successor, s, is the original relation, which isn't s, so s isn't a self-fixed-point either. So any relation with no fixed points is an heir. In particular, Heirs isn't empty.
Describe a relation, n, as successive
if every fixed point of n is an
heir. For such n, consider any relation, k, whose successor is equal to
successor(n). Now, k is a fixed point of this successor so either k=n or k is a
fixed point of n; in the latter case, k is an heir, which again implies n=k. So
successor(k)=successor(n) implies k=n: any successive relation is an heir.
Consequently, any successive relation's successor is also successive. Notice
that any union of successive relations is successive, as is any sub-relation of
any successive relation.
Let H= {successive relation} be the collection of successive relations: this is a sub-collection of Heirs= {heir}. Notice that Heirs (and, thus, any sub-collection of it, H included) is successive and so a member of H - whence Heirs and H are members of themselves (and of one another), so each is its own successor and the only thing whose successor it is.
Thus far, then, we have, as heirs (ie relations from which successor
is invertible
)
With remarkably little dilligence (after all, relations lacking fixed points are two-a-penny, for starters) this is a tool-set capable of yielding plenty of heirs. I do not know whether there are heirs whose successors are not heirs ... but then again, I have trouble believing in non-heirs and am mostly concerned with members of H.
Crucially, aside from being an heir, any relation lacking fixed points is successive and differs from its successor: any successive relation which differs from its successor, s, is an heir - so s must, in its turn, differ from successor(s). Since s is also successive, we can thus repeatedly apply successor, getting a new successive relation at each application. This is the process by which we build up the natural numbers from empty: however, we need not start from empty or, indeed, from a relation lacking fixed points - we can start from any successive relation which differs from its successor.
We can also apply successor in reverse: if a relation's successor is
successive then the given relation is also successive; and if a relation, h, has
successor s with s not a fixed point of s, then s is not a fixed point of h, but
h is a fixed point of s, so h isn't s and h isn't a fixed point of h. We can
use this to rewind
any successive relation which differs from its successor,
as long as it is a successor. However far we rewind it, we get an alternate
start-point from which we can reach the original on our way to its successors.
It makes sense to rewind to a relation which is not the successor of anything:
this serves as an alternate start-point with a natural one-sidedness - assuming,
of course, that the rewinding operation terminates !
I'll describe a collection, C, as a limit precisely if (C: successor |) is a sub-collection of C: so the successor of any member of C is in C. (|All), the collection of all values, is a limit - as is empty. Any union or (non-empty) intersection of limits is a limit. Note that I regard non-empty limits as fiction.
If a collection, r, has a limit as its successor, then r is in the limit, consequently so is r's successor, so the limit is in itself. Thus any limit which is a successor is its own successor.
For any collection, r, we can collect together all the limits of which r is a sub-collection and take their intersection. There is at least one such limit, (|all), so this is never an empty intersection. The intersection is, itself, a limit and has r as a sub-collection. It is, in fact, (r: transitive-closure(successor) |)&unite;r. Crucially, it's a sub-collection of every limit of which r is a sub-collection. Notice that when r is empty so is its closure - whereas that of {empty} is rather more interesting.
Since every successive relation's successor is successive, H is also a
limit. Let L= {successive r: r not in r} - note that r not in r
is synonymous
with r is not its own successor
. L is successive, because all its members are
heirs: I must return later to the question of whether it is a member of
itself. We have already seen that the successor of a member of L is successive
and not a member of itself, so L is a limit.
Let E be any limit which is a sub-collection of L. For any sub-collection, N, of E (thus also of L), either N= successor(n) for some n or N is not its own successor, and so not a member of itself. In the former case, n is both a sub-collection and a member of N, thus of L, so n and N differ, with n an heir, so successor(N) and N=successor(n) differ, so N isn't in N. Thus no sub-collection of E is a member of itself. Thus nor is E a member of E. So E is successive - thus an heir - and not its own successor: E is a member of L. In particular, when E= intersect({limit C: e in C}) for some e in L (such as empty, in which case E is the natural numbers), E is a limit and a sub-collection of L, so also a member of L.
The attentive reader will already have noticed that L is a limit and a
sub-collection of itself, hence a member of itself, which is a contradiction. I
assume this arises from my heavy use of the law of the excluded middle (the word
not
appears far too often in the above), but if you can see some other error,
or can see how to escape the contradiction, please do tell me ! I look on this
problem as an illustration of why I shouldn't attempt to do
the foundations of
mathematics: that requires a lot more time and care, but I want to press on to
other things.
[ up | denotations | bestiary | relations | mappings | natural numbers ]
Written by Eddy.